fof(t29_wsierp_1,theorem,( ! [A] : ( v1_rat_1(A) => r1_int_2(k2_rat_1(A),k1_rat_1(A)) ) ), inference(mizar_proof,[status(thm)],[d3_rat_1,t29_int_2,d4_int_2,t35_int_2,t38_nat_1,d5_real_1,t31_int_2,t32_int_2,l12_wsierp_1,d9_int_1,d3_nat_1,t62_rat_1]), [file(wsierp_1,t29_wsierp_1),interesting(1.00)]). fof(t14_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => r1_int_2(1,A) ) ), inference(mizar_proof,[status(thm)],[t13_wsierp_1,d4_int_2]), [file(wsierp_1,t14_wsierp_1),interesting(0.95)]). fof(l72_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r2_int_1(A,B) <=> r2_int_1(A,k1_prepower(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_absvalue,d1_absvalue,t14_int_2]), [file(wsierp_1,l72_wsierp_1),interesting(0.95)]). fof(l47_wsierp_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( k2_finseq_3(1,k7_finseq_1(k9_finseq_1(B),A)) = A & k2_finseq_3(k1_nat_1(k3_finseq_1(A),1),k7_finseq_1(A,k9_finseq_1(B))) = A ) ) ), inference(mizar_proof,[status(thm)],[t56_finseq_1,t56_finseq_1,t27_finseq_3,d1_wsierp_1,t25_finseq_1,t47_finseq_1,l46_wsierp_1,l46_wsierp_1]), [file(wsierp_1,l47_wsierp_1),interesting(0.91)]). fof(l38_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ~ r1_xreal_0(B,A) <=> r1_xreal_0(A,k6_xcmplx_0(B,1)) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_int_1,t21_xreal_1,t21_xreal_1,t31_xreal_1,t2_xreal_1]), [file(wsierp_1,l38_wsierp_1),interesting(0.90)]). fof(l39_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_xreal_1,l38_wsierp_1]), [file(wsierp_1,l39_wsierp_1),interesting(0.90)]). fof(t35_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ? [C] : ( v1_int_1(C) & ? [D] : ( v1_int_1(D) & k3_int_2(A,B) = k2_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_int_2,t34_wsierp_1,d1_absvalue,d1_absvalue,d1_absvalue,d1_absvalue]), [file(wsierp_1,t35_wsierp_1),interesting(0.88)]). fof(l73_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ( r2_int_1(A,B) <=> r1_nat_1(A,k1_prepower(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l72_wsierp_1,l12_wsierp_1]), [file(wsierp_1,l73_wsierp_1),interesting(0.88)]). fof(l74_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => k6_int_1(k3_xcmplx_0(A,B),B) = 0 ) ) ), inference(mizar_proof,[status(thm)],[d8_int_1,d7_int_1,t90_xcmplx_1,t47_int_1,d8_int_1]), [file(wsierp_1,l74_wsierp_1),interesting(0.87)]). fof(l13_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_prepower(A) = A ) ), inference(mizar_proof,[status(thm)],[d1_absvalue]), [file(wsierp_1,l13_wsierp_1),interesting(0.86)]). fof(t9_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( r2_int_1(A,B) & r2_int_1(A,C) ) => r2_int_1(A,k2_xcmplx_0(B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_int_1,d9_int_1,d9_int_1]), [file(wsierp_1,t9_wsierp_1),interesting(0.86)]). fof(t31_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( ? [C] : ( v1_rat_1(C) & A = k2_newton(C,B) ) & ! [C] : ( v1_int_1(C) => A != k2_newton(C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_newton,t9_newton,t29_wsierp_1,t37_rat_1,d3_rat_1,t51_card_4,t15_prepower,t88_xcmplx_1,t15_wsierp_1,d4_int_2,t22_nat_1,t11_newton,d9_int_1,t33_int_2,t17_int_2,t9_int_2]), [file(wsierp_1,t31_wsierp_1),interesting(0.85)]). fof(t40_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ? [D] : ( v1_int_1(D) & ? [E] : ( v1_int_1(E) & k2_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,E)) = C ) ) <=> r2_int_1(k3_int_2(A,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_int_2,t32_int_2,t10_wsierp_1,d9_int_1,t35_wsierp_1]), [file(wsierp_1,t40_wsierp_1),interesting(0.84)]). fof(l8_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(C,B) ) => ( r1_xreal_0(C,k2_xcmplx_0(A,B)) & r1_xreal_0(k6_xcmplx_0(C,A),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_xreal_1,t22_xreal_1]), [file(wsierp_1,l8_wsierp_1),interesting(0.84)]). fof(t10_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ! [D] : ( v1_int_1(D) => ! [E] : ( v1_int_1(E) => ( ( r2_int_1(A,B) & r2_int_1(A,C) ) => r2_int_1(A,k2_xcmplx_0(k3_xcmplx_0(B,D),k3_xcmplx_0(C,E))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t12_int_2,t9_wsierp_1]), [file(wsierp_1,t10_wsierp_1),interesting(0.83)]). fof(l52_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ( r2_hidden(A,k4_finseq_1(B)) => k4_real_1(k16_rvsum_1(k11_wsierp_1(k1_numbers,A,B)),k1_wsierp_1(B,A)) = k16_rvsum_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseq_3,t27_finseq_3,l51_wsierp_1,t127_rvsum_1,t125_rvsum_1,t29_nat_1,t38_nat_1,t27_finseq_3,l42_wsierp_1,l44_wsierp_1,t50_finseq_1,t50_finseq_1,t127_rvsum_1,t127_rvsum_1,t125_rvsum_1,t127_rvsum_1,t38_nat_1,t27_finseq_3,s1_nat_1]), [file(wsierp_1,l52_wsierp_1),interesting(0.82)]). fof(l76_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( k6_int_1(B,A) = 0 => ( A = 0 | r2_int_1(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t80_newton,d9_int_1]), [file(wsierp_1,l76_wsierp_1),interesting(0.82)]). fof(t26_wsierp_1,theorem,( ! [A,B,C] : ( k2_finseq_3(1,k9_finseq_1(A)) = k1_xboole_0 & k2_finseq_3(1,k10_finseq_1(A,B)) = k9_finseq_1(B) & k2_finseq_3(2,k10_finseq_1(A,B)) = k9_finseq_1(A) & k2_finseq_3(1,k11_finseq_1(A,B,C)) = k10_finseq_1(B,C) & k2_finseq_3(2,k11_finseq_1(A,B,C)) = k10_finseq_1(A,C) & k2_finseq_3(3,k11_finseq_1(A,B,C)) = k10_finseq_1(A,B) ) ), inference(mizar_proof,[status(thm)],[t47_finseq_1,l47_wsierp_1,l47_wsierp_1,t56_finseq_1,l47_wsierp_1,t60_finseq_1,l47_wsierp_1,t61_finseq_1,l46_wsierp_1,l47_wsierp_1]), [file(wsierp_1,t26_wsierp_1),interesting(0.81)]). fof(l12_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_nat_1(A,B) <=> r2_int_1(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_nat_1,d9_int_1,d9_int_1,t133_xreal_1,t53_nat_1,t16_int_1,d3_nat_1]), [file(wsierp_1,l12_wsierp_1),interesting(0.81)]). fof(l9_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( ( r1_xreal_0(0,A) & ~ r1_xreal_0(B,C) ) | ( ~ r1_xreal_0(A,0) & r1_xreal_0(C,B) ) ) => ( ~ r1_xreal_0(k2_xcmplx_0(A,B),C) & ~ r1_xreal_0(B,k6_xcmplx_0(C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_xreal_1,t21_xreal_1]), [file(wsierp_1,l9_wsierp_1),interesting(0.81)]). fof(l75_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( k6_int_1(A,B) = k6_int_1(C,B) => k6_int_1(k6_xcmplx_0(A,C),B) = 0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_int_1,d8_int_1,l74_wsierp_1,d8_int_1]), [file(wsierp_1,l75_wsierp_1),interesting(0.81)]). fof(t48_wsierp_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( k2_finseq_3(1,k7_finseq_1(k9_finseq_1(B),A)) = A & k2_finseq_3(k1_nat_1(k3_finseq_1(A),1),k7_finseq_1(A,k9_finseq_1(B))) = A ) ) ), inference(mizar_proof,[status(thm)],[l47_wsierp_1]), [file(wsierp_1,t48_wsierp_1),interesting(0.81)]). fof(t13_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ( k3_int_2(0,A) = k1_prepower(A) & k3_int_2(1,A) = 1 ) ) ), inference(mizar_proof,[status(thm)],[d3_int_2,t7_absvalue,t65_newton,d3_int_2,d1_absvalue,t64_newton]), [file(wsierp_1,t13_wsierp_1),interesting(0.80)]). fof(l35_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(A,B) => m2_subset_1(B,k1_numbers,k5_numbers) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_int_1]), [file(wsierp_1,l35_wsierp_1),interesting(0.80)]). fof(l36_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(k1_nat_1(A,B),C) => ( r1_xreal_0(A,C) & r1_xreal_0(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t2_xreal_1]), [file(wsierp_1,l36_wsierp_1),interesting(0.79)]). fof(t15_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( r1_int_2(B,C) => r1_int_2(k2_newton(B,A),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_newton,t14_wsierp_1,t41_int_2,t11_newton,s1_nat_1]), [file(wsierp_1,t15_wsierp_1),interesting(0.79)]). fof(t18_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r2_int_1(k1_prepower(A),B) <=> r2_int_1(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_int_1,d1_absvalue,d9_int_1,d1_absvalue,d9_int_1,d9_int_1,d1_absvalue,d9_int_1,d1_absvalue,d9_int_1]), [file(wsierp_1,t18_wsierp_1),interesting(0.78)]). fof(t32_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( ? [C] : ( v1_rat_1(C) & A = k2_newton(C,B) ) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => A != k2_wsierp_1(C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_wsierp_1,t9_newton,t39_nat_1,t16_newton,t9_newton,t9_newton,t8_int_1,l14_wsierp_1,t3_wsierp_1,t3_wsierp_1,t8_int_2]), [file(wsierp_1,t32_wsierp_1),interesting(0.78)]). fof(t36_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( r2_int_1(A,k3_xcmplx_0(B,C)) & k3_int_2(A,B) = 1 ) => r2_int_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_wsierp_1,t10_wsierp_1]), [file(wsierp_1,t36_wsierp_1),interesting(0.78)]). fof(t6_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,k2_square_1(B,C)) <=> ( ~ r1_xreal_0(A,B) & ~ r1_xreal_0(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_square_1,t50_square_1,t50_square_1,d5_real_1,t49_square_1]), [file(wsierp_1,t6_wsierp_1),interesting(0.77)]). fof(t2_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( k2_newton(A,2) = k3_xcmplx_0(A,A) & k2_newton(k4_xcmplx_0(A),2) = k2_newton(A,2) ) ) ), inference(mizar_proof,[status(thm)],[t10_newton,t10_newton,t13_newton,t13_newton,t13_newton]), [file(wsierp_1,t2_wsierp_1),interesting(0.76)]). fof(t22_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( A != 0 => ( r2_int_1(A,B) <=> v1_int_1(k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_int_1,t90_xcmplx_1,t88_xcmplx_1,d9_int_1]), [file(wsierp_1,t22_wsierp_1),interesting(0.74)]). fof(l71_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_nat_1(A,B) => ( r1_xreal_0(A,B) | B = 0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t54_nat_1]), [file(wsierp_1,l71_wsierp_1),interesting(0.74)]). fof(t33_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_nat_1(k2_wsierp_1(B,A),k2_wsierp_1(C,A)) => ( r1_xreal_0(A,0) | r1_nat_1(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_nat_1,t39_nat_1,t16_newton,d3_nat_1,t51_card_4,d3_nat_1,t51_card_4,t90_xcmplx_1,t15_prepower,t32_wsierp_1,t12_newton,l15_wsierp_1,d3_nat_1]), [file(wsierp_1,t33_wsierp_1),interesting(0.73)]). fof(l32_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( A != 0 => ( r1_nat_1(A,B) <=> m2_subset_1(k6_real_1(B,A),k1_numbers,k5_numbers) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_nat_1,t90_xcmplx_1,t88_xcmplx_1,d3_nat_1]), [file(wsierp_1,l32_wsierp_1),interesting(0.73)]). fof(l45_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => r1_tarski(k4_finseq_1(k2_finseq_3(A,B)),k4_finseq_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d1_wsierp_1,t11_finseq_1,d3_finseq_1,t7_xboole_1,d1_wsierp_1]), [file(wsierp_1,l45_wsierp_1),interesting(0.72)]). fof(t8_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( ( r1_xreal_0(A,0) & ~ r1_xreal_0(B,C) ) | ( ~ r1_xreal_0(0,A) & r1_xreal_0(C,B) ) ) => ( ~ r1_xreal_0(B,k2_xcmplx_0(C,A)) & ~ r1_xreal_0(k6_xcmplx_0(B,A),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_xreal_1,t39_xreal_1,t55_xreal_1,t56_xreal_1]), [file(wsierp_1,t8_wsierp_1),interesting(0.72)]). fof(t27_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ( r2_hidden(A,k4_finseq_1(B)) => k3_real_1(k15_rvsum_1(k11_wsierp_1(k1_numbers,A,B)),k1_wsierp_1(B,A)) = k15_rvsum_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseq_3,t27_finseq_3,l51_wsierp_1,t105_rvsum_1,t103_rvsum_1,t29_nat_1,t38_nat_1,t27_finseq_3,l42_wsierp_1,l44_wsierp_1,t50_finseq_1,t50_finseq_1,t105_rvsum_1,t105_rvsum_1,t103_rvsum_1,t105_rvsum_1,t38_nat_1,t27_finseq_3,s1_nat_1]), [file(wsierp_1,t27_wsierp_1),interesting(0.70)]). fof(t34_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ? [C] : ( v1_int_1(C) & ? [D] : ( v1_int_1(D) & k6_nat_1(A,B) = k2_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t65_newton,t31_xreal_1,s5_nat_1,t42_nat_1,d3_nat_1,t42_nat_1,d3_nat_1,d5_nat_1,d5_nat_1,l12_wsierp_1,t10_wsierp_1,l12_wsierp_1,t52_nat_1]), [file(wsierp_1,t34_wsierp_1),interesting(0.70)]). fof(l18_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k3_int_2(A,B) = k6_nat_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d3_int_2,l13_wsierp_1,l13_wsierp_1]), [file(wsierp_1,l18_wsierp_1),interesting(0.70)]). fof(l19_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_int_2(A,B) <=> r1_int_2(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_int_2,l18_wsierp_1,d4_int_2]), [file(wsierp_1,l19_wsierp_1),interesting(0.70)]). fof(t7_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(C,B) ) => ( r1_xreal_0(C,k6_xcmplx_0(B,A)) & r1_xreal_0(k2_xcmplx_0(C,A),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_xreal_1,t54_xreal_1]), [file(wsierp_1,t7_wsierp_1),interesting(0.70)]). fof(l40_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( r2_hidden(A,k1_relat_1(B)) & r2_hidden(k1_funct_1(B,A),k2_relat_1(B)) ) | k1_funct_1(B,A) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,d4_funct_1]), [file(wsierp_1,l40_wsierp_1),interesting(0.69)]). fof(t20_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_nat_1(A,1) => A = 1 ) ) ), inference(mizar_proof,[status(thm)],[t55_nat_1,t52_newton]), [file(wsierp_1,t20_wsierp_1),interesting(0.69)]). fof(t23_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(A,k5_real_1(B,C)) => ( r1_xreal_0(A,B) & r1_xreal_0(C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_xreal_1,l36_wsierp_1]), [file(wsierp_1,t23_wsierp_1),interesting(0.68)]). fof(l14_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( A != k2_nat_1(2,B) & A != k1_nat_1(k2_nat_1(2,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_nat_1,t46_nat_1,t71_nat_1]), [file(wsierp_1,l14_wsierp_1),interesting(0.68)]). fof(t16_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( v1_int_1(C) => ! [D] : ( v1_int_1(D) => ( r1_int_2(C,D) => r1_int_2(k2_newton(C,A),k2_newton(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_wsierp_1,t15_wsierp_1]), [file(wsierp_1,t16_wsierp_1),interesting(0.66)]). fof(t19_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_nat_1(A,B) => r1_nat_1(k2_wsierp_1(A,C),k2_wsierp_1(B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_nat_1,t12_newton,d3_nat_1]), [file(wsierp_1,t19_wsierp_1),interesting(0.65)]). fof(t11_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( k3_int_2(A,B) = 1 & k3_int_2(C,B) = 1 ) => k3_int_2(k3_xcmplx_0(A,C),B) = 1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_int_2,t41_int_2,d4_int_2]), [file(wsierp_1,t11_wsierp_1),interesting(0.64)]). fof(l41_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( r2_hidden(0,B) => ! [C] : ( m2_finseq_1(C,B) => m1_subset_1(k1_funct_1(C,A),B) ) ) ) ), inference(mizar_proof,[status(thm)],[l40_wsierp_1,d4_finseq_1]), [file(wsierp_1,l41_wsierp_1),interesting(0.63)]). fof(l51_wsierp_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( r1_xreal_0(1,k3_finseq_1(A)) => ( A = k7_finseq_1(k9_finseq_1(k1_funct_1(A,1)),k2_finseq_3(1,A)) & A = k7_finseq_1(k2_finseq_3(k3_finseq_1(A),A),k9_finseq_1(k1_funct_1(A,k3_finseq_1(A)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t56_finseq_1,t27_finseq_3,t27_finseq_3,d1_wsierp_1,d1_wsierp_1,t35_finseq_1,d1_wsierp_1,t35_finseq_1,t27_finseq_3,d7_finseq_1,t57_finseq_1,t52_xreal_1,t16_int_1,t39_nat_1,t37_finseq_1,d1_wsierp_1,t1_xreal_1,t18_finseq_1,t148_xreal_1,t37_finseq_1,t57_finseq_1,t38_nat_1,t21_xreal_1,t27_finseq_3,d7_finseq_1,d1_wsierp_1,t1_xreal_1,t18_finseq_1]), [file(wsierp_1,l51_wsierp_1),interesting(0.63)]). fof(t28_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_trees_4(B,k1_numbers,k5_numbers) => ( r2_hidden(A,k4_finseq_1(B)) => m2_subset_1(k6_real_1(k10_wsierp_1(B),k3_wsierp_1(B,A)),k1_numbers,k5_numbers) ) ) ) ), inference(mizar_proof,[status(thm)],[l42_wsierp_1,t50_finseq_1,t50_finseq_1,t50_finseq_1,t127_rvsum_1,t126_rvsum_1,t90_xcmplx_1,d9_xcmplx_0,d7_xcmplx_0]), [file(wsierp_1,t28_wsierp_1),interesting(0.63)]). fof(l46_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( r1_xreal_0(A,k3_finseq_1(B)) => k2_finseq_3(A,k7_finseq_1(B,C)) = k7_finseq_1(k2_finseq_3(A,B),C) ) & ( r1_xreal_0(1,A) => k2_finseq_3(k1_nat_1(k3_finseq_1(B),A),k7_finseq_1(B,C)) = k7_finseq_1(B,k2_finseq_3(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_finseq_1,t29_nat_1,t2_xreal_1,t27_finseq_3,d1_wsierp_1,d1_wsierp_1,t27_finseq_3,l42_wsierp_1,t19_finseq_2,t64_finseq_1,l44_wsierp_1,t45_finseq_1,t46_finseq_1,l44_wsierp_1,t45_finseq_1,t27_finseq_3,t8_xreal_1,t27_finseq_3,d1_wsierp_1,d1_wsierp_1,t27_finseq_3,t8_xreal_1,t37_nat_1,t27_finseq_3,l42_wsierp_1,l44_wsierp_1,t45_finseq_1,t50_xreal_1,l7_wsierp_1,t64_finseq_1,t45_finseq_1,t45_finseq_1,t46_finseq_1,t35_finseq_1,l44_wsierp_1,t45_finseq_1]), [file(wsierp_1,l46_wsierp_1),interesting(0.62)]). fof(t43_wsierp_1,theorem,( ! [A] : ( m1_trees_4(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(A)) => k6_nat_1(k3_wsierp_1(A,C),B) = 1 ) ) => k6_nat_1(k10_wsierp_1(A),B) = 1 ) ) ) ), inference(mizar_proof,[status(thm)],[t64_newton,t124_rvsum_1,t39_finseq_1,d7_finseq_1,t19_finseq_2,t6_finseq_5,t59_finseq_1,t126_rvsum_1,t12_wsierp_1,s2_finseq_2]), [file(wsierp_1,t43_wsierp_1),interesting(0.61)]). fof(l34_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( v1_int_1(C) => ( k3_xcmplx_0(B,C) = A => ( A = 0 | m2_subset_1(C,k1_numbers,k5_numbers) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_int_1,l12_wsierp_1,t90_xcmplx_1,l32_wsierp_1]), [file(wsierp_1,l34_wsierp_1),interesting(0.60)]). fof(t47_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => r1_tarski(k4_finseq_1(k2_finseq_3(A,B)),k4_finseq_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[l45_wsierp_1]), [file(wsierp_1,t47_wsierp_1),interesting(0.58)]). fof(t3_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k2_newton(k4_xcmplx_0(A),k2_nat_1(2,B)) = k2_newton(A,k2_nat_1(2,B)) & k2_newton(k4_xcmplx_0(A),k1_nat_1(k2_nat_1(2,B),1)) = k4_xcmplx_0(k2_newton(A,k1_nat_1(k2_nat_1(2,B),1))) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_newton,t2_wsierp_1,t14_newton,t11_newton,t11_newton]), [file(wsierp_1,t3_wsierp_1),interesting(0.52)]). fof(t30_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_rat_1(C) => ( ( C = k7_xcmplx_0(B,A) & r1_int_2(B,A) ) => ( C = 0 | A = 0 | ( B = k2_rat_1(C) & A = k1_rat_1(C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_rat_1,t29_wsierp_1,t39_int_2,d4_int_2,l13_wsierp_1]), [file(wsierp_1,t30_wsierp_1),interesting(0.51)]). fof(l44_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ! [E] : ( ( r2_hidden(A,k4_finseq_1(B)) & B = k7_finseq_1(k7_finseq_1(C,k9_finseq_1(E)),D) & k3_finseq_1(C) = k5_real_1(A,1) ) => k2_finseq_3(A,B) = k7_finseq_1(C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_finseq_1,t19_finseq_2,t45_finseq_1,t56_finseq_1,t35_finseq_1,d1_wsierp_1,t35_finseq_1,l38_wsierp_1,t27_finseq_3,d7_finseq_1,d7_finseq_1,d1_wsierp_1,l38_wsierp_1,t21_xreal_1,t52_xreal_1,t8_xreal_1,t148_xreal_1,t2_xreal_1,t52_xreal_1,t16_int_1,t8_xreal_1,t11_xreal_1,t37_finseq_1,t37_finseq_1,t37_finseq_1,d1_wsierp_1,t18_finseq_1]), [file(wsierp_1,l44_wsierp_1),interesting(0.44)]). fof(l42_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( r2_hidden(A,k4_finseq_1(B)) & ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ~ ( B = k7_finseq_1(k7_finseq_1(C,k9_finseq_1(k1_funct_1(B,A))),D) & k3_finseq_1(C) = k5_real_1(A,1) & k3_finseq_1(D) = k5_real_1(k3_finseq_1(B),A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseq_3,t18_int_1,t25_finseq_2,t27_finseq_3,t25_finseq_1,t6_finseq_5,d7_finseq_1,t21_finseq_2,t19_finseq_2,t59_finseq_1]), [file(wsierp_1,l42_wsierp_1),interesting(0.37)]). fof(t46_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ~ ( A != 0 & k3_int_2(A,B) = 1 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( 0 != C & 0 != D & r1_xreal_0(C,k9_square_1(A)) & r1_xreal_0(D,k9_square_1(A)) & ( r2_int_1(A,k2_xcmplx_0(k3_xcmplx_0(B,C),D)) | r2_int_1(A,k6_xcmplx_0(k3_xcmplx_0(B,C),D)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_nat_1,t83_square_1,t16_int_2,l77_wsierp_1,t93_square_1,d4_int_1,t2_xreal_1,t83_square_1,t95_square_1,t52_xreal_1,t16_int_1,l7_wsierp_1,l7_wsierp_1,t21_xreal_1,t78_square_1,d4_square_1,s2_finseq_1,d3_finseq_1,d3_tarski,t11_finseq_2,d3_finseq_1,t78_newton,l7_wsierp_1,l35_wsierp_1,t79_newton,l39_wsierp_1,t7_finseq_1,t1_xboole_1,t7_finseq_1,t74_finseq_4,d8_funct_1,t27_finseq_3,t80_newton,t80_newton,t79_newton,t78_newton,l9_wsierp_1,l39_wsierp_1,l9_wsierp_1,l39_wsierp_1,t26_xreal_1,t12_absvalue,t2_xreal_1,d7_int_1,d4_int_1,t11_xreal_1,t73_real_1,t128_xcmplx_1,t127_real_2,l7_wsierp_1,t2_xreal_1,t2_xreal_1,l39_wsierp_1,t47_int_1,t50_xreal_1,t125_real_2,t11_pre_ff,l8_wsierp_1,t26_xreal_1,t12_absvalue,t2_xreal_1,t2_xcmplx_1,l75_wsierp_1,l76_wsierp_1,l73_wsierp_1,l71_wsierp_1,t7_absvalue,t36_wsierp_1,l73_wsierp_1,l71_wsierp_1,t7_absvalue,t7_absvalue,t2_xreal_1,t2_xreal_1,t1_absvalue,t14_int_2,d5_real_1]), [file(wsierp_1,t46_wsierp_1),interesting(0.33)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(d4_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> r2_hidden(k4_tarski(B,C),A) ) ) & ( ~ r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> C = k1_xboole_0 ) ) ) ) ), file(funct_1,d4_funct_1), [interesting(0.00)]). fof(d4_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( m1_finseq_1(B,A) <=> r1_tarski(k2_relat_1(B),A) ) ) ), file(finseq_1,d4_finseq_1), [interesting(0.00)]). fof(d9_int_1,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r2_int_1(A,B) <=> ? [C] : ( v1_int_1(C) & B = k3_xcmplx_0(A,C) ) ) ) ) ), file(int_1,d9_int_1), [interesting(0.00)]). fof(d1_absvalue,definition,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) => k16_complex1(A) = A ) & ( ~ r1_xreal_0(0,A) => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ), file(absvalue,d1_absvalue), [interesting(0.00)]). fof(t1_wsierp_1,theorem,( $true ), file(wsierp_1,t1_wsierp_1), [interesting(0.00)]). fof(t90_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => B = k7_xcmplx_0(k3_xcmplx_0(B,A),A) ) ) ) ), file(xcmplx_1,t90_xcmplx_1), [interesting(0.00)]). fof(t88_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ), file(xcmplx_1,t88_xcmplx_1), [interesting(0.00)]). fof(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(t24_wsierp_1,theorem,( $true ), file(wsierp_1,t24_wsierp_1), [interesting(0.00)]). fof(t25_wsierp_1,theorem,( $true ), file(wsierp_1,t25_wsierp_1), [interesting(0.00)]). fof(t47_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k7_finseq_1(A,k1_xboole_0) = A & k7_finseq_1(k1_xboole_0,A) = A ) ) ), file(finseq_1,t47_finseq_1), [interesting(0.00)]). fof(t56_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t56_finseq_1), [interesting(0.00)]). fof(t27_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(B,k4_finseq_1(A)) <=> ( r1_xreal_0(1,B) & r1_xreal_0(B,k3_finseq_1(A)) ) ) ) ) ), file(finseq_3,t27_finseq_3), [interesting(0.00)]). fof(d1_wsierp_1,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( ~ r2_hidden(A,k4_finseq_1(B)) => ( C = k2_finseq_3(A,B) <=> C = B ) ) & ( r2_hidden(A,k4_finseq_1(B)) => ( C = k2_finseq_3(A,B) <=> ( k1_nat_1(k3_finseq_1(C),1) = k3_finseq_1(B) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( ~ r1_xreal_0(A,D) => k1_funct_1(C,D) = k1_funct_1(B,D) ) & ( r1_xreal_0(A,D) => k1_funct_1(C,D) = k1_funct_1(B,k1_nat_1(D,1)) ) ) ) ) ) ) ) ) ) ) ), file(wsierp_1,d1_wsierp_1), [interesting(0.00)]). fof(t25_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k3_finseq_1(A) = 0 <=> A = k1_xboole_0 ) ) ), file(finseq_1,t25_finseq_1), [interesting(0.00)]). fof(t35_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ), file(finseq_1,t35_finseq_1), [interesting(0.00)]). fof(t18_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(A,B) => r2_hidden(k6_xcmplx_0(B,A),k5_numbers) ) ) ) ), file(int_1,t18_int_1), [interesting(0.00)]). fof(t25_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ~ ( k3_finseq_1(C) = k1_nat_1(A,B) & ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) & v1_finseq_1(E) ) => ~ ( k3_finseq_1(D) = A & k3_finseq_1(E) = B & C = k7_finseq_1(D,E) ) ) ) ) ) ) ) ), file(finseq_2,t25_finseq_2), [interesting(0.00)]). fof(t6_finseq_5,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( r2_hidden(1,k4_finseq_1(A)) & r2_hidden(k3_finseq_1(A),k4_finseq_1(A)) ) ) ), file(finseq_5,t6_finseq_5), [interesting(0.00)]). fof(d7_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k7_finseq_1(A,B) <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ), file(finseq_1,d7_finseq_1), [interesting(0.00)]). fof(t21_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( k3_finseq_1(B) = k1_nat_1(A,1) & ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : B != k7_finseq_1(C,k9_finseq_1(D)) ) ) ) ) ), file(finseq_2,t21_finseq_2), [interesting(0.00)]). fof(t19_finseq_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(B,k9_finseq_1(A))) = k1_nat_1(k3_finseq_1(B),1) ) ), file(finseq_2,t19_finseq_2), [interesting(0.00)]). fof(t59_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k1_funct_1(k7_finseq_1(B,k9_finseq_1(A)),k1_nat_1(k3_finseq_1(B),1)) = A ) ), file(finseq_1,t59_finseq_1), [interesting(0.00)]). fof(t64_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ~ ( k7_finseq_1(A,B) = k7_finseq_1(C,D) & r1_xreal_0(k3_finseq_1(A),k3_finseq_1(C)) & ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) & v1_finseq_1(E) ) => k7_finseq_1(A,E) != C ) ) ) ) ) ) ), file(finseq_1,t64_finseq_1), [interesting(0.00)]). fof(t45_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ), file(finseq_1,t45_finseq_1), [interesting(0.00)]). fof(t20_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ~ r1_xreal_0(B,A) => r1_xreal_0(k2_xcmplx_0(A,1),B) ) ) ) ), file(int_1,t20_int_1), [interesting(0.00)]). fof(t31_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ), file(xreal_1,t31_xreal_1), [interesting(0.00)]). fof(t52_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ), file(xreal_1,t52_xreal_1), [interesting(0.00)]). fof(t8_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(t148_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ r1_xreal_0(A,k6_xcmplx_0(A,1)) ) ), file(xreal_1,t148_xreal_1), [interesting(0.00)]). fof(t16_int_1,theorem,( ! [A] : ( v1_int_1(A) => ( r1_xreal_0(0,A) => r2_hidden(A,k5_numbers) ) ) ), file(int_1,t16_int_1), [interesting(0.00)]). fof(t11_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). fof(t37_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(C,k3_finseq_1(k7_finseq_1(A,B))) => ( r1_xreal_0(C,k3_finseq_1(A)) | k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ) ), file(finseq_1,t37_finseq_1), [interesting(0.00)]). fof(t18_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( ( k3_finseq_1(A) = k3_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(A)) ) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t18_finseq_1), [interesting(0.00)]). fof(t46_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( k7_finseq_1(A,B) = k7_finseq_1(C,B) | k7_finseq_1(B,A) = k7_finseq_1(B,C) ) => A = C ) ) ) ) ), file(finseq_1,t46_finseq_1), [interesting(0.00)]). fof(t37_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(A,B) => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) ) ) ), file(nat_1,t37_nat_1), [interesting(0.00)]). fof(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_xreal_1), [interesting(0.00)]). fof(t22_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k2_xcmplx_0(B,C)) <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ), file(xreal_1,t22_xreal_1), [interesting(0.00)]). fof(l7_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) => r1_xreal_0(B,k2_xcmplx_0(A,B)) ) & ( r1_xreal_0(B,k2_xcmplx_0(A,B)) => r1_xreal_0(0,A) ) & ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k2_xcmplx_0(A,B),B) ) & ~ ( ~ r1_xreal_0(k2_xcmplx_0(A,B),B) & r1_xreal_0(A,0) ) & ( r1_xreal_0(0,A) => r1_xreal_0(k6_xcmplx_0(B,A),B) ) & ( r1_xreal_0(k6_xcmplx_0(B,A),B) => r1_xreal_0(0,A) ) & ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(B,k6_xcmplx_0(B,A)) ) & ~ ( ~ r1_xreal_0(B,k6_xcmplx_0(B,A)) & r1_xreal_0(A,0) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_xreal_1,t8_xreal_1,t22_xreal_1,t21_xreal_1]), [file(wsierp_1,l7_wsierp_1),interesting(0.00)]). fof(t60_finseq_1,theorem,( ! [A,B,C] : ( k11_finseq_1(A,B,C) = k7_finseq_1(k9_finseq_1(A),k10_finseq_1(B,C)) & k11_finseq_1(A,B,C) = k7_finseq_1(k10_finseq_1(A,B),k9_finseq_1(C)) ) ), file(finseq_1,t60_finseq_1), [interesting(0.00)]). fof(t61_finseq_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k10_finseq_1(A,B) <=> ( k3_finseq_1(C) = 2 & k1_funct_1(C,1) = A & k1_funct_1(C,2) = B ) ) ) ), file(finseq_1,t61_finseq_1), [interesting(0.00)]). fof(t57_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,t57_finseq_1), [interesting(0.00)]). fof(t39_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(1,A) => A = 0 ) ) ), file(nat_1,t39_nat_1), [interesting(0.00)]). fof(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [interesting(0.00)]). fof(t38_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), file(nat_1,t38_nat_1), [interesting(0.00)]). fof(t105_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,A,B)) = k9_binop_2(k15_rvsum_1(A),k15_rvsum_1(B)) ) ) ), file(rvsum_1,t105_rvsum_1), [interesting(0.00)]). fof(t103_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k15_rvsum_1(k12_finseq_1(k1_numbers,A)) = A ) ), file(rvsum_1,t103_rvsum_1), [interesting(0.00)]). fof(t50_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( m2_finseq_1(k7_finseq_1(A,B),C) => ( m2_finseq_1(A,C) & m2_finseq_1(B,C) ) ) ) ) ), file(finseq_1,t50_finseq_1), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(t127_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k16_rvsum_1(k8_finseq_1(k1_numbers,A,B)) = k11_binop_2(k16_rvsum_1(A),k16_rvsum_1(B)) ) ) ), file(rvsum_1,t127_rvsum_1), [interesting(0.00)]). fof(t126_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k16_rvsum_1(k8_finseq_1(k1_numbers,B,k12_finseq_1(k1_numbers,A))) = k11_binop_2(k16_rvsum_1(B),A) ) ) ), file(rvsum_1,t126_rvsum_1), [interesting(0.00)]). fof(d9_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ), file(xcmplx_0,d9_xcmplx_0), [interesting(0.00)]). fof(d7_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( ( A != 0 => ( B = k5_xcmplx_0(A) <=> k3_xcmplx_0(A,B) = 1 ) ) & ( A = 0 => ( B = k5_xcmplx_0(A) <=> B = 0 ) ) ) ) ) ), file(xcmplx_0,d7_xcmplx_0), [interesting(0.00)]). fof(t60_rat_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_rat_1(C) => ~ ( A != 0 & C = k7_xcmplx_0(B,A) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( B = k3_xcmplx_0(k2_rat_1(C),D) & A = k2_nat_1(k1_rat_1(C),D) ) ) ) ) ) ) ), file(rat_1,t60_rat_1), [interesting(0.00)]). fof(d3_rat_1,definition,( ! [A] : ( v1_rat_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k1_rat_1(A) <=> ( B != 0 & ? [C] : ( v1_int_1(C) & A = k7_xcmplx_0(C,B) ) & ! [C] : ( v1_int_1(C) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( A = k7_xcmplx_0(C,D) => ( D = 0 | r1_xreal_0(B,D) ) ) ) ) ) ) ) ) ), file(rat_1,d3_rat_1), [interesting(0.00)]). fof(t29_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => m2_subset_1(k3_int_2(A,B),k1_numbers,k5_numbers) ) ) ), file(int_2,t29_int_2), [interesting(0.00)]). fof(d4_int_2,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_int_2(A,B) <=> k3_int_2(A,B) = 1 ) ) ) ), file(int_2,d4_int_2), [interesting(0.00)]). fof(t35_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ( A = 0 & B = 0 ) <=> k3_int_2(A,B) = 0 ) ) ) ), file(int_2,t35_int_2), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t31_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => r2_int_1(k3_int_2(A,B),A) ) ) ), file(int_2,t31_int_2), [interesting(0.00)]). fof(t32_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => r2_int_1(k3_int_2(A,B),B) ) ) ), file(int_2,t32_int_2), [interesting(0.00)]). fof(d3_nat_1,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_nat_1(A,B) <=> ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & B = k3_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,d3_nat_1), [interesting(0.00)]). fof(t133_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,0) ) => r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t133_xreal_1), [interesting(0.00)]). fof(t53_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( r1_nat_1(A,0) & r1_nat_1(1,A) ) ) ), file(nat_1,t53_nat_1), [interesting(0.00)]). fof(t62_rat_1,theorem,( ! [A] : ( v1_rat_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(B,1) & ? [C] : ( v1_int_1(C) & ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & k2_rat_1(A) = k3_xcmplx_0(C,B) & k1_rat_1(A) = k2_nat_1(D,B) ) ) ) ) ) ), file(rat_1,t62_rat_1), [interesting(0.00)]). fof(t39_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( r1_int_2(A,B) => ( k3_int_2(k3_xcmplx_0(C,A),k3_xcmplx_0(C,B)) = k1_int_2(C) & k3_int_2(k3_xcmplx_0(C,A),k3_xcmplx_0(B,C)) = k1_int_2(C) & k3_int_2(k3_xcmplx_0(A,C),k3_xcmplx_0(C,B)) = k1_int_2(C) & k3_int_2(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) = k1_int_2(C) ) ) ) ) ) ), file(int_2,t39_int_2), [interesting(0.00)]). fof(t16_newton,theorem,( ! [A] : ( v4_ordinal2(A) => ( r1_xreal_0(1,A) => k3_newton(0,A) = 0 ) ) ), file(newton,t16_newton), [interesting(0.00)]). fof(t51_card_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ( ~ ( ~ ( B = 0 & A != 0 ) & k3_newton(B,A) = 0 ) & ~ ( k3_newton(B,A) != 0 & B = 0 & A != 0 ) ) ) ) ), file(card_4,t51_card_4), [interesting(0.00)]). fof(t15_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v4_ordinal2(C) => k2_newton(k7_xcmplx_0(A,B),C) = k7_xcmplx_0(k2_newton(A,C),k2_newton(B,C)) ) ) ) ), file(prepower,t15_prepower), [interesting(0.00)]). fof(t9_newton,theorem,( ! [A] : ( v1_xreal_0(A) => k2_newton(A,0) = 1 ) ), file(newton,t9_newton), [interesting(0.00)]). fof(t37_rat_1,theorem,( ! [A] : ( v1_rat_1(A) => ( A = k7_xcmplx_0(k2_rat_1(A),k1_rat_1(A)) & A = k3_xcmplx_0(k2_rat_1(A),k2_real_1(k1_rat_1(A))) & A = k3_xcmplx_0(k2_real_1(k1_rat_1(A)),k2_rat_1(A)) ) ) ), file(rat_1,t37_rat_1), [interesting(0.00)]). fof(d3_int_2,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => k3_int_2(A,B) = k6_nat_1(k1_int_2(A),k1_int_2(B)) ) ) ), file(int_2,d3_int_2), [interesting(0.00)]). fof(t7_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ( A = 0 <=> k18_complex1(A) = 0 ) ) ), file(absvalue,t7_absvalue), [interesting(0.00)]). fof(t65_newton,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k6_nat_1(A,0) = A ) ), file(newton,t65_newton), [interesting(0.00)]). fof(t64_newton,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k6_nat_1(A,1) = 1 ) ), file(newton,t64_newton), [interesting(0.00)]). fof(t41_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( r1_int_2(A,B) & r1_int_2(C,B) ) => r1_int_2(k3_xcmplx_0(A,C),B) ) ) ) ) ), file(int_2,t41_int_2), [interesting(0.00)]). fof(t11_newton,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_xreal_0(B) => k2_newton(B,k2_xcmplx_0(A,1)) = k3_xcmplx_0(k2_newton(B,A),B) ) ) ), file(newton,t11_newton), [interesting(0.00)]). fof(t22_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(B,1) ) ) ) ), file(nat_1,t22_nat_1), [interesting(0.00)]). fof(t33_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( r2_int_1(C,A) & r2_int_1(C,B) ) => r2_int_1(C,k3_int_2(A,B)) ) ) ) ) ), file(int_2,t33_int_2), [interesting(0.00)]). fof(t17_int_2,theorem,( ! [A] : ( v1_int_1(A) => ~ ( ( r2_int_1(A,1) | r2_int_1(A,k1_real_1(1)) ) & A != 1 & A != k1_real_1(1) ) ) ), file(int_2,t17_int_2), [interesting(0.00)]). fof(t9_int_2,theorem,( ~ m2_subset_1(k1_real_1(1),k1_numbers,k5_numbers) ), file(int_2,t9_int_2), [interesting(0.00)]). fof(t8_int_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( v1_int_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( A != B & A != k1_real_1(B) ) ) ) ) ), file(int_1,t8_int_1), [interesting(0.00)]). fof(t47_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,0) => B = k2_xcmplx_0(k3_xcmplx_0(A,k3_nat_1(B,A)),k4_nat_1(B,A)) ) ) ) ), file(nat_1,t47_nat_1), [interesting(0.00)]). fof(t46_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k4_nat_1(B,A)) ) ) ) ), file(nat_1,t46_nat_1), [interesting(0.00)]). fof(t71_nat_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(2,A) & A != 0 & A != 1 ) ) ), file(nat_1,t71_nat_1), [interesting(0.00)]). fof(t14_newton,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v1_xreal_0(C) => k2_newton(k2_newton(C,A),B) = k2_newton(C,k3_xcmplx_0(A,B)) ) ) ) ), file(newton,t14_newton), [interesting(0.00)]). fof(t10_newton,theorem,( ! [A] : ( v1_xreal_0(A) => k2_newton(A,1) = A ) ), file(newton,t10_newton), [interesting(0.00)]). fof(t13_newton,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v1_xreal_0(C) => k2_newton(C,k2_xcmplx_0(A,B)) = k3_xcmplx_0(k2_newton(C,A),k2_newton(C,B)) ) ) ) ), file(newton,t13_newton), [interesting(0.00)]). fof(t8_int_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( m2_subset_1(k1_real_1(A),k1_numbers,k5_numbers) <=> A = 0 ) ) ), file(int_2,t8_int_2), [interesting(0.00)]). fof(t12_newton,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k2_newton(k3_xcmplx_0(B,C),A) = k3_xcmplx_0(k2_newton(B,A),k2_newton(C,A)) ) ) ) ), file(newton,t12_newton), [interesting(0.00)]). fof(t28_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ( r1_xreal_0(0,A) & r1_xreal_0(1,B) ) => ( k2_newton(k4_prepower(B,A),B) = A & k4_prepower(B,k2_newton(A,B)) = A ) ) ) ) ), file(prepower,t28_prepower), [interesting(0.00)]). fof(t5_wsierp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) & k2_newton(A,C) = k2_newton(B,C) ) => ( r1_xreal_0(C,0) | A = B ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_nat_1,t28_prepower,t28_prepower]), [file(wsierp_1,t5_wsierp_1),interesting(0.00)]). fof(l15_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( k2_wsierp_1(B,A) = k2_wsierp_1(C,A) => ( r1_xreal_0(A,0) | B = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_wsierp_1]), [file(wsierp_1,l15_wsierp_1),interesting(0.00)]). fof(s5_nat_1,theorem, ( ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s5_nat_1(A) ) => ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s5_nat_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( p1_s5_nat_1(B) => r1_xreal_0(A,B) ) ) ) ), file(nat_1,s5_nat_1), [interesting(0.00)]). fof(t42_nat_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(A,0) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & B = k1_nat_1(k2_nat_1(A,C),D) & ~ r1_xreal_0(A,D) ) ) ) ) ) ), file(nat_1,t42_nat_1), [interesting(0.00)]). fof(d5_nat_1,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k6_nat_1(A,B) <=> ( r1_nat_1(C,A) & r1_nat_1(C,B) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r1_nat_1(D,A) & r1_nat_1(D,B) ) => r1_nat_1(D,C) ) ) ) ) ) ) ) ), file(nat_1,d5_nat_1), [interesting(0.00)]). fof(t12_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( r2_int_1(A,B) => r2_int_1(A,k3_xcmplx_0(B,C)) ) ) ) ) ), file(int_2,t12_int_2), [interesting(0.00)]). fof(t52_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ( r1_nat_1(A,B) & r1_nat_1(B,A) ) => A = B ) ) ) ), file(nat_1,t52_nat_1), [interesting(0.00)]). fof(t57_int_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ r1_xreal_0(k2_int_1(A),k6_xcmplx_0(A,1)) & ~ r1_xreal_0(k2_xcmplx_0(k2_int_1(A),1),A) ) ) ), file(int_1,t57_int_1), [interesting(0.00)]). fof(t50_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,B) ) <=> r1_xreal_0(k2_square_1(A,C),B) ) ) ) ) ), file(square_1,t50_square_1), [interesting(0.00)]). fof(t49_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( k2_square_1(A,B) = A | k2_square_1(A,B) = B ) ) ) ), file(square_1,t49_square_1), [interesting(0.00)]). fof(t188_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k4_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k4_xcmplx_0(A),B) ) ) ), file(xcmplx_1,t188_xcmplx_1), [interesting(0.00)]). fof(t177_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(k3_xcmplx_0(B,A),C) => ( r1_xreal_0(A,0) | r1_xreal_0(B,k7_xcmplx_0(C,A)) ) ) & ( r1_xreal_0(k3_xcmplx_0(B,A),C) => ( r1_xreal_0(0,A) | r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) & ( r1_xreal_0(C,k3_xcmplx_0(B,A)) => ( r1_xreal_0(A,0) | r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) & ( r1_xreal_0(C,k3_xcmplx_0(B,A)) => ( r1_xreal_0(0,A) | r1_xreal_0(B,k7_xcmplx_0(C,A)) ) ) ) ) ) ) ), file(real_2,t177_real_2), [interesting(0.00)]). fof(t38_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( A != 0 & B != 0 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k6_nat_1(A,B) != k5_real_1(k2_nat_1(A,C),k2_nat_1(B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_wsierp_1,t57_int_1,t6_wsierp_1,t188_xcmplx_1,t177_real_2,t52_xreal_1,t16_int_1]), [file(wsierp_1,t38_wsierp_1),interesting(0.00)]). fof(t45_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => k6_prepower(A,1) = A ) ), file(prepower,t45_prepower), [interesting(0.00)]). fof(t53_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( A != 0 => k6_prepower(A,k6_xcmplx_0(B,C)) = k7_xcmplx_0(k2_newton(A,B),k2_newton(A,C)) ) ) ) ) ), file(prepower,t53_prepower), [interesting(0.00)]). fof(t39_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & k6_nat_1(A,B) = 1 & k2_wsierp_1(C,A) = k2_wsierp_1(D,B) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ~ ( C = k2_wsierp_1(E,B) & D = k2_wsierp_1(E,A) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_nat_1,t16_newton,t51_card_4,t16_newton,t51_card_4,t38_wsierp_1,t45_prepower,t53_prepower,t14_newton,t14_newton,t14_newton,t14_newton,t15_prepower,t32_wsierp_1,t14_newton,t14_newton,l15_wsierp_1]), [file(wsierp_1,t39_wsierp_1),interesting(0.00)]). fof(t38_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ~ ( ~ ( A = 0 & B = 0 ) & ! [C] : ( v1_int_1(C) => ! [D] : ( v1_int_1(D) => ~ ( A = k3_xcmplx_0(k3_int_2(A,B),C) & B = k3_xcmplx_0(k3_int_2(A,B),D) & r1_int_2(C,D) ) ) ) ) ) ) ), file(int_2,t38_int_2), [interesting(0.00)]). fof(t75_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t75_xcmplx_1), [interesting(0.00)]). fof(t95_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => ( k3_xcmplx_0(C,A) = k3_xcmplx_0(D,B) => ( A = 0 | B = 0 | k7_xcmplx_0(C,B) = k7_xcmplx_0(D,A) ) ) ) ) ) ) ), file(xcmplx_1,t95_xcmplx_1), [interesting(0.00)]). fof(t41_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ! [D] : ( v1_int_1(D) => ! [E] : ( v1_int_1(E) => ( k2_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) = E => ( A = 0 | B = 0 | ! [F] : ( v1_int_1(F) => ! [G] : ( v1_int_1(G) => ~ ( k2_xcmplx_0(k3_xcmplx_0(A,F),k3_xcmplx_0(B,G)) = E & ! [H] : ( v1_int_1(H) => ~ ( F = k2_xcmplx_0(C,k3_xcmplx_0(H,k7_xcmplx_0(B,k3_int_2(A,B)))) & G = k6_xcmplx_0(D,k3_xcmplx_0(H,k7_xcmplx_0(A,k3_int_2(A,B)))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_int_2,t38_int_2,t90_xcmplx_1,d4_int_2,t75_xcmplx_1,t75_xcmplx_1,t95_xcmplx_1,d9_int_1,t36_wsierp_1,d9_int_1,t90_xcmplx_1,t88_xcmplx_1]), [file(wsierp_1,t41_wsierp_1),interesting(0.00)]). fof(t70_newton,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_nat_1(A,B) => r1_nat_1(k6_nat_1(C,A),k6_nat_1(C,B)) ) ) ) ) ), file(newton,t70_newton), [interesting(0.00)]). fof(t55_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( ( r1_nat_1(A,B) & r1_nat_1(A,C) ) => r1_nat_1(A,k2_xcmplx_0(B,C)) ) ) ) ) ), file(nat_1,t55_nat_1), [interesting(0.00)]). fof(t52_newton,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ( r1_nat_1(B,A) & r1_nat_1(B,k1_nat_1(A,1)) ) <=> B = 1 ) ) ) ), file(newton,t52_newton), [interesting(0.00)]). fof(t21_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_nat_1(A,B) & k6_nat_1(B,C) = 1 ) => k6_nat_1(A,C) = 1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t70_newton,t20_wsierp_1]), [file(wsierp_1,t21_wsierp_1),interesting(0.00)]). fof(t17_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( v1_int_1(C) => ! [D] : ( v1_int_1(D) => ( k3_int_2(C,D) = 1 => ( k3_int_2(C,k2_newton(D,A)) = 1 & k3_int_2(k2_newton(C,B),k2_newton(D,A)) = 1 ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_int_2,t15_wsierp_1,t16_wsierp_1,d4_int_2]), [file(wsierp_1,t17_wsierp_1),interesting(0.00)]). fof(l27_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( k6_nat_1(A,B) = 1 => ( k6_nat_1(A,k2_wsierp_1(B,C)) = 1 & k6_nat_1(k2_wsierp_1(A,D),k2_wsierp_1(B,C)) = 1 ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_wsierp_1,t17_wsierp_1,l18_wsierp_1]), [file(wsierp_1,l27_wsierp_1),interesting(0.00)]). fof(t37_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( k6_nat_1(A,B) = 1 & r1_nat_1(A,k2_nat_1(B,C)) ) => r1_nat_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_wsierp_1,l12_wsierp_1,t36_wsierp_1,l12_wsierp_1]), [file(wsierp_1,t37_wsierp_1),interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(t5_int_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ( A = 0 & B = 0 ) <=> k6_nat_1(A,B) = 0 ) ) ) ), file(int_2,t5_int_2), [interesting(0.00)]). fof(t15_newton,theorem,( ! [A] : ( v4_ordinal2(A) => k3_newton(1,A) = 1 ) ), file(newton,t15_newton), [interesting(0.00)]). fof(t6_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( k3_xcmplx_0(A,B) = 0 & A != 0 & B != 0 ) ) ) ), file(xcmplx_1,t6_xcmplx_1), [interesting(0.00)]). fof(d6_int_2,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_int_2(A,B) <=> k6_nat_1(A,B) = 1 ) ) ) ), file(int_2,d6_int_2), [interesting(0.00)]). fof(t62_newton,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_nat_1(A,B) => k6_nat_1(A,B) = A ) ) ) ), file(newton,t62_newton), [interesting(0.00)]). fof(t42_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( k6_nat_1(A,B) = 1 & k2_nat_1(A,B) = k2_wsierp_1(C,D) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ~ ( A = k2_wsierp_1(E,D) & B = k2_wsierp_1(F,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_wsierp_1,d5_nat_1,t19_wsierp_1,t21_wsierp_1,l27_wsierp_1,t37_wsierp_1,d3_nat_1,t9_newton,d3_nat_1,t20_wsierp_1,t9_newton,t39_nat_1,t28_nat_1,t5_int_2,t65_newton,t15_newton,t16_newton,t51_card_4,t16_newton,t6_xcmplx_1,t65_newton,t15_newton,t16_newton,t51_card_4,t38_int_2,l34_wsierp_1,t90_xcmplx_1,l19_wsierp_1,d6_int_2,t90_xcmplx_1,t11_newton,t90_xcmplx_1,d3_nat_1,t21_wsierp_1,l27_wsierp_1,t15_prepower,t90_xcmplx_1,d3_nat_1,t62_newton]), [file(wsierp_1,t42_wsierp_1),interesting(0.00)]). fof(t32_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( A = k6_finseq_1(B) <=> k3_finseq_1(A) = 0 ) ) ), file(finseq_1,t32_finseq_1), [interesting(0.00)]). fof(t16_int_2,theorem,( ! [A] : ( v1_int_1(A) => ( r2_int_1(A,0) & r2_int_1(1,A) & r2_int_1(k1_real_1(1),A) ) ) ), file(int_2,t16_int_2), [interesting(0.00)]). fof(d2_int_1,definition,( ! [A] : ( v1_int_1(A) <=> r2_hidden(A,k4_numbers) ) ), file(int_1,d2_int_1), [interesting(0.00)]). fof(d3_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k3_finseq_1(A) <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ), file(finseq_1,d3_finseq_1), [interesting(0.00)]). fof(t34_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => ( k6_xcmplx_0(A,B) = k6_xcmplx_0(C,D) => k2_xcmplx_0(A,D) = k2_xcmplx_0(B,C) ) ) ) ) ) ), file(xcmplx_1,t34_xcmplx_1), [interesting(0.00)]). fof(t4_finseq_1,theorem, ( k2_finseq_1(0) = k1_xboole_0 & k2_finseq_1(1) = k1_tarski(1) & k2_finseq_1(2) = k2_tarski(1,2) ), file(finseq_1,t4_finseq_1), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t39_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => r1_tarski(k4_finseq_1(A),k4_finseq_1(k7_finseq_1(A,B))) ) ) ), file(finseq_1,t39_finseq_1), [interesting(0.00)]). fof(t22_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ~ ( k3_finseq_1(B) != 0 & ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m1_subset_1(D,A) => B != k8_finseq_1(A,C,k12_finseq_1(A,D)) ) ) ) ) ) ), file(finseq_2,t22_finseq_2), [interesting(0.00)]). fof(t124_rvsum_1,theorem,( k16_rvsum_1(k6_finseq_1(k1_numbers)) = 1 ), file(rvsum_1,t124_rvsum_1), [interesting(0.00)]). fof(t12_wsierp_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( k6_nat_1(A,B) = 1 & k6_nat_1(C,B) = 1 ) => k6_nat_1(k2_nat_1(A,C),B) = 1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_wsierp_1,t11_wsierp_1,l18_wsierp_1]), [file(wsierp_1,t12_wsierp_1),interesting(0.00)]). fof(s2_finseq_2,theorem, ( ( p1_s2_finseq_2(k6_finseq_1(f1_s2_finseq_2)) & ! [A] : ( m2_finseq_1(A,f1_s2_finseq_2) => ! [B] : ( m1_subset_1(B,f1_s2_finseq_2) => ( p1_s2_finseq_2(A) => p1_s2_finseq_2(k8_finseq_1(f1_s2_finseq_2,A,k12_finseq_1(f1_s2_finseq_2,B))) ) ) ) ) => ! [A] : ( m2_finseq_1(A,f1_s2_finseq_2) => p1_s2_finseq_2(A) ) ), file(finseq_2,s2_finseq_2), [interesting(0.00)]). fof(s2_finseq_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & k3_finseq_1(A) = f1_s2_finseq_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k2_finseq_1(f1_s2_finseq_1)) => k1_funct_1(A,B) = f2_s2_finseq_1(B) ) ) ) ), file(finseq_1,s2_finseq_1), [interesting(0.00)]). fof(t14_finseq_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(A)) => r2_hidden(k1_funct_1(A,C),B) ) ) => m2_finseq_1(A,B) ) ) ), file(finseq_2,t14_finseq_2), [interesting(0.00)]). fof(t125_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k16_rvsum_1(k12_finseq_1(k1_numbers,A)) = A ) ), file(rvsum_1,t125_rvsum_1), [interesting(0.00)]). fof(t26_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,k2_xcmplx_0(B,1)) & ~ r1_xreal_0(A,B) & A != k2_xcmplx_0(B,1) ) ) ) ), file(nat_1,t26_nat_1), [interesting(0.00)]). fof(t44_wsierp_1,theorem,( ! [A] : ( m1_trees_4(A,k1_numbers,k5_numbers) => ( ( r1_xreal_0(2,k3_finseq_1(A)) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k4_finseq_1(A)) & r2_hidden(C,k4_finseq_1(A)) ) => ( B = C | k6_nat_1(k3_wsierp_1(A,B),k3_wsierp_1(A,C)) = 1 ) ) ) ) ) => ! [B] : ( m1_trees_4(B,k1_numbers,k6_wsierp_1) => ~ ( k3_finseq_1(B) = k3_finseq_1(A) & ! [C] : ( m1_trees_4(C,k1_numbers,k6_wsierp_1) => ~ ( k3_finseq_1(C) = k3_finseq_1(A) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k3_real_1(k4_real_1(k3_wsierp_1(A,D),k1_wsierp_1(C,D)),k1_wsierp_1(B,D)) = k3_real_1(k4_real_1(k3_wsierp_1(A,1),k1_wsierp_1(C,1)),k1_wsierp_1(B,1)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_finseq_1,t19_finseq_2,t27_finseq_3,t16_int_2,l18_wsierp_1,t40_wsierp_1,d2_int_1,t61_finseq_1,d3_finseq_1,t61_finseq_1,t34_xcmplx_1,t4_finseq_1,d2_tarski,t19_finseq_2,t38_nat_1,t39_finseq_1,d7_finseq_1,t22_finseq_2,t19_finseq_2,t38_nat_1,d7_finseq_1,t39_finseq_1,t59_finseq_1,t38_nat_1,t27_finseq_3,t6_finseq_5,t43_wsierp_1,l18_wsierp_1,t16_int_2,t40_wsierp_1,s2_finseq_1,d3_finseq_1,d2_int_1,t14_finseq_2,d2_int_1,t19_finseq_2,t27_finseq_3,d3_finseq_1,d7_finseq_1,d7_finseq_1,l52_wsierp_1,t2_xreal_1,d3_finseq_1,d7_finseq_1,d3_finseq_1,t2_xreal_1,t59_finseq_1,t26_nat_1,d5_real_1,s2_finseq_2]), [file(wsierp_1,t44_wsierp_1),interesting(0.00)]). fof(t45_wsierp_1,theorem,( $true ), file(wsierp_1,t45_wsierp_1), [interesting(0.00)]). fof(t83_square_1,theorem,( k9_square_1(1) = 1 ), file(square_1,t83_square_1), [interesting(0.00)]). fof(t95_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(B,A) & r1_xreal_0(k8_square_1(B),k8_square_1(A)) ) ) ) ), file(square_1,t95_square_1), [interesting(0.00)]). fof(t76_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,1) & r1_xreal_0(k5_square_1(A),A) ) ) ), file(square_1,t76_square_1), [interesting(0.00)]). fof(d4_square_1,definition,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(0,A) => ! [B] : ( v1_xreal_0(B) => ( B = k8_square_1(A) <=> ( r1_xreal_0(0,B) & k5_square_1(B) = A ) ) ) ) ) ), file(square_1,d4_square_1), [interesting(0.00)]). fof(t82_square_1,theorem,( k9_square_1(0) = 0 ), file(square_1,t82_square_1), [interesting(0.00)]). fof(t75_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(1,A) & r1_xreal_0(A,k5_square_1(A)) ) ) ), file(square_1,t75_square_1), [interesting(0.00)]). fof(l77_wsierp_1,theorem,( ! [A] : ( v1_int_1(A) => ( ( ~ r1_xreal_0(A,1) => ( ~ r1_xreal_0(k8_square_1(A),1) & ~ r1_xreal_0(A,k8_square_1(A)) ) ) & ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(1,A) & ~ ( ~ r1_xreal_0(k8_square_1(A),0) & ~ r1_xreal_0(1,k8_square_1(A)) & ~ r1_xreal_0(k8_square_1(A),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t83_square_1,t95_square_1,t76_square_1,d4_square_1,t82_square_1,t95_square_1,t83_square_1,t95_square_1,t75_square_1,d4_square_1]), [file(wsierp_1,l77_wsierp_1),interesting(0.00)]). fof(t93_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k8_square_1(A),0) ) ) ), file(square_1,t93_square_1), [interesting(0.00)]). fof(d4_int_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_int_1(B) => ( B = k1_int_1(A) <=> ( r1_xreal_0(B,A) & ~ r1_xreal_0(B,k6_xcmplx_0(A,1)) ) ) ) ) ), file(int_1,d4_int_1), [interesting(0.00)]). fof(t78_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(B,A) & r1_xreal_0(k5_square_1(B),k5_square_1(A)) ) ) ) ), file(square_1,t78_square_1), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(t11_finseq_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( r2_hidden(A,k2_relat_1(B)) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(B)) & k1_funct_1(B,C) = A ) ) ) ) ), file(finseq_2,t11_finseq_2), [interesting(0.00)]). fof(t78_newton,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(0,A) => r1_xreal_0(0,k6_int_1(B,A)) ) ) ) ), file(newton,t78_newton), [interesting(0.00)]). fof(t79_newton,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k6_int_1(B,A)) ) ) ) ), file(newton,t79_newton), [interesting(0.00)]). fof(t7_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) <=> r1_tarski(k2_finseq_1(A),k2_finseq_1(B)) ) ) ) ), file(finseq_1,t7_finseq_1), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t74_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( ( r1_tarski(k2_relat_1(A),k4_finseq_1(A)) & v2_funct_1(A) ) => k2_relat_1(A) = k4_finseq_1(A) ) ) ), file(finseq_4,t74_finseq_4), [interesting(0.00)]). fof(d8_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) & k1_funct_1(A,B) = k1_funct_1(A,C) ) => B = C ) ) ) ), file(funct_1,d8_funct_1), [interesting(0.00)]). fof(t80_newton,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( A != 0 => B = k2_xcmplx_0(k3_xcmplx_0(k5_int_1(B,A),A),k6_int_1(B,A)) ) ) ) ), file(newton,t80_newton), [interesting(0.00)]). fof(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t26_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ), file(xreal_1,t26_xreal_1), [interesting(0.00)]). fof(t12_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(B,A) ) <=> r1_xreal_0(k18_complex1(B),A) ) ) ) ), file(absvalue,t12_absvalue), [interesting(0.00)]). fof(d7_int_1,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => k5_int_1(A,B) = k1_int_1(k7_xcmplx_0(A,B)) ) ) ), file(int_1,d7_int_1), [interesting(0.00)]). fof(t73_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => ( ~ ( ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) & ~ ( ~ r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) & r1_xreal_0(C,B) ) ) ) ) ) ) ), file(real_1,t73_real_1), [interesting(0.00)]). fof(t128_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( A != 0 => k6_xcmplx_0(B,k7_xcmplx_0(C,A)) = k7_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(B,A),C),A) ) ) ) ) ), file(xcmplx_1,t128_xcmplx_1), [interesting(0.00)]). fof(t127_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ( ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) | ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) & r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), file(real_2,t127_real_2), [interesting(0.00)]). fof(t47_int_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( k1_int_1(A) = A <=> v1_int_1(A) ) ) ), file(int_1,t47_int_1), [interesting(0.00)]). fof(t125_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(A,0) & r1_xreal_0(B,0) ) | ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) ) => r1_xreal_0(0,k7_xcmplx_0(A,B)) ) ) ) ), file(real_2,t125_real_2), [interesting(0.00)]). fof(t11_pre_ff,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(B,A) => r1_xreal_0(k1_int_1(B),k1_int_1(A)) ) ) ) ), file(pre_ff,t11_pre_ff), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t2_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( k2_xcmplx_0(A,B) = k2_xcmplx_0(C,B) => A = C ) ) ) ) ), file(xcmplx_1,t2_xcmplx_1), [interesting(0.00)]). fof(d8_int_1,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ( B != 0 => k6_int_1(A,B) = k6_xcmplx_0(A,k3_xcmplx_0(k5_int_1(A,B),B)) ) & ( B = 0 => k6_int_1(A,B) = 0 ) ) ) ) ), file(int_1,d8_int_1), [interesting(0.00)]). fof(t14_int_2,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ( r2_int_1(A,B) => r2_int_1(A,k4_xcmplx_0(B)) ) & ( r2_int_1(A,k4_xcmplx_0(B)) => r2_int_1(A,B) ) & ( r2_int_1(A,B) => r2_int_1(k4_xcmplx_0(A),B) ) & ( r2_int_1(k4_xcmplx_0(A),B) => r2_int_1(A,B) ) & ( r2_int_1(A,B) => r2_int_1(k4_xcmplx_0(A),k4_xcmplx_0(B)) ) & ( r2_int_1(k4_xcmplx_0(A),k4_xcmplx_0(B)) => r2_int_1(A,B) ) & ( r2_int_1(A,k4_xcmplx_0(B)) => r2_int_1(k4_xcmplx_0(A),B) ) & ( r2_int_1(k4_xcmplx_0(A),B) => r2_int_1(A,k4_xcmplx_0(B)) ) ) ) ) ), file(int_2,t14_int_2), [interesting(0.00)]). fof(t54_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_nat_1(B,A) => ( r1_xreal_0(A,0) | r1_xreal_0(B,A) ) ) ) ) ), file(nat_1,t54_nat_1), [interesting(0.00)]). fof(t1_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ( k18_complex1(A) = A | k18_complex1(A) = k4_xcmplx_0(A) ) ) ), file(absvalue,t1_absvalue), [interesting(0.00)]). fof(t11_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => k2_xboole_0(k2_finseq_1(A),k1_tarski(k2_xcmplx_0(A,1))) = k2_finseq_1(k2_xcmplx_0(A,1)) ) ), file(finseq_1,t11_finseq_1), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t4_wsierp_1,theorem,( $true ), file(wsierp_1,t4_wsierp_1), [interesting(0.00)]). fof(t37_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,C) ) => r1_xreal_0(k2_xcmplx_0(B,A),C) ) ) ) ) ), file(xreal_1,t37_xreal_1), [interesting(0.00)]). fof(t54_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,C) ) => r1_xreal_0(B,k6_xcmplx_0(C,A)) ) ) ) ) ), file(xreal_1,t54_xreal_1), [interesting(0.00)]). fof(t38_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(A,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(C,k2_xcmplx_0(B,A)) ) ) ) ) ), file(xreal_1,t38_xreal_1), [interesting(0.00)]). fof(t39_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(B,C) & r1_xreal_0(C,k2_xcmplx_0(B,A)) ) ) ) ) ), file(xreal_1,t39_xreal_1), [interesting(0.00)]). fof(t55_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(A,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k6_xcmplx_0(C,A),B) ) ) ) ) ), file(xreal_1,t55_xreal_1), [interesting(0.00)]). fof(t56_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(B,C) & r1_xreal_0(k6_xcmplx_0(C,A),B) ) ) ) ) ), file(xreal_1,t56_xreal_1), [interesting(0.00)]).