fof(t28_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ r1_xreal_0(1,k18_complex1(A)) => ( v1_series_1(k2_prepower(A)) & k2_series_1(k2_prepower(A)) = k7_xcmplx_0(1,k6_xcmplx_0(1,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[s1_seq_1,t3_series_1,t9_seq_2,t52_xreal_1,t70_xreal_1,d7_seq_2,t9_seq_2,t26_series_1,t121_xcmplx_1,t188_xcmplx_1,t138_complex1,t153_complex1,d1_absvalue,t73_real_1,t90_xcmplx_1,d6_seq_2,d7_seq_2,d2_series_1]), [file(series_1,t28_series_1),interesting(1.00)]). fof(t36_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => k8_funct_2(k5_numbers,k1_numbers,B,C) = k7_xcmplx_0(1,k3_power(C,A)) ) ) => ( r1_xreal_0(A,1) | v1_series_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_nat_1,s1_rcomp_1,t99_prepower,d2_power,t164_real_2,t9_xreal_1,t37_nat_1,t39_power,t141_xreal_1,t101_xcmplx_1,t100_xcmplx_1,t36_power,d2_power,t127_real_2,t29_nat_1,t143_real_2,t98_prepower,t85_prepower,t118_real_2,t22_nat_1,d14_seqm_3,s1_seq_1,t9_xreal_1,t39_power,t127_real_2,t22_nat_1,s1_seq_1,t39_power,t38_nat_1,t38_power,t33_power,t32_power,t39_power,t38_power,t8_xreal_1,t39_power,d9_seqm_3,t46_power,t5_power,d6_seqm_3,t39_seq_4,t35_seq_4,t41_seq_4,t36_seq_4,t105_real_2,t41_power,t32_series_1,t35_series_1,t15_series_1,t8_xreal_1,d9_seqm_3,d9_seqm_3,d9_seqm_3,t8_xreal_1,d9_seqm_3,d9_seqm_3,t22_series_1,t16_series_1]), [file(series_1,t36_series_1),interesting(0.99)]). fof(t40_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v2_series_1(A) => v1_series_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d5_series_1,t25_series_1,t39_series_1,t2_xreal_1,t25_series_1]), [file(series_1,t40_series_1),interesting(0.96)]). fof(t16_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & v1_series_1(k1_seqm_3(A,B)) ) => v1_series_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t15_series_1,d2_series_1,t57_funcop_1,t13_funcop_1,t39_seq_4,d1_series_1,d9_seqm_3,d9_seqm_3,d1_series_1,d1_series_1,d9_seqm_3,d9_seqm_3,d1_series_1,d9_seqm_3,s1_nat_1,t11_seq_1,t36_seqm_3,t19_seq_2,t35_seq_4,d2_series_1]), [file(series_1,t16_series_1),interesting(0.92)]). fof(t15_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_series_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => v1_series_1(k1_seqm_3(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_seqm_3,d2_series_1,t33_seq_4,t36_seqm_3,t57_funcop_1,t13_funcop_1,t39_seq_4,t14_series_1,t25_seq_2,d2_series_1,s1_nat_1]), [file(series_1,t15_series_1),interesting(0.91)]). fof(t7_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_series_1(A) => ( v4_seq_2(A) & k2_seq_2(A) = 0 ) ) ) ), inference(mizar_proof,[status(thm)],[d2_series_1,t33_seq_4,t26_seq_2,d1_series_1,d9_seqm_3,d9_seqm_3,t11_seq_1,t11_seq_1,t15_seq_1,t11_seq_1,t14_seq_1,t113_funct_2,t39_seq_1,t25_seq_2,t35_seq_4,t36_seq_4]), [file(series_1,t7_series_1),interesting(0.90)]). fof(t2_series_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ( B != 0 => k4_power(k18_complex1(B),A) = k18_complex1(k3_power(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t133_complex1,d1_absvalue,t39_power,d1_absvalue,t1_scheme1,d1_absvalue,t54_power,t39_power,d1_absvalue,d1_absvalue,t55_power,t39_power,d1_absvalue,t138_complex1]), [file(series_1,t2_series_1),interesting(0.86)]). fof(t12_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => k1_series_1(k14_seq_1(B,A)) = k14_seq_1(k1_series_1(B),A) ) ) ), inference(mizar_proof,[status(thm)],[t13_seq_1,d1_series_1,t13_seq_1,t13_seq_1,d1_series_1,t13_seq_1,t13_seq_1,d1_series_1]), [file(series_1,t12_series_1),interesting(0.80)]). fof(t37_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ~ ( r1_xreal_0(A,1) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => k8_funct_2(k5_numbers,k1_numbers,B,C) = k7_xcmplx_0(1,k3_power(C,A)) ) ) & v1_series_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_xreal_1,d7_seq_2,t10_seq_4,t38_nat_1,t2_xreal_1,t33_power,d1_absvalue,t99_prepower,d2_power,t7_series_1,t38_nat_1,s1_rcomp_1,t99_prepower,d2_power,t164_real_2,t9_xreal_1,t37_nat_1,t39_power,t141_xreal_1,t101_xcmplx_1,t100_xcmplx_1,t36_power,d2_power,t127_real_2,t29_nat_1,t143_real_2,t98_prepower,t85_prepower,t118_real_2,t22_nat_1,d14_seqm_3,s1_seq_1,t9_xreal_1,t39_power,t127_real_2,t22_nat_1,d7_seq_2,t46_power,t19_prepower,t38_power,t33_power,t32_power,d1_absvalue,t70_xreal_1,t30_power,t32_power,t50_xreal_1,t121_real_2,t9_xreal_1,t99_prepower,d2_power,t7_series_1,t35_series_1,t22_series_1]), [file(series_1,t37_series_1),interesting(0.74)]). fof(t32_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,A,C)) ) ) & v4_seq_2(B) ) => ( r1_xreal_0(1,k2_seq_2(B)) | v1_series_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_xreal_1,t217_xreal_1,t33_seq_4,t29_nat_1,d9_seqm_3,t8_power,t2_prepower,t2_xreal_1,t109_real_2,t8_xreal_1,t73_real_1,t52_xreal_1,d7_seq_2,t38_nat_1,t29_nat_1,t2_xreal_1,t9_seq_2,t21_xreal_1,t39_power,d3_prepower,d1_power,t42_power,t47_power,t5_power,t52_xreal_1,t217_xreal_1,t105_real_2,t106_real_2,t2_xreal_1,t73_real_1,t21_xreal_1,t26_xreal_1,t9_seq_2,t28_series_1,t29_nat_1,t2_xreal_1,d1_prepower,t47_power,t22_series_1]), [file(series_1,t32_series_1),interesting(0.63)]). fof(t30_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,C),0) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k6_real_1(k8_funct_2(k5_numbers,k1_numbers,A,k1_nat_1(C,1)),k8_funct_2(k5_numbers,k1_numbers,A,C)) ) ) & v4_seq_2(B) ) => ( r1_xreal_0(1,k2_seq_2(B)) | v1_series_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_xreal_1,t217_xreal_1,d7_seq_2,t141_xreal_1,t2_prepower,t52_xreal_1,t217_xreal_1,t105_real_2,t106_real_2,t2_xreal_1,t73_real_1,t21_xreal_1,t26_xreal_1,t9_seq_2,t28_series_1,t13_series_1,t2_xreal_1,t109_real_2,t8_xreal_1,t73_real_1,t52_xreal_1,t13_seq_1,d1_prepower,t46_power,t32_power,t29_power,t29_nat_1,t9_seq_2,t21_xreal_1,t88_xcmplx_1,t66_xreal_1,t66_xreal_1,t13_seq_1,t4_prepower,t13_seq_1,t2_xreal_1,s1_nat_1,t28_nat_1,t22_series_1]), [file(series_1,t30_series_1),interesting(0.55)]). fof(t45_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,A,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(B),C)) ) & v4_seq_2(A) ) => ( r1_xreal_0(1,k2_seq_2(A)) | v2_series_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_seq_1,t132_complex1,t32_series_1,d5_series_1]), [file(series_1,t45_series_1),interesting(0.54)]). fof(t3_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,C) = k3_power(A,k1_nat_1(C,1)) ) => ( r1_xreal_0(1,k18_complex1(A)) | ( v4_seq_2(B) & k2_seq_2(B) = 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_absvalue,d2_power,d6_seqm_3,t39_seq_4,t41_seq_4,t7_absvalue,t132_complex1,s1_seq_1,t1_series_1,t2_series_1,t16_seq_1,t28_seq_4]), [file(series_1,t3_series_1),interesting(0.51)]). fof(t1_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,C) = k3_power(A,k1_nat_1(C,1)) ) => ( r1_xreal_0(A,0) | r1_xreal_0(1,A) | ( v4_seq_2(B) & k2_seq_2(B) = 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l1_series_1,t151_real_2,t52_xreal_1,t127_real_2,t79_xcmplx_1,t122_real_2,t127_real_2,t52_int_1,t20_int_1,t16_int_1,d4_int_1,t2_xreal_1,t21_xreal_1,t177_real_2,t39_power,d1_absvalue,t56_power,t36_power,t31_power,t8_xreal_1,t2_xreal_1,t2_xreal_1,t154_real_2,d6_seq_2,d7_seq_2]), [file(series_1,t1_series_1),interesting(0.50)]). fof(t35_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seqm_3(A) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k4_real_1(k3_series_1(2,C),k8_funct_2(k5_numbers,k1_numbers,A,k3_series_1(2,C))) ) ) ) => ( v1_series_1(A) <=> v1_series_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t121_real_2,t29_power,d1_series_1,d1_series_1,d1_series_1,t9_xreal_1,t9_xreal_1,t9_xreal_1,t8_xreal_1,d1_series_1,s1_seq_1,t14_xcmplx_1,t38_nat_1,t38_nat_1,t9_xreal_1,t30_power,t32_power,t14_seqm_3,t9_xreal_1,d1_series_1,t38_nat_1,s1_nat_1,t66_xreal_1,t30_power,t32_power,t30_power,t32_power,t9_xreal_1,t2_xreal_1,s1_nat_1,t20_series_1,d3_seq_2,t70_xreal_1,t2_xreal_1,d3_seq_2,t20_series_1,t30_power,d1_series_1,d1_series_1,d1_series_1,t29_power,d1_series_1,t9_xreal_1,d1_series_1,t29_nat_1,t14_seqm_3,t9_xreal_1,d1_series_1,s1_nat_1,t30_power,t32_power,t9_xreal_1,t2_xreal_1,s1_nat_1,t19_series_1,t20_series_1,d3_seq_2,t56_power,t29_nat_1,t2_xreal_1,t9_xreal_1,t30_power,t32_power,t29_nat_1,t2_xreal_1,t12_seqm_3,t2_xreal_1,t8_xreal_1,t2_xreal_1,d3_seq_2,t20_series_1]), [file(series_1,t35_series_1),interesting(0.47)]). fof(t25_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_series_1(A) <=> ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & r1_xreal_0(B,k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),D),k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),C)))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_series_1,t58_seq_4,t58_seq_4,d2_series_1]), [file(series_1,t25_series_1),interesting(0.47)]). fof(t18_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_series_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k2_series_1(A) = k3_real_1(k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),B),k2_series_1(k1_seqm_3(A,k1_nat_1(B,1)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t57_funcop_1,t13_funcop_1,d2_series_1,t33_seq_4,t39_seq_4,t14_series_1,t26_seq_2,t33_seq_4,t41_seq_4,d1_series_1,t57_funcop_1,t13_funcop_1,t39_seq_4,t15_series_1,d2_series_1,t33_seq_4,t14_series_1,t36_seqm_3,t26_seq_2,t33_seq_4,t41_seq_4,d9_seqm_3,d1_series_1,s1_nat_1]), [file(series_1,t18_series_1),interesting(0.45)]). fof(t47_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ~ ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,A,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(B),C)) ) & v4_seq_2(A) & ~ r1_xreal_0(k2_seq_2(A),1) & v1_series_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_xreal_1,d7_seq_2,t29_nat_1,t2_xreal_1,t132_complex1,t16_seq_1,t9_seq_2,t8_xreal_1,t19_prepower,t29_nat_1,t2_xreal_1,t5_power,t43_series_1,t7_series_1]), [file(series_1,t47_series_1),interesting(0.31)]). fof(t42_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( k8_funct_2(k5_numbers,k1_numbers,A,C) != 0 & k8_funct_2(k5_numbers,k1_numbers,B,C) = k6_real_1(k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(A),k1_nat_1(C,1)),k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(A),C)) ) ) & v4_seq_2(B) ) => ( r1_xreal_0(1,k2_seq_2(B)) | v2_series_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_seq_1,t133_complex1,t30_series_1,d5_series_1]), [file(series_1,t42_series_1),interesting(0.29)]). fof(t34_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ~ ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,A,C)) ) ) & v4_seq_2(B) & ~ r1_xreal_0(k2_seq_2(B),1) & v1_series_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_xreal_1,d7_seq_2,t9_seq_2,t8_xreal_1,t33_series_1]), [file(series_1,t34_series_1),interesting(0.26)]). fof(t44_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ~ ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,A,B) != 0 ) & ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,C) => r1_xreal_0(1,k6_real_1(k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(A),k1_nat_1(C,1)),k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(A),C))) ) ) ) & v1_series_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t133_complex1,t29_nat_1,t16_seq_1,t16_seq_1,t133_complex1,t118_real_2,t2_xreal_1,s1_nat_1,t28_nat_1,t43_series_1,t7_series_1]), [file(series_1,t44_series_1),interesting(0.25)]). fof(t29_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,k1_nat_1(C,1)) = k3_xcmplx_0(A,k8_funct_2(k5_numbers,k1_numbers,B,C)) ) => ( r1_xreal_0(1,k18_complex1(A)) | ( v1_series_1(B) & k2_series_1(B) = k7_xcmplx_0(k8_funct_2(k5_numbers,k1_numbers,B,0),k6_xcmplx_0(1,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_prepower,t4_prepower,s1_nat_1,t13_seq_1,t12_series_1,t28_series_1,d2_series_1,t21_seq_2,t22_seq_2,t75_xcmplx_1,d2_series_1]), [file(series_1,t29_series_1),interesting(0.15)]). fof(d2_series_1,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_series_1(A) <=> v4_seq_2(k1_series_1(A)) ) ) ), file(series_1,d2_series_1), [interesting(0.00)]). fof(t19_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(A) & v4_seq_2(B) ) => v4_seq_2(k9_seq_1(A,B)) ) ) ) ), file(seq_2,t19_seq_2), [interesting(0.00)]). fof(t11_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( A = k6_seq_1(k5_numbers,k1_numbers,B,C) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,D) = k3_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ), file(seq_1,t11_seq_1), [interesting(0.00)]). fof(d1_series_1,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( B = k1_series_1(A) <=> ( k8_funct_2(k5_numbers,k1_numbers,B,0) = k8_funct_2(k5_numbers,k1_numbers,A,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,k1_nat_1(C,1)) = k3_real_1(k8_funct_2(k5_numbers,k1_numbers,B,C),k8_funct_2(k5_numbers,k1_numbers,A,k1_nat_1(C,1))) ) ) ) ) ) ), file(series_1,d1_series_1), [interesting(0.00)]). fof(t8_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => k9_seq_1(k1_series_1(A),k1_series_1(B)) = k1_series_1(k9_seq_1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t11_seq_1,d1_series_1,d1_series_1,t11_seq_1,t11_seq_1,d1_series_1,d1_series_1,t11_seq_1,t11_seq_1,d1_series_1]), [file(series_1,t8_series_1),interesting(0.00)]). fof(t20_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(A) & v4_seq_2(B) ) => k2_seq_2(k9_seq_1(A,B)) = k3_real_1(k2_seq_2(A),k2_seq_2(B)) ) ) ) ), file(seq_2,t20_seq_2), [interesting(0.00)]). fof(t10_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v1_series_1(A) & v1_series_1(B) ) => ( v1_series_1(k9_seq_1(A,B)) & k2_series_1(k9_seq_1(A,B)) = k3_real_1(k2_series_1(A),k2_series_1(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_series_1,d2_series_1,t19_seq_2,t8_series_1,d2_series_1,t8_series_1,t20_seq_2]), [file(series_1,t10_series_1),interesting(0.00)]). fof(t25_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(A) & v4_seq_2(B) ) => v4_seq_2(k10_seq_1(A,B)) ) ) ) ), file(seq_2,t25_seq_2), [interesting(0.00)]). fof(t6_rfunct_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( A = k10_seq_1(B,C) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,D) = k5_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ), file(rfunct_2,t6_rfunct_2), [interesting(0.00)]). fof(t9_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => k10_seq_1(k1_series_1(A),k1_series_1(B)) = k1_series_1(k10_seq_1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t6_rfunct_2,d1_series_1,d1_series_1,t6_rfunct_2,t6_rfunct_2,d1_series_1,d1_series_1,t6_rfunct_2,t6_rfunct_2,d1_series_1]), [file(series_1,t9_series_1),interesting(0.00)]). fof(t26_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(A) & v4_seq_2(B) ) => k2_seq_2(k10_seq_1(A,B)) = k5_real_1(k2_seq_2(A),k2_seq_2(B)) ) ) ) ), file(seq_2,t26_seq_2), [interesting(0.00)]). fof(t11_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v1_series_1(A) & v1_series_1(B) ) => ( v1_series_1(k10_seq_1(A,B)) & k2_series_1(k10_seq_1(A,B)) = k5_real_1(k2_series_1(A),k2_series_1(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_series_1,d2_series_1,t25_seq_2,t9_series_1,d2_series_1,t9_series_1,t26_seq_2]), [file(series_1,t11_series_1),interesting(0.00)]). fof(t57_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(C,B) => ( v1_funct_1(k2_funcop_1(A,C)) & v1_funct_2(k2_funcop_1(A,C),A,B) & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ), file(funcop_1,t57_funcop_1), [interesting(0.00)]). fof(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(t33_seq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v4_seq_2(B) => ( v4_seq_2(k1_seqm_3(B,A)) & k2_seq_2(k1_seqm_3(B,A)) = k2_seq_2(B) ) ) ) ) ), file(seq_4,t33_seq_4), [interesting(0.00)]). fof(t39_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v5_seqm_3(A) => v4_seq_2(A) ) ) ), file(seq_4,t39_seq_4), [interesting(0.00)]). fof(d9_seqm_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( C = k1_seqm_3(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(D,B)) ) ) ) ) ) ), file(seqm_3,d9_seqm_3), [interesting(0.00)]). fof(t14_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,C) = k8_funct_2(k5_numbers,k1_numbers,A,0) ) => k1_series_1(k1_seqm_3(A,1)) = k10_seq_1(k1_seqm_3(k1_series_1(A),1),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_rfunct_2,d9_seqm_3,d1_series_1,d1_series_1,d9_seqm_3,t6_rfunct_2,d9_seqm_3,d1_series_1,d9_seqm_3,t6_rfunct_2,d9_seqm_3,d1_series_1]), [file(series_1,t14_series_1),interesting(0.00)]). fof(t41_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v5_seqm_3(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k2_seq_2(A) = k8_funct_2(k5_numbers,k1_numbers,A,B) ) ) ) ), file(seq_4,t41_seq_4), [interesting(0.00)]). fof(t34_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => k1_seqm_3(A,0) = A ) ), file(seqm_3,t34_seqm_3), [interesting(0.00)]). fof(t36_seqm_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => k1_seqm_3(k1_seqm_3(C,A),B) = k1_seqm_3(C,k1_nat_1(A,B)) ) ) ) ), file(seqm_3,t36_seqm_3), [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(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(d13_seqm_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1))) ) ) ) ), file(seqm_3,d13_seqm_3), [interesting(0.00)]). fof(t19_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,B)) ) => v3_seqm_3(k1_series_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[t8_xreal_1,d1_series_1,d13_seqm_3]), [file(series_1,t19_series_1),interesting(0.00)]). fof(t21_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,0),k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ) ), file(seqm_3,t21_seqm_3), [interesting(0.00)]). fof(t31_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) => r1_xreal_0(0,k2_seq_2(A)) ) ) ), file(seq_2,t31_seq_2), [interesting(0.00)]). fof(t21_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ( v1_series_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,B)) ) ) => r1_xreal_0(0,k2_series_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[t19_series_1,d2_series_1,t21_seqm_3,d1_series_1,t31_seq_2]), [file(series_1,t21_series_1),interesting(0.00)]). fof(t23_series_1,theorem,( $true ), file(series_1,t23_series_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(t51_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ( v3_seqm_3(A) & v1_seq_2(A) ) => v4_seq_2(A) ) ) ), file(seq_4,t51_seq_4), [interesting(0.00)]). fof(t27_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) => v3_seq_2(A) ) ) ), file(seq_2,t27_seq_2), [interesting(0.00)]). fof(d5_seq_2,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ( v3_seq_2(A) <=> ( v1_seq_2(A) & v2_seq_2(A) ) ) ) ), file(seq_2,d5_seq_2), [interesting(0.00)]). fof(t20_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,B)) ) => ( v1_seq_2(k1_series_1(A)) <=> v1_series_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_series_1,t51_seq_4,d2_series_1,d2_series_1,t27_seq_2,d5_seq_2]), [file(series_1,t20_series_1),interesting(0.00)]). fof(d3_seq_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_seq_2(A) <=> ? [B] : ( v1_xreal_0(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ r1_xreal_0(B,k2_seq_1(k5_numbers,k1_numbers,A,C)) ) ) ) ) ), file(seq_2,d3_seq_2), [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(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(t17_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,C),k8_funct_2(k5_numbers,k1_numbers,B,C)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),C),k8_funct_2(k5_numbers,k1_numbers,k1_series_1(B),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_series_1,d1_series_1,d1_series_1,d1_series_1,t9_xreal_1,s1_nat_1]), [file(series_1,t17_series_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(t35_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => A != k1_seqm_3(B,C) ) | v4_seq_2(B) ) ) ) ) ), file(seq_4,t35_seq_4), [interesting(0.00)]). fof(t22_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) ) & v1_series_1(B) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & ~ r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,D),k8_funct_2(k5_numbers,k1_numbers,B,D)) ) ) | v1_series_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_seqm_3,t29_nat_1,t15_series_1,t20_series_1,d3_seq_2,t37_nat_1,d9_seqm_3,d9_seqm_3,d9_seqm_3,t17_series_1,t2_xreal_1,d3_seq_2,t20_series_1,t16_series_1]), [file(series_1,t22_series_1),interesting(0.00)]). fof(t32_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(A) & v4_seq_2(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) => r1_xreal_0(k2_seq_2(A),k2_seq_2(B)) ) ) ) ), file(seq_2,t32_seq_2), [interesting(0.00)]). fof(t24_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,C),k8_funct_2(k5_numbers,k1_numbers,B,C)) ) ) & v1_series_1(B) ) => ( v1_series_1(A) & r1_xreal_0(k2_series_1(A),k2_series_1(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_series_1,d2_series_1,d2_series_1,t17_series_1,t32_seq_2]), [file(series_1,t24_series_1),interesting(0.00)]). fof(t4_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( B = k2_prepower(A) <=> ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 1 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,B,k1_nat_1(C,1)) = k3_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,B,C),A) ) ) ) ) ) ), file(prepower,t4_prepower), [interesting(0.00)]). fof(t13_seq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( B = k14_seq_1(C,A) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,B,D) = k3_xcmplx_0(A,k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ), file(seq_1,t13_seq_1), [interesting(0.00)]). fof(t60_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ( A != 0 => k7_xcmplx_0(A,A) = 1 ) ) ), file(xcmplx_1,t60_xcmplx_1), [interesting(0.00)]). fof(t30_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(A,1) = A ) ), file(power,t30_power), [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(d1_prepower,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( B = k2_prepower(A) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,B,C) = k2_newton(A,C) ) ) ) ) ), file(prepower,d1_prepower), [interesting(0.00)]). fof(t47_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => k3_power(A,B) = k2_newton(A,B) ) ) ) ), file(power,t47_power), [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(t63_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k2_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k2_xcmplx_0(A,C),B) ) ) ) ), file(xcmplx_1,t63_xcmplx_1), [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(t26_series_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ( B != 1 => k8_funct_2(k5_numbers,k1_numbers,k1_series_1(k2_prepower(B)),A) = k7_xcmplx_0(k6_xcmplx_0(1,k3_power(B,k1_nat_1(A,1))),k6_xcmplx_0(1,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_series_1,t4_prepower,t60_xcmplx_1,t30_power,t8_xreal_1,t31_xreal_1,t2_xreal_1,d1_series_1,d1_prepower,t47_power,t60_xcmplx_1,t75_xcmplx_1,t63_xcmplx_1,t47_power,t11_newton,t47_power,s1_nat_1]), [file(series_1,t26_series_1),interesting(0.00)]). fof(t27_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,k1_nat_1(C,1)) = k3_xcmplx_0(A,k8_funct_2(k5_numbers,k1_numbers,B,C)) ) => ( A = 1 | ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,k1_series_1(B),C) = k7_xcmplx_0(k3_xcmplx_0(k8_funct_2(k5_numbers,k1_numbers,B,0),k6_xcmplx_0(1,k3_power(A,k1_nat_1(C,1)))),k6_xcmplx_0(1,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_prepower,t4_prepower,s1_nat_1,t13_seq_1,t12_series_1,t13_seq_1,t26_series_1,t75_xcmplx_1]), [file(series_1,t27_series_1),interesting(0.00)]). fof(s1_seq_1,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,B) = f1_s1_seq_1(B) ) ) ), file(seq_1,s1_seq_1), [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(d2_power,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( ~ r1_xreal_0(A,0) => ( C = k3_power(A,B) <=> C = k12_prepower(A,B) ) ) & ( A = 0 => ( r1_xreal_0(B,0) | ( C = k3_power(A,B) <=> C = 0 ) ) ) & ( ( A = 0 & B = 0 ) => ( C = k3_power(A,B) <=> C = 1 ) ) & ( v1_int_1(B) => ( r1_xreal_0(0,A) | ( C = k3_power(A,B) <=> ? [D] : ( v1_int_1(D) & D = B & C = k6_prepower(A,D) ) ) ) ) ) ) ) ) ), file(power,d2_power), [interesting(0.00)]). fof(d6_seqm_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v5_seqm_3(A) <=> ? [B] : ( v1_xreal_0(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,C) = B ) ) ) ) ), file(seqm_3,d6_seqm_3), [interesting(0.00)]). fof(t132_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => r1_xreal_0(0,k17_complex1(A)) ) ), file(complex1,t132_complex1), [interesting(0.00)]). fof(l1_series_1,theorem, ( k6_real_1(1,1) = 1 & k6_real_1(1,k1_real_1(1)) = k1_real_1(1) ), file(series_1,l1_series_1), [interesting(0.00)]). fof(t151_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ ( r1_xreal_0(A,0) & r1_xreal_0(0,B) ) & ~ r1_xreal_0(B,A) & r1_xreal_0(k7_xcmplx_0(1,A),k7_xcmplx_0(1,B)) ) ) ) ), file(real_2,t151_real_2), [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(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(t79_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k7_xcmplx_0(A,k3_xcmplx_0(B,C)) = k7_xcmplx_0(k7_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t79_xcmplx_1), [interesting(0.00)]). fof(t122_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ( ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) | ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) ) & r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(real_2,t122_real_2), [interesting(0.00)]). fof(t52_int_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ r1_xreal_0(k2_xcmplx_0(k1_int_1(A),1),A) ) ), file(int_1,t52_int_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(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(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(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(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(t39_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k3_power(A,B),0) ) ) ) ), file(power,t39_power), [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(t56_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(A,k1_real_1(1)) => r1_xreal_0(k2_xcmplx_0(1,k3_xcmplx_0(B,A)),k3_power(k2_xcmplx_0(1,A),B)) ) ) ) ), file(power,t56_power), [interesting(0.00)]). fof(t36_power,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,0) & k3_power(k7_xcmplx_0(A,B),C) != k7_xcmplx_0(k3_power(A,C),k3_power(B,C)) ) ) ) ) ), file(power,t36_power), [interesting(0.00)]). fof(t31_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(1,A) = 1 ) ), file(power,t31_power), [interesting(0.00)]). fof(t154_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ ( r1_xreal_0(k7_xcmplx_0(1,A),0) & r1_xreal_0(0,k7_xcmplx_0(1,B)) ) & ~ r1_xreal_0(k7_xcmplx_0(1,B),k7_xcmplx_0(1,A)) & r1_xreal_0(A,B) ) ) ) ), file(real_2,t154_real_2), [interesting(0.00)]). fof(d6_seq_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) <=> ? [B] : ( v1_xreal_0(B) & ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ), file(seq_2,d6_seq_2), [interesting(0.00)]). fof(d7_seq_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) => ! [B] : ( v1_xreal_0(B) => ( B = k1_seq_2(A) <=> ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ) ), file(seq_2,d7_seq_2), [interesting(0.00)]). fof(t133_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ( ~ ( A != 0 & r1_xreal_0(k17_complex1(A),0) ) & ~ ( ~ r1_xreal_0(k17_complex1(A),0) & A = 0 ) ) ) ), file(complex1,t133_complex1), [interesting(0.00)]). fof(t1_scheme1,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) ) ) ) ), file(scheme1,t1_scheme1), [interesting(0.00)]). fof(t54_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_int_1(B) => ~ ( A != 0 & ? [C] : ( v1_int_1(C) & B = k3_xcmplx_0(2,C) ) & k3_power(k4_xcmplx_0(A),B) != k3_power(A,B) ) ) ) ), file(power,t54_power), [interesting(0.00)]). fof(t55_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_int_1(B) => ~ ( A != 0 & ? [C] : ( v1_int_1(C) & B = k2_xcmplx_0(k3_xcmplx_0(2,C),1) ) & k3_power(k4_xcmplx_0(A),B) != k4_xcmplx_0(k3_power(A,B)) ) ) ) ), file(power,t55_power), [interesting(0.00)]). fof(t138_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ), file(complex1,t138_complex1), [interesting(0.00)]). fof(t16_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( A = k22_seq_1(B) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,C) = k18_complex1(k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ) ), file(seq_1,t16_seq_1), [interesting(0.00)]). fof(t28_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(k22_seq_1(A)) & k2_seq_2(k22_seq_1(A)) = 0 ) => ( v4_seq_2(A) & k2_seq_2(A) = 0 ) ) ) ), file(seq_4,t28_seq_4), [interesting(0.00)]). fof(t9_seq_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ~ r1_xreal_0(B,k4_xcmplx_0(A)) & ~ r1_xreal_0(A,B) ) <=> ~ r1_xreal_0(A,k18_complex1(B)) ) ) ) ), file(seq_2,t9_seq_2), [interesting(0.00)]). fof(t70_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(k3_xcmplx_0(C,A),k3_xcmplx_0(B,A)) ) ) ) ) ), file(xreal_1,t70_xreal_1), [interesting(0.00)]). fof(t121_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k6_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k6_xcmplx_0(A,C),B) ) ) ) ), file(xcmplx_1,t121_xcmplx_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(t153_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k6_real_1(k17_complex1(A),k17_complex1(B)) = k17_complex1(k7_xcmplx_0(A,B)) ) ) ), file(complex1,t153_complex1), [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(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(t21_seq_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v4_seq_2(B) => v4_seq_2(k14_seq_1(B,A)) ) ) ) ), file(seq_2,t21_seq_2), [interesting(0.00)]). fof(t22_seq_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v4_seq_2(B) => k2_seq_2(k14_seq_1(B,A)) = k3_xcmplx_0(A,k2_seq_2(B)) ) ) ) ), file(seq_2,t22_seq_2), [interesting(0.00)]). fof(t118_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(A,0) => ( ( r1_xreal_0(1,k7_xcmplx_0(B,A)) => r1_xreal_0(A,B) ) & ( r1_xreal_0(k7_xcmplx_0(B,A),1) => r1_xreal_0(B,A) ) & ( r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) => ( r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(k4_xcmplx_0(B),A) ) ) & ( r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) => ( r1_xreal_0(B,k4_xcmplx_0(A)) & r1_xreal_0(A,k4_xcmplx_0(B)) ) ) ) ) ) ) ), file(real_2,t118_real_2), [interesting(0.00)]). fof(t15_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => k10_seq_1(A,B) = k9_seq_1(A,k17_seq_1(B)) ) ) ), file(seq_1,t15_seq_1), [interesting(0.00)]). fof(t14_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( A = k17_seq_1(B) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,C) = k1_real_1(k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ) ), file(seq_1,t14_seq_1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t39_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => k9_seq_1(A,k10_seq_1(B,C)) = k10_seq_1(k9_seq_1(A,B),C) ) ) ) ), file(seq_1,t39_seq_1), [interesting(0.00)]). fof(t36_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => A != k1_seqm_3(B,C) ) | k2_seq_2(B) = k2_seq_2(A) ) ) ) ) ), file(seq_4,t36_seq_4), [interesting(0.00)]). fof(t31_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ~ ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,B),0) ) & ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,C) => r1_xreal_0(1,k6_real_1(k8_funct_2(k5_numbers,k1_numbers,A,k1_nat_1(C,1)),k8_funct_2(k5_numbers,k1_numbers,A,C))) ) ) ) & v1_series_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t118_real_2,t2_xreal_1,s1_nat_1,t29_nat_1,t9_seq_2,d7_seq_2,t7_series_1]), [file(series_1,t31_series_1),interesting(0.00)]). fof(t5_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ~ ( ~ ( r1_xreal_0(1,B) & r1_xreal_0(0,A) ) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k1_nat_1(k2_nat_1(2,C),1) ) ) => ( k2_newton(k1_power(B,A),B) = A & k1_power(B,k2_newton(A,B)) = A ) ) ) ) ), file(power,t5_power), [interesting(0.00)]). fof(t15_newton,theorem,( ! [A] : ( v4_ordinal2(A) => k3_newton(1,A) = 1 ) ), file(newton,t15_newton), [interesting(0.00)]). fof(t40_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,1) & ~ r1_xreal_0(B,0) & r1_xreal_0(k3_power(A,B),1) ) ) ) ), file(power,t40_power), [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(t33_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ~ ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,A,C)) ) ) & ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(C,D) => r1_xreal_0(1,k8_funct_2(k5_numbers,k1_numbers,B,D)) ) ) ) & v1_series_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t2_xreal_1,t29_nat_1,t2_xreal_1,t5_power,t15_newton,t40_power,t47_power,t5_power,d5_real_1,t29_nat_1,t29_nat_1,t9_seq_2,d7_seq_2,t7_series_1]), [file(series_1,t33_series_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(s1_rcomp_1,theorem, ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ? [B] : ( v1_xreal_0(B) & p1_s1_rcomp_1(A,B) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => p1_s1_rcomp_1(B,k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ), file(rcomp_1,s1_rcomp_1), [interesting(0.00)]). fof(t99_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(1,A) & r1_xreal_0(0,B) ) => r1_xreal_0(1,k12_prepower(A,B)) ) ) ) ), file(prepower,t99_prepower), [interesting(0.00)]). fof(t164_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(1,A) => r1_xreal_0(k7_xcmplx_0(1,A),1) ) ) ), file(real_2,t164_real_2), [interesting(0.00)]). fof(t141_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t141_xreal_1), [interesting(0.00)]). fof(t101_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k7_xcmplx_0(A,k7_xcmplx_0(1,B)) = k3_xcmplx_0(A,B) ) ) ), file(xcmplx_1,t101_xcmplx_1), [interesting(0.00)]). fof(t100_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k3_xcmplx_0(A,k7_xcmplx_0(1,B)) = k7_xcmplx_0(A,B) ) ) ), file(xcmplx_1,t100_xcmplx_1), [interesting(0.00)]). fof(t143_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,B) ) | ( r1_xreal_0(B,A) & ~ r1_xreal_0(0,A) ) ) => ( r1_xreal_0(k7_xcmplx_0(A,B),1) & r1_xreal_0(1,k7_xcmplx_0(B,A)) ) ) ) ) ), file(real_2,t143_real_2), [interesting(0.00)]). fof(t98_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,1) & r1_xreal_0(C,B) ) => ( r1_xreal_0(A,0) | r1_xreal_0(k12_prepower(A,B),k12_prepower(A,C)) ) ) ) ) ) ), file(prepower,t98_prepower), [interesting(0.00)]). fof(t85_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ r1_xreal_0(A,0) => k12_prepower(A,0) = 1 ) ) ), file(prepower,t85_prepower), [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(d14_seqm_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1)),k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ) ), file(seqm_3,d14_seqm_3), [interesting(0.00)]). fof(t38_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => k3_power(k3_power(A,B),C) = k3_power(A,k3_xcmplx_0(B,C)) ) ) ) ) ), file(power,t38_power), [interesting(0.00)]). fof(t33_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(A,0) => k3_power(A,k4_xcmplx_0(B)) = k7_xcmplx_0(1,k3_power(A,B)) ) ) ) ), file(power,t33_power), [interesting(0.00)]). fof(t32_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => k3_power(A,k2_xcmplx_0(B,C)) = k3_xcmplx_0(k3_power(A,B),k3_power(A,C)) ) ) ) ) ), file(power,t32_power), [interesting(0.00)]). fof(t46_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( A != 0 => k3_power(A,B) = k2_newton(A,B) ) ) ) ), file(power,t46_power), [interesting(0.00)]). fof(t105_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ ( ~ r1_xreal_0(k2_xcmplx_0(A,k4_xcmplx_0(B)),0) & ~ r1_xreal_0(0,k6_xcmplx_0(B,A)) & ~ r1_xreal_0(0,k2_xcmplx_0(B,k4_xcmplx_0(A))) & ~ r1_xreal_0(k6_xcmplx_0(A,C),k2_xcmplx_0(B,k4_xcmplx_0(C))) & ~ r1_xreal_0(k2_xcmplx_0(A,k4_xcmplx_0(C)),k6_xcmplx_0(B,C)) & ~ r1_xreal_0(k6_xcmplx_0(C,B),k6_xcmplx_0(C,A)) ) => r1_xreal_0(A,B) ) ) ) ) ), file(real_2,t105_real_2), [interesting(0.00)]). fof(t41_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,1) & ~ r1_xreal_0(0,B) & r1_xreal_0(1,k3_power(A,B)) ) ) ) ), file(power,t41_power), [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(t217_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k7_xcmplx_0(A,2),0) ) ) ), file(xreal_1,t217_xreal_1), [interesting(0.00)]). fof(t8_power,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) ) => r1_xreal_0(0,k1_power(B,A)) ) ) ) ), file(power,t8_power), [interesting(0.00)]). fof(t2_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(A,k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) => r1_xreal_0(A,k2_seq_2(B)) ) ) ) ), file(prepower,t2_prepower), [interesting(0.00)]). fof(t109_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,k4_xcmplx_0(B)) => ( r1_xreal_0(k2_xcmplx_0(A,B),0) & r1_xreal_0(B,k4_xcmplx_0(A)) ) ) ) ) ), file(real_2,t109_real_2), [interesting(0.00)]). fof(d3_prepower,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(1,A) => ! [C] : ( v1_xreal_0(C) => ( ( ~ r1_xreal_0(B,0) => ( C = k4_prepower(A,B) <=> ( k2_newton(C,A) = B & ~ r1_xreal_0(C,0) ) ) ) & ( B = 0 => ( C = k4_prepower(A,B) <=> C = 0 ) ) ) ) ) ) ) ), file(prepower,d3_prepower), [interesting(0.00)]). fof(d1_power,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(0,B) & r1_xreal_0(1,A) ) => k1_power(A,B) = k4_prepower(A,B) ) & ~ ( ~ r1_xreal_0(0,B) & ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & A = k1_nat_1(k2_nat_1(2,C),1) ) & k1_power(A,B) != k4_xcmplx_0(k4_prepower(A,k4_xcmplx_0(B))) ) ) ) ) ), file(power,d1_power), [interesting(0.00)]). fof(t42_power,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,A) & ~ r1_xreal_0(C,0) & r1_xreal_0(k3_power(B,C),k3_power(A,C)) ) ) ) ) ), file(power,t42_power), [interesting(0.00)]). fof(t106_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ ( r1_xreal_0(0,k2_xcmplx_0(A,k4_xcmplx_0(B))) & r1_xreal_0(k6_xcmplx_0(B,A),0) & r1_xreal_0(k2_xcmplx_0(k4_xcmplx_0(A),B),0) & r1_xreal_0(k2_xcmplx_0(B,k4_xcmplx_0(C)),k6_xcmplx_0(A,C)) & r1_xreal_0(k6_xcmplx_0(B,C),k2_xcmplx_0(A,k4_xcmplx_0(C))) & r1_xreal_0(k6_xcmplx_0(C,A),k6_xcmplx_0(C,B)) ) & r1_xreal_0(B,A) ) ) ) ) ), file(real_2,t106_real_2), [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(t121_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) | ( r1_xreal_0(A,0) & r1_xreal_0(B,0) ) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(real_2,t121_real_2), [interesting(0.00)]). fof(t29_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(A,0) = 1 ) ), file(power,t29_power), [interesting(0.00)]). fof(t14_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k6_xcmplx_0(A,A) = 0 ) ), file(xcmplx_1,t14_xcmplx_1), [interesting(0.00)]). fof(t14_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,C) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ) ) ) ), file(seqm_3,t14_seqm_3), [interesting(0.00)]). fof(t66_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(0,C) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t66_xreal_1), [interesting(0.00)]). fof(t12_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,C) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),k2_seq_1(k5_numbers,k1_numbers,A,C)) ) ) ) ) ) ), file(seqm_3,t12_seqm_3), [interesting(0.00)]). fof(t60_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(k4_xcmplx_0(A),0) ) & ~ ( ~ r1_xreal_0(k4_xcmplx_0(A),0) & r1_xreal_0(0,A) ) ) ) ), file(xreal_1,t60_xreal_1), [interesting(0.00)]). fof(t10_seq_4,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(B,A) ) ) ), file(seq_4,t10_seq_4), [interesting(0.00)]). fof(t19_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(1,A) => r1_xreal_0(1,k2_newton(A,B)) ) ) ) ), file(prepower,t19_prepower), [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(t38_series_1,theorem,( $true ), file(series_1,t38_series_1), [interesting(0.00)]). fof(d5_series_1,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v2_series_1(A) <=> v1_series_1(k22_seq_1(A)) ) ) ), file(series_1,d5_series_1), [interesting(0.00)]). fof(t58_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) <=> ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & r1_xreal_0(B,k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,A,D),k8_funct_2(k5_numbers,k1_numbers,A,C)))) ) ) ) ) ) ) ), file(seq_4,t58_seq_4), [interesting(0.00)]). fof(t142_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => r1_xreal_0(k17_complex1(k2_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ), file(complex1,t142_complex1), [interesting(0.00)]). fof(t11_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,C))) ) ) ) ) ), file(seqm_3,t11_seqm_3), [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(t39_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,C) => r1_xreal_0(k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),C),k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),B))),k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,k1_series_1(k22_seq_1(A)),C),k8_funct_2(k5_numbers,k1_numbers,k1_series_1(k22_seq_1(A)),B)))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_xcmplx_1,t7_absvalue,t132_complex1,t132_complex1,t16_seq_1,t19_series_1,d1_series_1,t142_complex1,t9_xreal_1,t2_xreal_1,t11_seqm_3,t50_xreal_1,d1_absvalue,t132_complex1,t9_xreal_1,d1_series_1,t16_seq_1,d1_absvalue,s1_nat_1,t18_int_1]), [file(series_1,t39_series_1),interesting(0.00)]). fof(t41_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,B)) ) & v1_series_1(A) ) => v2_series_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d2_series_1,d1_absvalue,t16_seq_1,d2_series_1,d5_series_1]), [file(series_1,t41_series_1),interesting(0.00)]). fof(t13_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v1_series_1(B) => ( v1_series_1(k14_seq_1(B,A)) & k2_series_1(k14_seq_1(B,A)) = k3_xcmplx_0(A,k2_series_1(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_series_1,t21_seq_2,t12_series_1,d2_series_1,t12_series_1,t22_seq_2]), [file(series_1,t13_series_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(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(t43_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ~ ( ~ r1_xreal_0(A,0) & ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(C,D) => r1_xreal_0(A,k18_complex1(k8_funct_2(k5_numbers,k1_numbers,B,D))) ) ) ) & v4_seq_2(B) & k2_seq_2(B) = 0 ) ) ) ), inference(mizar_proof,[status(thm)],[d7_seq_2,t29_nat_1,t2_xreal_1,t29_nat_1,t2_xreal_1]), [file(series_1,t43_series_1),interesting(0.00)]). fof(t46_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ~ ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,A,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,k22_seq_1(B),C)) ) & ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(C,D) => r1_xreal_0(1,k8_funct_2(k5_numbers,k1_numbers,A,D)) ) ) ) & v1_series_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t2_xreal_1,t132_complex1,t16_seq_1,t19_prepower,t29_nat_1,t2_xreal_1,t5_power,t43_series_1,t7_series_1]), [file(series_1,t46_series_1),interesting(0.00)]). fof(t4_series_1,theorem,( $true ), file(series_1,t4_series_1), [interesting(0.00)]). fof(t5_series_1,theorem,( $true ), file(series_1,t5_series_1), [interesting(0.00)]). fof(t6_series_1,theorem,( $true ), file(series_1,t6_series_1), [interesting(0.00)]).