fof(t29_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => k4_topreal9(A,B,B) = k1_struct_0(k15_euclid(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t26_topreal9,t4_topreal9,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t27_topreal9]), [file(topreal9,t29_topreal9),interesting(1.00)]). fof(t36_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ( ( r2_hidden(C,k3_topreal9(A,D,B)) & r2_hidden(E,k3_topreal9(A,D,B)) ) => k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,C,E),k3_topreal9(A,D,B)) = k2_struct_0(k15_euclid(A),C,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_topreal9,t69_enumset1,d3_xboole_0,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,d3_xboole_0,d3_xboole_0,d3_xboole_0,t26_topreal9,d1_xreal_0,d3_topreal1,d3_topreal1,t4_topreal9,d2_tarski,t4_topreal9,d2_tarski,t34_topreal9,d2_tarski,t4_topreal9,d4_xboole_0,t7_topreal9,t9_topreal9,t2_square_1,t127_real_2,t36_euclid,t34_euclid,t88_xcmplx_1,t33_euclid,t30_euclid,t34_euclid,t37_euclid,t88_xcmplx_1,t33_euclid,t31_euclid,d2_tarski,t4_topreal9,d4_xboole_0,t34_topreal9,t7_topreal9,t9_topreal9,d5_real_1,d3_tarski,d10_xboole_0,d3_tarski,d2_tarski,t27_topreal9,t28_topreal9,d3_xboole_0]), [file(topreal9,t36_topreal9),interesting(0.95)]). fof(l28_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k15_euclid(A)))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( C = a_3_4_topreal9(A,B,D) => v1_jordan1(C,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_jordan1,d3_tarski,d3_topreal1,d1_absvalue,t8_toprns_1,t50_xreal_1,d1_absvalue,t66_xreal_1,t8_toprns_1,t132_complex1,t66_xreal_1,t54_euclid,t52_euclid,t33_euclid,t50_euclid,t45_euclid,t30_euclid,t45_euclid,t53_euclid,t49_euclid,t53_euclid,t30_toprns_1,t9_xreal_1,t2_xreal_1,t1_xreal_1,t4_topreal9]), [file(topreal9,l28_topreal9),interesting(0.86)]). fof(t62_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ( ( r2_hidden(D,k5_jgraph_6(A,B,C)) & r2_hidden(E,k5_jgraph_6(A,B,C)) ) => k5_subset_1(u1_struct_0(k15_euclid(2)),k4_topreal9(2,D,E),k5_jgraph_6(A,B,C)) = k2_struct_0(k15_euclid(2),D,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t49_topreal9,t15_topreal9,t36_topreal9]), [file(topreal9,t62_topreal9),interesting(0.86)]). fof(t35_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ( ( r2_hidden(C,k3_topreal9(A,D,B)) & r2_hidden(E,k3_topreal9(A,D,B)) ) => k5_subset_1(u1_struct_0(k15_euclid(A)),k3_topreal1(A,C,E),k3_topreal9(A,D,B)) = k2_struct_0(k15_euclid(A),C,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_topreal9,d3_xboole_0,d4_xboole_0,d3_xboole_0,t19_topreal9,t3_xboole_0,d3_tarski,d10_xboole_0,d3_tarski,d2_tarski,t6_topreal1,d3_xboole_0]), [file(topreal9,t35_topreal9),interesting(0.84)]). fof(t16_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_tarski(k1_topreal9(A,C,B),k2_topreal9(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_topreal9,t14_topreal9,t15_metric_1]), [file(topreal9,t16_topreal9),interesting(0.83)]). fof(t17_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_tarski(k3_topreal9(A,C,B),k2_topreal9(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t15_topreal9,t14_topreal9,t16_metric_1]), [file(topreal9,t17_topreal9),interesting(0.83)]). fof(t34_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ( ( r2_hidden(C,k3_topreal9(A,D,B)) & r2_hidden(E,k3_topreal9(A,D,B)) ) => r1_tarski(k6_subset_1(u1_struct_0(k15_euclid(A)),k3_topreal1(A,C,E),k2_struct_0(k15_euclid(A),C,E)),k1_topreal9(A,D,B)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t69_enumset1,t7_topreal1,t37_xboole_1,t2_xboole_1,d3_tarski,d4_xboole_0,t52_jgraph_1,t25_euclid,t27_euclid,d6_toprns_1,t116_rvsum_1,t9_topreal9,t9_topreal9,d13_euclid,d11_euclid,d13_euclid,d11_euclid,d10_euclid,t53_euclid,t53_euclid,t49_euclid,t9_jordan2c,t50_euclid,t54_euclid,t52_euclid,t33_euclid,d4_square_1,t98_rvsum_1,t119_rvsum_1,t119_rvsum_1,t84_rvsum_1,t117_rvsum_1,t84_rvsum_1,t117_rvsum_1,t5_topreal9,t5_topreal9,d6_toprns_1,d6_toprns_1,t117_rvsum_1,t94_rvsum_1,t94_rvsum_1,t71_rvsum_1,t117_rvsum_1,d1_euclid_2,d2_euclid_2,t17_topreal9,d1_jordan1,t8_topreal9,t4_topreal9,d2_tarski,d4_xboole_0,t131_xreal_1,t92_real_1,t4_topreal9,d2_tarski,d4_xboole_0,t131_xreal_1,t116_rvsum_1,d13_euclid,t6_xcmplx_1,t68_euclid_2,t51_euclid,t9_jordan2c,t52_euclid,d6_toprns_1,d4_square_1,t121_rvsum_1,t59_rvsum_1,d5_real_1]), [file(topreal9,t34_topreal9),interesting(0.82)]). fof(t52_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k3_topreal9(2,k23_euclid(A,B),C) = k5_jgraph_6(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t15_topreal9,t49_topreal9]), [file(topreal9,t52_topreal9),interesting(0.81)]). fof(t31_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(B,k4_topreal9(A,C,D)) => ( B = C | k4_topreal9(A,C,D) = k4_topreal9(A,C,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t26_topreal9,d3_tarski,t26_topreal9,t138_xreal_1,t4_topreal9,t88_xcmplx_1,t34_euclid,t37_euclid,t34_euclid,t30_euclid,t36_euclid,t26_topreal9,d10_xboole_0,t30_topreal9]), [file(topreal9,t31_topreal9),interesting(0.80)]). fof(t50_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k1_topreal9(2,k23_euclid(A,B),C) = k6_jgraph_6(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_topreal9,t48_topreal9]), [file(topreal9,t50_topreal9),interesting(0.80)]). fof(t18_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k4_subset_1(u1_struct_0(k15_euclid(A)),k1_topreal9(A,C,B),k3_topreal9(A,C,B)) = k2_topreal9(A,C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t15_topreal9,t13_topreal9,t14_topreal9,t17_metric_1]), [file(topreal9,t18_topreal9),interesting(0.79)]). fof(t60_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ( ( r2_hidden(D,k5_jgraph_6(A,B,C)) & r2_hidden(E,k5_jgraph_6(A,B,C)) ) => r1_tarski(k6_subset_1(u1_struct_0(k15_euclid(2)),k3_topreal1(2,D,E),k2_struct_0(k15_euclid(2),D,E)),k6_jgraph_6(A,B,C)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t50_topreal9,t49_topreal9,t15_topreal9,t34_topreal9]), [file(topreal9,t60_topreal9),interesting(0.75)]). fof(t5_topreal9,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k7_square_1(k12_euclid(A)) = k15_rvsum_1(k11_rvsum_1(A)) ) ), inference(mizar_proof,[status(thm)],[t116_rvsum_1,d4_square_1]), [file(topreal9,t5_topreal9),interesting(0.74)]). fof(t61_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ( ( r2_hidden(D,k5_jgraph_6(A,B,C)) & r2_hidden(E,k5_jgraph_6(A,B,C)) ) => k5_subset_1(u1_struct_0(k15_euclid(2)),k3_topreal1(2,D,E),k5_jgraph_6(A,B,C)) = k2_struct_0(k15_euclid(2),D,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t49_topreal9,t15_topreal9,t35_topreal9]), [file(topreal9,t61_topreal9),interesting(0.74)]). fof(t33_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ( ( r2_hidden(C,k3_topreal9(A,D,B)) & r2_hidden(E,k1_topreal9(A,D,B)) ) => k5_subset_1(u1_struct_0(k15_euclid(A)),k3_topreal1(A,C,E),k3_topreal9(A,D,B)) = k1_struct_0(k15_euclid(A),C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_xboole_0,t52_jgraph_1,d3_xboole_0,t13_topreal3,t9_topreal9,t33_euclid,t37_euclid,t50_euclid,t9_jordan2c,t53_euclid,t49_euclid,t53_euclid,t11_xreal_1,t26_xreal_1,t8_toprns_1,d1_absvalue,t9_topreal9,t8_toprns_1,d1_absvalue,t7_topreal9,t70_xreal_1,t10_xreal_1,t30_toprns_1,t33_euclid,t31_euclid,t33_euclid,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t6_topreal1,d3_xboole_0]), [file(topreal9,t33_topreal9),interesting(0.73)]). fof(t19_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_xboole_0(k1_topreal9(A,C,B),k3_topreal9(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_xboole_0,t9_topreal9,t7_topreal9]), [file(topreal9,t19_topreal9),interesting(0.73)]). fof(t27_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r2_hidden(B,k4_topreal9(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_euclid,t33_euclid,t31_euclid]), [file(topreal9,t27_topreal9),interesting(0.72)]). fof(t28_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r2_hidden(B,k4_topreal9(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_euclid,t33_euclid,t31_euclid]), [file(topreal9,t28_topreal9),interesting(0.72)]). fof(t4_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( E = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,B),A,C),k18_euclid(B,A,D)) => ( ~ ( E = C & B != 0 & C != D ) & ( ( B = 0 | C = D ) => E = C ) & ~ ( E = D & B != 1 & C != D ) & ( ( B = 1 | C = D ) => E = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_euclid,t9_jordan2c,t33_euclid,t54_euclid,t44_euclid,t45_euclid,t53_euclid,t35_euclid,t47_euclid,t33_euclid,t33_euclid,t31_euclid,t37_euclid,t33_euclid,t46_euclid,t49_euclid,t33_euclid,t45_euclid,t44_euclid,t37_euclid,t44_euclid,t45_euclid,t53_euclid,t35_euclid,t47_euclid,t33_euclid,t31_euclid,t33_euclid,t37_euclid,t33_euclid]), [file(topreal9,t4_topreal9),interesting(0.71)]). fof(t49_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(2))) => ( D = k23_euclid(A,B) => k11_metric_1(k14_euclid(2),D,C) = k5_jgraph_6(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_topreal3,t45_jgraph_1,t14_metric_1,t43_topreal9,d3_tarski,d10_xboole_0,d3_tarski,t13_topreal3,t45_jgraph_1,t43_topreal9,t14_metric_1]), [file(topreal9,t49_topreal9),interesting(0.71)]). fof(t48_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(2))) => ( D = k23_euclid(A,B) => k9_metric_1(k14_euclid(2),D,C) = k6_jgraph_6(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_topreal3,t45_jgraph_1,t12_metric_1,t45_topreal9,d3_tarski,d10_xboole_0,d3_tarski,t13_topreal3,t45_jgraph_1,t45_topreal9,t12_metric_1]), [file(topreal9,t48_topreal9),interesting(0.71)]). fof(t3_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ~ ( ~ v1_xboole_0(A) & B = k17_euclid(A,B,k5_jordan2c(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_euclid,t2_topreal9,t19_revrot_1]), [file(topreal9,t3_topreal9),interesting(0.69)]). fof(t51_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k2_topreal9(2,k23_euclid(A,B),C) = k7_jgraph_6(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t14_topreal9,t47_topreal9]), [file(topreal9,t51_topreal9),interesting(0.69)]). fof(t55_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k4_subset_1(u1_struct_0(k15_euclid(2)),k6_jgraph_6(A,B,C),k5_jgraph_6(A,B,C)) = k7_jgraph_6(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t49_topreal9,t48_topreal9,t47_topreal9,t17_metric_1]), [file(topreal9,t55_topreal9),interesting(0.69)]). fof(t47_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(2))) => ( D = k23_euclid(A,B) => k10_metric_1(k14_euclid(2),D,C) = k7_jgraph_6(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_topreal3,t45_jgraph_1,t13_metric_1,t44_topreal9,d3_tarski,d10_xboole_0,d3_tarski,t13_topreal3,t45_jgraph_1,t44_topreal9,t13_metric_1]), [file(topreal9,t47_topreal9),interesting(0.67)]). fof(t54_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => r1_xboole_0(k6_jgraph_6(A,B,C),k5_jgraph_6(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_xboole_0,t43_topreal9,t45_topreal9]), [file(topreal9,t54_topreal9),interesting(0.67)]). fof(t46_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => r1_tarski(k5_jgraph_6(A,B,C),k7_jgraph_6(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t43_topreal9,t44_topreal9]), [file(topreal9,t46_topreal9),interesting(0.66)]). fof(t53_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => r1_tarski(k6_jgraph_6(A,B,C),k7_jgraph_6(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t45_topreal9,t44_topreal9]), [file(topreal9,t53_topreal9),interesting(0.66)]). fof(l29_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k15_euclid(A)))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( C = a_3_5_topreal9(A,B,D) => v1_jordan1(C,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_jordan1,t13_topreal3,t13_topreal9,t28_topreal3]), [file(topreal9,l29_topreal9),interesting(0.65)]). fof(t59_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ( ( r2_hidden(D,k5_jgraph_6(A,B,C)) & r2_hidden(E,k6_jgraph_6(A,B,C)) ) => k5_subset_1(u1_struct_0(k15_euclid(2)),k3_topreal1(2,D,E),k5_jgraph_6(A,B,C)) = k1_struct_0(k15_euclid(2),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t49_topreal9,t15_topreal9,t48_topreal9,t13_topreal9,t33_topreal9]), [file(topreal9,t59_topreal9),interesting(0.64)]). fof(t24_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(A))) => ! [G] : ( m1_subset_1(G,u1_struct_0(k15_euclid(A))) => ( ( k2_xcmplx_0(B,C) = 1 & k3_real_1(k18_complex1(B),k18_complex1(C)) = 1 & r2_hidden(E,k2_topreal9(A,F,D)) & r2_hidden(G,k1_topreal9(A,F,D)) ) => ( C = 0 | r2_hidden(k17_euclid(A,k18_euclid(B,A,E),k18_euclid(C,A,G)),k1_topreal9(A,F,D)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t37_euclid,t33_euclid,t9_jordan2c,t50_euclid,t9_jordan2c,t49_euclid,t53_euclid,t53_euclid,d1_xreal_0,d1_xreal_0,t132_complex1,t133_complex1,t7_topreal9,t8_topreal9,t28_toprns_1,t66_xreal_1,t70_xreal_1,t10_xreal_1,t8_toprns_1,t8_toprns_1,t30_toprns_1,t2_xreal_1,t28_toprns_1]), [file(topreal9,t24_topreal9),interesting(0.64)]). fof(t32_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_tarski(k3_topreal1(A,B,C),k4_topreal9(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t52_jgraph_1]), [file(topreal9,t32_topreal9),interesting(0.57)]). fof(t12_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k3_topreal9(A,k16_euclid(A),B)) => k5_toprns_1(A,C) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_topreal9,t13_jordan2c]), [file(topreal9,t12_topreal9),interesting(0.55)]). fof(t10_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ~ ( r2_hidden(C,k1_topreal9(A,k16_euclid(A),B)) & r1_xreal_0(B,k5_toprns_1(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_topreal9,t13_jordan2c]), [file(topreal9,t10_topreal9),interesting(0.54)]). fof(t11_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k2_topreal9(A,k16_euclid(A),B)) => r1_xreal_0(k5_toprns_1(A,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_topreal9,t13_jordan2c]), [file(topreal9,t11_topreal9),interesting(0.54)]). fof(t26_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( r2_hidden(D,k4_topreal9(A,B,C)) <=> ? [E] : ( v1_xreal_0(E) & D = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,E),A,B),k18_euclid(E,A,C)) & r1_xreal_0(0,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xreal_0]), [file(topreal9,t26_topreal9),interesting(0.52)]). fof(t25_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A))) & v1_topreal9(B,A) & v2_topreal9(B,A) & m2_relset_1(B,u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A))) ) => ! [C] : ( ( v1_jordan1(C,A) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k15_euclid(A)))) ) => v1_jordan1(k4_pre_topc(k15_euclid(A),k15_euclid(A),B,C),A) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_jordan1,t116_funct_2,t116_funct_2,d3_topreal1,d3_topreal1,d3_tarski,d1_jordan1,d5_topreal9,d4_topreal9,d4_topreal9,t43_funct_2]), [file(topreal9,t25_topreal9),interesting(0.51)]). fof(t56_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ( r2_hidden(B,k3_topreal9(2,k16_euclid(2),A)) => k3_real_1(k7_square_1(k21_euclid(B)),k7_square_1(k22_euclid(B))) = k5_square_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_topreal9,t13_jordan2c,t46_jgraph_1]), [file(topreal9,t56_topreal9),interesting(0.48)]). fof(t6_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( ~ v3_struct_0(B) & v6_metric_1(B) & v7_metric_1(B) & v8_metric_1(B) & v9_metric_1(B) & l1_metric_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ~ ( C != D & r2_hidden(C,k10_metric_1(B,E,A)) & r2_hidden(D,k10_metric_1(B,E,A)) & r1_xreal_0(A,0) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t64_topreal6,d1_tarski,t63_topreal6]), [file(topreal9,t6_topreal9),interesting(0.44)]). fof(t38_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(A))) => ! [G] : ( m2_finseq_2(G,k1_numbers,k1_euclid(A)) => ! [H] : ( m2_finseq_2(H,k1_numbers,k1_euclid(A)) => ! [I] : ( m2_finseq_2(I,k1_numbers,k1_euclid(A)) => ~ ( G = k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E)) & H = E & I = F & D != E & r2_hidden(D,k3_topreal9(A,F,B)) & r2_hidden(E,k2_topreal9(A,F,B)) & ! [J] : ( m1_subset_1(J,u1_struct_0(k15_euclid(A))) => ~ ( J != D & k2_struct_0(k15_euclid(A),D,J) = k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,D,E),k3_topreal9(A,F,B)) & ( r2_hidden(E,k3_topreal9(A,F,B)) => J = E ) & ( C = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E))),k20_euclid(A,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E)),F)))),k8_square_1(k1_quin_1(k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))),k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E))),k20_euclid(A,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E)),F))),k6_xcmplx_0(k15_rvsum_1(k11_euclid(A,k8_euclid(A,G,I))),k5_square_1(B))))),k4_real_1(2,k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))))) => ( r2_hidden(E,k3_topreal9(A,F,B)) | J = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,C),A,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E))),k18_euclid(C,A,E)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_topreal9,t17_topreal9,t36_topreal9,d1_absvalue,t13_topreal9,t18_topreal9,d2_xboole_0,t24_topreal9,t50_euclid,t46_euclid,t1_topreal9,t33_euclid,t54_euclid,t53_euclid,t35_euclid,t47_euclid,t37_topreal9,d1_tarski,d3_xboole_0,t26_topreal9,t46_euclid,t36_euclid,t30_euclid,t9_jordan2c,t33_euclid,t34_euclid,t54_euclid,t34_euclid,t37_euclid,t34_euclid,t43_euclid,t45_euclid,t53_euclid,t35_euclid,t47_euclid,t27_topreal9,d2_tarski,t36_euclid,t34_euclid,t34_euclid,t30_euclid,t37_euclid,t8_xreal_1,t138_xreal_1,t26_topreal9,d3_xboole_0,d3_xboole_0,d3_tarski,d10_xboole_0,d3_xboole_0,d3_xboole_0,d1_tarski,d2_tarski,t26_topreal9,t70_xreal_1,t92_real_1,t36_euclid,t34_euclid,t34_euclid,t30_euclid,t37_euclid,t26_topreal9,t8_topreal9,d5_real_1,t33_topreal9,d1_xreal_0,d3_topreal1,d3_xboole_0,d1_tarski,d2_tarski,d3_tarski]), [file(topreal9,t38_topreal9),interesting(0.30)]). fof(t37_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(A))) => ! [G] : ( m2_finseq_2(G,k1_numbers,k1_euclid(A)) => ! [H] : ( m2_finseq_2(H,k1_numbers,k1_euclid(A)) => ! [I] : ( m2_finseq_2(I,k1_numbers,k1_euclid(A)) => ~ ( G = D & H = E & I = F & D != E & r2_hidden(D,k1_topreal9(A,F,B)) & C = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,D),k20_euclid(A,D,F)))),k8_square_1(k1_quin_1(k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))),k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,D),k20_euclid(A,D,F))),k6_xcmplx_0(k15_rvsum_1(k11_euclid(A,k8_euclid(A,G,I))),k5_square_1(B))))),k4_real_1(2,k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))))) & ! [J] : ( m1_subset_1(J,u1_struct_0(k15_euclid(A))) => ~ ( k1_struct_0(k15_euclid(A),J) = k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,D,E),k3_topreal9(A,F,B)) & J = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,C),A,D),k18_euclid(C,A,E)) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_topreal9,t13_topreal3,t14_topreal9,t63_topreal6,t19_euclid,t116_rvsum_1,t82_square_1,t7_topreal9,t12_euclid,d13_euclid,d6_toprns_1,t116_rvsum_1,d4_square_1,t116_rvsum_1,d4_square_1,d13_euclid,d6_toprns_1,t78_square_1,t105_real_2,t128_real_2,d1_quin_1,t131_xreal_1,t134_xreal_1,t72_square_1,t173_real_2,d2_polyeq_1,t16_quin_1,d3_polyeq_1,t11_polyeq_1,t135_xreal_1,d2_polyeq_1,d3_polyeq_1,t26_topreal9,t27_quin_1,t26_toprns_1,d1_xreal_0,t54_euclid,t33_euclid,t9_jordan2c,t49_euclid,t9_jordan2c,t53_euclid,t67_euclid_2,t41_euclid_2,t8_toprns_1,t161_complex1,t1_jgraph_3,t60_xreal_1,d1_tarski,d3_xboole_0,d3_tarski,d10_xboole_0,d3_xboole_0,t26_topreal9,d1_xreal_0,t8_toprns_1,t161_complex1,d3_xboole_0,t9_topreal9,t54_euclid,t33_euclid,t51_euclid,t1_topreal9,t53_euclid,t45_euclid,t44_euclid,t48_euclid,t67_euclid_2,t41_euclid_2,d2_polyeq_1,t5_polyeq_1,d1_tarski,t27_quin_1,d3_tarski]), [file(topreal9,t37_topreal9),interesting(0.25)]). fof(t58_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(2))) => ! [G] : ( m2_finseq_2(G,k1_numbers,k1_euclid(2)) => ! [H] : ( m2_finseq_2(H,k1_numbers,k1_euclid(2)) => ! [I] : ( m2_finseq_2(I,k1_numbers,k1_euclid(2)) => ~ ( G = E & H = F & I = k23_euclid(A,B) & C = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k3_xcmplx_0(2,k2_euclid_2(2,k20_euclid(2,F,E),k20_euclid(2,E,k23_euclid(A,B))))),k8_square_1(k1_quin_1(k15_rvsum_1(k11_euclid(2,k8_euclid(2,H,G))),k3_xcmplx_0(2,k2_euclid_2(2,k20_euclid(2,F,E),k20_euclid(2,E,k23_euclid(A,B)))),k6_xcmplx_0(k15_rvsum_1(k11_euclid(2,k8_euclid(2,G,I))),k5_square_1(D))))),k4_real_1(2,k15_rvsum_1(k11_euclid(2,k8_euclid(2,H,G))))) & E != F & r2_hidden(E,k6_jgraph_6(A,B,D)) & ! [J] : ( m1_subset_1(J,u1_struct_0(k15_euclid(2))) => ~ ( k1_struct_0(k15_euclid(2),J) = k5_subset_1(u1_struct_0(k15_euclid(2)),k4_topreal9(2,E,F),k5_jgraph_6(A,B,D)) & J = k17_euclid(2,k18_euclid(k6_xcmplx_0(1,C),2,E),k18_euclid(C,2,F)) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_topreal9,t52_topreal9,t37_topreal9]), [file(topreal9,t58_topreal9),interesting(0.01)]). fof(d1_jordan1,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k15_euclid(A)))) => ( v1_jordan1(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( ( r2_hidden(C,B) & r2_hidden(D,B) ) => r1_tarski(k3_topreal1(A,C,D),B) ) ) ) ) ) ) ), file(jordan1,d1_jordan1), [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(d3_topreal1,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k1_topreal1(A,B,C) = a_3_0_topreal1(A,B,C) ) ) ) ), file(topreal1,d3_topreal1), [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(t8_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k4_real_1(k18_complex1(B),k5_toprns_1(A,C)) = k5_toprns_1(A,k18_euclid(B,A,C)) ) ) ) ), file(toprns_1,t8_toprns_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(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(t132_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => r1_xreal_0(0,k17_complex1(A)) ) ), file(complex1,t132_complex1), [interesting(0.00)]). fof(t54_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => k18_euclid(k6_xcmplx_0(C,D),A,B) = k20_euclid(A,k18_euclid(C,A,B),k18_euclid(D,A,B)) ) ) ) ) ), file(euclid,t54_euclid), [interesting(0.00)]). fof(t52_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( B = k20_euclid(A,k17_euclid(A,B,C),C) & B = k17_euclid(A,k20_euclid(A,B,C),C) ) ) ) ) ), file(euclid,t52_euclid), [interesting(0.00)]). fof(t33_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ( k18_euclid(1,A,B) = B & k18_euclid(0,A,B) = k16_euclid(A) ) ) ) ), file(euclid,t33_euclid), [interesting(0.00)]). fof(t50_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,k17_euclid(A,C,D)) = k20_euclid(A,k20_euclid(A,B,C),D) ) ) ) ) ), file(euclid,t50_euclid), [interesting(0.00)]). fof(t45_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,C) = k17_euclid(A,B,k19_euclid(A,C)) ) ) ) ), file(euclid,t45_euclid), [interesting(0.00)]). fof(t30_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k17_euclid(A,k17_euclid(A,B,C),D) = k17_euclid(A,B,k17_euclid(A,C,D)) ) ) ) ) ), file(euclid,t30_euclid), [interesting(0.00)]). fof(t53_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( v1_xreal_0(D) => k18_euclid(D,A,k20_euclid(A,B,C)) = k20_euclid(A,k18_euclid(D,A,B),k18_euclid(D,A,C)) ) ) ) ) ), file(euclid,t53_euclid), [interesting(0.00)]). fof(t49_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k17_euclid(A,B,k20_euclid(A,C,D)) = k20_euclid(A,k17_euclid(A,B,C),D) ) ) ) ) ), file(euclid,t49_euclid), [interesting(0.00)]). fof(t30_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_xreal_0(k5_toprns_1(A,k17_euclid(A,B,C)),k3_real_1(k5_toprns_1(A,B),k5_toprns_1(A,C))) ) ) ) ), file(toprns_1,t30_toprns_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(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(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(t46_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,B) = k16_euclid(A) ) ) ), file(euclid,t46_euclid), [interesting(0.00)]). fof(t9_jordan2c,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,k17_euclid(A,B,C),D) = k17_euclid(A,k20_euclid(A,B,D),C) ) ) ) ) ), file(jordan2c,t9_jordan2c), [interesting(0.00)]). fof(t44_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ( k19_euclid(A,k18_euclid(C,A,B)) = k18_euclid(k4_xcmplx_0(C),A,B) & k19_euclid(A,k18_euclid(C,A,B)) = k18_euclid(C,A,k19_euclid(A,B)) ) ) ) ) ), file(euclid,t44_euclid), [interesting(0.00)]). fof(t35_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ~ ( k18_euclid(C,A,B) = k16_euclid(A) & C != 0 & B != k16_euclid(A) ) ) ) ) ), file(euclid,t35_euclid), [interesting(0.00)]). fof(t47_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( k20_euclid(A,B,C) = k16_euclid(A) => B = C ) ) ) ) ), file(euclid,t47_euclid), [interesting(0.00)]). fof(t31_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ( k17_euclid(A,k16_euclid(A),B) = B & k17_euclid(A,B,k16_euclid(A)) = B ) ) ) ), file(euclid,t31_euclid), [interesting(0.00)]). fof(t37_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => k18_euclid(k2_xcmplx_0(C,D),A,B) = k17_euclid(A,k18_euclid(C,A,B),k18_euclid(D,A,B)) ) ) ) ) ), file(euclid,t37_euclid), [interesting(0.00)]). fof(t13_topreal3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => u1_struct_0(k15_euclid(A)) = u1_struct_0(k14_euclid(A)) ) ), file(topreal3,t13_topreal3), [interesting(0.00)]). fof(t12_metric_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( l1_metric_1(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( r2_hidden(D,k9_metric_1(B,C,A)) <=> ( ~ v3_struct_0(B) & ~ r1_xreal_0(A,k2_metric_1(B,C,D)) ) ) ) ) ) ) ), file(metric_1,t12_metric_1), [interesting(0.00)]). fof(t45_jgraph_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k14_euclid(A))) => ( ( D = B & E = C ) => k5_toprns_1(A,k20_euclid(A,B,C)) = k4_metric_1(k14_euclid(A),D,E) ) ) ) ) ) ) ), file(jgraph_1,t45_jgraph_1), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(t7_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k1_topreal9(A,D,B)) <=> ~ r1_xreal_0(B,k5_toprns_1(A,k20_euclid(A,C,D))) ) ) ) ) ) ), file(topreal9,t7_topreal9), [interesting(0.00)]). fof(t13_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(A))) => ( C = D => k9_metric_1(k14_euclid(A),D,B) = k1_topreal9(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t12_metric_1,t45_jgraph_1,d3_tarski,d10_xboole_0,d3_tarski,t13_topreal3,t7_topreal9,t45_jgraph_1,t12_metric_1]), [file(topreal9,t13_topreal9),interesting(0.00)]). fof(t28_topreal3,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(B))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k14_euclid(B))) => ( ( r2_hidden(C,k9_metric_1(k14_euclid(B),E,A)) & r2_hidden(D,k9_metric_1(k14_euclid(B),E,A)) ) => r1_tarski(k3_topreal1(B,C,D),k9_metric_1(k14_euclid(B),E,A)) ) ) ) ) ) ) ), file(topreal3,t28_topreal3), [interesting(0.00)]). fof(t13_jordan2c,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ( k20_euclid(A,B,k16_euclid(A)) = B & k20_euclid(A,k16_euclid(A),B) = k19_euclid(A,B) ) ) ) ), file(jordan2c,t13_jordan2c), [interesting(0.00)]). fof(t8_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k2_topreal9(A,D,B)) <=> r1_xreal_0(k5_toprns_1(A,k20_euclid(A,C,D)),B) ) ) ) ) ) ), file(topreal9,t8_topreal9), [interesting(0.00)]). fof(t9_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k3_topreal9(A,D,B)) <=> k5_toprns_1(A,k20_euclid(A,C,D)) = B ) ) ) ) ) ), file(topreal9,t9_topreal9), [interesting(0.00)]). fof(t20_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ~ ( ~ v1_xboole_0(k1_topreal9(A,C,B)) & r1_xreal_0(B,0) ) ) ) ) ), file(topreal9,t20_topreal9), [interesting(0.00)]). fof(t21_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( v1_xboole_0(k1_topreal9(A,C,B)) => r1_xreal_0(B,0) ) ) ) ) ), file(topreal9,t21_topreal9), [interesting(0.00)]). fof(t22_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( ~ v1_xboole_0(k2_topreal9(A,C,B)) => r1_xreal_0(0,B) ) ) ) ) ), file(topreal9,t22_topreal9), [interesting(0.00)]). fof(t23_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ~ ( v1_xboole_0(k2_topreal9(A,C,B)) & r1_xreal_0(0,B) ) ) ) ) ), file(topreal9,t23_topreal9), [interesting(0.00)]). fof(t116_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ~ ( r2_hidden(E,k2_funct_2(A,B,D,C)) & ! [F] : ( m1_subset_1(F,A) => ~ ( r2_hidden(F,C) & E = k1_funct_1(D,F) ) ) ) ) ), file(funct_2,t116_funct_2), [interesting(0.00)]). fof(d5_topreal9,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A))) & m2_relset_1(B,u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A))) ) => ( v2_topreal9(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k8_funct_2(u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A)),B,k17_euclid(A,C,D)) = k17_euclid(A,k8_funct_2(u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A)),B,C),k8_funct_2(u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A)),B,D)) ) ) ) ) ) ), file(topreal9,d5_topreal9), [interesting(0.00)]). fof(d4_topreal9,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A))) & m2_relset_1(B,u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A))) ) => ( v1_topreal9(B,A) <=> ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k8_funct_2(u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A)),B,k18_euclid(C,A,D)) = k18_euclid(C,A,k8_funct_2(u1_struct_0(k15_euclid(A)),u1_struct_0(k15_euclid(A)),B,D)) ) ) ) ) ) ), file(topreal9,d4_topreal9), [interesting(0.00)]). fof(t43_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( B != k1_xboole_0 => ! [E] : ( ? [F] : ( r2_hidden(F,A) & r2_hidden(F,C) & E = k1_funct_1(D,F) ) => r2_hidden(E,k9_relat_1(D,C)) ) ) ) ), file(funct_2,t43_funct_2), [interesting(0.00)]). fof(d1_xreal_0,definition,( ! [A] : ( v1_xreal_0(A) <=> r2_hidden(A,k1_numbers) ) ), file(xreal_0,d1_xreal_0), [interesting(0.00)]). fof(t138_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => r1_xreal_0(0,k7_xcmplx_0(A,B)) ) ) ) ), file(xreal_1,t138_xreal_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(t34_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => k18_euclid(k3_xcmplx_0(C,D),A,B) = k18_euclid(C,A,k18_euclid(D,A,B)) ) ) ) ) ), file(euclid,t34_euclid), [interesting(0.00)]). fof(t36_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( v1_xreal_0(D) => k18_euclid(D,A,k17_euclid(A,B,C)) = k17_euclid(A,k18_euclid(D,A,B),k18_euclid(D,A,C)) ) ) ) ) ), file(euclid,t36_euclid), [interesting(0.00)]). fof(t129_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(xreal_1,t129_xreal_1), [interesting(0.00)]). fof(t30_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(B,k4_topreal9(A,C,D)) => r1_tarski(k4_topreal9(A,C,B),k4_topreal9(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t26_topreal9,d3_tarski,t26_topreal9,t129_xreal_1,t36_euclid,t30_euclid,t34_euclid,t37_euclid,t34_euclid,t26_topreal9]), [file(topreal9,t30_topreal9),interesting(0.00)]). fof(t52_jgraph_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ~ ( r2_hidden(B,k3_topreal1(A,C,D)) & ! [E] : ( m1_subset_1(E,k1_numbers) => ~ ( r1_xreal_0(0,E) & r1_xreal_0(E,1) & B = k17_euclid(A,k18_euclid(k5_real_1(1,E),A,C),k18_euclid(E,A,D)) ) ) ) ) ) ) ) ), file(jgraph_1,t52_jgraph_1), [interesting(0.00)]). fof(t39_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( ~ v1_xboole_0(k3_topreal9(A,C,B)) => r1_xreal_0(0,B) ) ) ) ) ), file(topreal9,t39_topreal9), [interesting(0.00)]). fof(t2_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( k17_euclid(A,B,C) = k17_euclid(A,B,D) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_euclid,t9_jordan2c,t9_jordan2c,t31_euclid,t31_euclid]), [file(topreal9,t2_topreal9),interesting(0.00)]). fof(t19_revrot_1,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => k16_euclid(A) != k5_jordan2c(A) ) ), file(revrot_1,t19_revrot_1), [interesting(0.00)]). fof(t40_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ~ ( ~ v1_xboole_0(A) & v1_xboole_0(k3_topreal9(A,C,B)) & r1_xreal_0(0,B) ) ) ) ) ), file(topreal9,t40_topreal9), [interesting(0.00)]). fof(t7_topreal3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ( k21_euclid(k17_euclid(2,A,B)) = k3_real_1(k21_euclid(A),k21_euclid(B)) & k22_euclid(k17_euclid(2,A,B)) = k3_real_1(k22_euclid(A),k22_euclid(B)) ) ) ) ), file(topreal3,t7_topreal3), [interesting(0.00)]). fof(t9_topreal3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( v1_xreal_0(B) => ( k21_euclid(k18_euclid(B,2,A)) = k3_xcmplx_0(B,k21_euclid(A)) & k22_euclid(k18_euclid(B,2,A)) = k3_xcmplx_0(B,k22_euclid(A)) ) ) ) ), file(topreal3,t9_topreal3), [interesting(0.00)]). fof(t41_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(2))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => k21_euclid(k17_euclid(2,k18_euclid(A,2,C),k18_euclid(B,2,D))) = k2_xcmplx_0(k3_xcmplx_0(A,k21_euclid(C)),k3_xcmplx_0(B,k21_euclid(D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_topreal3,t9_topreal3,t9_topreal3]), [file(topreal9,t41_topreal9),interesting(0.00)]). fof(t42_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(2))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => k22_euclid(k17_euclid(2,k18_euclid(A,2,C),k18_euclid(B,2,D))) = k2_xcmplx_0(k3_xcmplx_0(A,k22_euclid(C)),k3_xcmplx_0(B,k22_euclid(D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_topreal3,t9_topreal3,t9_topreal3]), [file(topreal9,t42_topreal9),interesting(0.00)]). fof(d5_jgraph_6,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k5_jgraph_6(A,B,C) = a_3_0_jgraph_6(A,B,C) ) ) ) ), file(jgraph_6,d5_jgraph_6), [interesting(0.00)]). fof(t43_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ( r2_hidden(D,k5_jgraph_6(A,B,C)) <=> k5_toprns_1(2,k20_euclid(2,D,k23_euclid(A,B))) = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_jgraph_6]), [file(topreal9,t43_topreal9),interesting(0.00)]). fof(d7_jgraph_6,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k7_jgraph_6(A,B,C) = a_3_2_jgraph_6(A,B,C) ) ) ) ), file(jgraph_6,d7_jgraph_6), [interesting(0.00)]). fof(t44_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ( r2_hidden(D,k7_jgraph_6(A,B,C)) <=> r1_xreal_0(k5_toprns_1(2,k20_euclid(2,D,k23_euclid(A,B))),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_jgraph_6]), [file(topreal9,t44_topreal9),interesting(0.00)]). fof(t13_metric_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( l1_metric_1(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( r2_hidden(D,k10_metric_1(B,C,A)) <=> ( ~ v3_struct_0(B) & r1_xreal_0(k2_metric_1(B,C,D),A) ) ) ) ) ) ) ), file(metric_1,t13_metric_1), [interesting(0.00)]). fof(t14_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(A))) => ( C = D => k10_metric_1(k14_euclid(A),D,B) = k2_topreal9(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t13_metric_1,t45_jgraph_1,d3_tarski,d10_xboole_0,d3_tarski,t13_topreal3,t8_topreal9,t45_jgraph_1,t13_metric_1]), [file(topreal9,t14_topreal9),interesting(0.00)]). fof(d6_jgraph_6,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k6_jgraph_6(A,B,C) = a_3_1_jgraph_6(A,B,C) ) ) ) ), file(jgraph_6,d6_jgraph_6), [interesting(0.00)]). fof(t45_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ( r2_hidden(D,k6_jgraph_6(A,B,C)) <=> ~ r1_xreal_0(C,k5_toprns_1(2,k20_euclid(2,D,k23_euclid(A,B)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_jgraph_6]), [file(topreal9,t45_topreal9),interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t14_metric_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( l1_metric_1(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( r2_hidden(D,k11_metric_1(B,C,A)) <=> ( ~ v3_struct_0(B) & k2_metric_1(B,C,D) = A ) ) ) ) ) ) ), file(metric_1,t14_metric_1), [interesting(0.00)]). fof(t17_metric_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( l1_metric_1(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k4_subset_1(u1_struct_0(B),k11_metric_1(B,C,A),k9_metric_1(B,C,A)) = k10_metric_1(B,C,A) ) ) ) ), file(metric_1,t17_metric_1), [interesting(0.00)]). fof(t46_jgraph_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => k7_square_1(k5_toprns_1(2,A)) = k3_real_1(k7_square_1(k21_euclid(A)),k7_square_1(k22_euclid(A))) ) ), file(jgraph_1,t46_jgraph_1), [interesting(0.00)]). fof(t64_topreal6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v6_metric_1(A) & v7_metric_1(A) & v8_metric_1(A) & v9_metric_1(A) & l1_metric_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k10_metric_1(A,B,0) = k1_struct_0(A,B) ) ) ), file(topreal6,t64_topreal6), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t63_topreal6,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( ~ v3_struct_0(B) & v6_metric_1(B) & v8_metric_1(B) & v9_metric_1(B) & l1_metric_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ( ~ r1_xreal_0(0,A) => k10_metric_1(B,C,A) = k1_xboole_0 ) ) ) ) ), file(topreal6,t63_topreal6), [interesting(0.00)]). fof(t57_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ~ ( D != E & r2_hidden(D,k7_jgraph_6(A,B,C)) & r2_hidden(E,k7_jgraph_6(A,B,C)) & r1_xreal_0(C,0) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t47_topreal9,t6_topreal9]), [file(topreal9,t57_topreal9),interesting(0.00)]). fof(t15_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k14_euclid(A))) => ( C = D => k11_metric_1(k14_euclid(A),D,B) = k3_topreal9(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t14_metric_1,t45_jgraph_1,d3_tarski,d10_xboole_0,d3_tarski,t13_topreal3,t9_topreal9,t45_jgraph_1,t14_metric_1]), [file(topreal9,t15_topreal9),interesting(0.00)]). fof(t15_metric_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( l1_metric_1(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => r1_tarski(k9_metric_1(B,C,A),k10_metric_1(B,C,A)) ) ) ) ), file(metric_1,t15_metric_1), [interesting(0.00)]). fof(t19_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k1_euclid(A)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k1_euclid(A)) => ( k12_euclid(k8_euclid(A,B,C)) = 0 <=> B = C ) ) ) ) ), file(euclid,t19_euclid), [interesting(0.00)]). fof(t116_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => r1_xreal_0(0,k15_rvsum_1(k11_rvsum_1(A))) ) ), file(rvsum_1,t116_rvsum_1), [interesting(0.00)]). fof(t82_square_1,theorem,( k9_square_1(0) = 0 ), file(square_1,t82_square_1), [interesting(0.00)]). fof(t12_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k1_euclid(A)) => r1_xreal_0(0,k12_euclid(B)) ) ) ), file(euclid,t12_euclid), [interesting(0.00)]). fof(d13_euclid,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( D = k20_euclid(A,B,C) <=> ! [E] : ( m2_finseq_2(E,k1_numbers,k1_euclid(A)) => ! [F] : ( m2_finseq_2(F,k1_numbers,k1_euclid(A)) => ( ( E = B & F = C ) => D = k8_euclid(A,E,F) ) ) ) ) ) ) ) ) ), file(euclid,d13_euclid), [interesting(0.00)]). fof(d6_toprns_1,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( C = k5_toprns_1(A,B) <=> ? [D] : ( m2_finseq_1(D,k1_numbers) & B = D & C = k12_euclid(D) ) ) ) ) ) ), file(toprns_1,d6_toprns_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(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(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(t128_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & ~ ( ~ r1_xreal_0(0,k7_xcmplx_0(A,B)) & ~ r1_xreal_0(0,k7_xcmplx_0(B,A)) ) ) ) ) ), file(real_2,t128_real_2), [interesting(0.00)]). fof(d1_quin_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k1_quin_1(A,B,C) = k6_xcmplx_0(k5_square_1(B),k3_xcmplx_0(k3_xcmplx_0(4,A),C)) ) ) ) ), file(quin_1,d1_quin_1), [interesting(0.00)]). fof(t131_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(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t131_xreal_1), [interesting(0.00)]). fof(t134_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(0,B) & r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(xreal_1,t134_xreal_1), [interesting(0.00)]). fof(t72_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => r1_xreal_0(0,k5_square_1(A)) ) ), file(square_1,t72_square_1), [interesting(0.00)]). fof(t173_real_2,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(k6_xcmplx_0(B,A),B) ) ) & ~ ( ~ ( r1_xreal_0(B,k2_xcmplx_0(A,B)) & r1_xreal_0(k6_xcmplx_0(B,A),B) ) & r1_xreal_0(0,A) ) ) ) ) ), file(real_2,t173_real_2), [interesting(0.00)]). fof(d2_polyeq_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => k3_polyeq_1(A,B,C,D) = k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,k5_square_1(D)),k3_xcmplx_0(B,D)),C) ) ) ) ) ), file(polyeq_1,d2_polyeq_1), [interesting(0.00)]). fof(t16_quin_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(0,k1_quin_1(A,B,C)) => ( A = 0 | k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,k5_square_1(D)),k3_xcmplx_0(B,D)),C) = k3_xcmplx_0(k3_xcmplx_0(A,k6_xcmplx_0(D,k7_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)))),k6_xcmplx_0(D,k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)))) ) ) ) ) ) ) ), file(quin_1,t16_quin_1), [interesting(0.00)]). fof(d3_polyeq_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => k5_polyeq_1(A,B,C,D) = k3_xcmplx_0(A,k3_xcmplx_0(k6_xcmplx_0(B,C),k6_xcmplx_0(B,D))) ) ) ) ) ), file(polyeq_1,d3_polyeq_1), [interesting(0.00)]). fof(t11_polyeq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => ! [E] : ( v1_xcmplx_0(E) => ( ! [F] : ( v1_xreal_0(F) => k3_polyeq_1(C,D,E,F) = k5_polyeq_1(C,F,A,B) ) => ( C = 0 | ( k7_xcmplx_0(D,C) = k4_xcmplx_0(k2_xcmplx_0(A,B)) & k7_xcmplx_0(E,C) = k3_xcmplx_0(A,B) ) ) ) ) ) ) ) ) ), file(polyeq_1,t11_polyeq_1), [interesting(0.00)]). fof(t135_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,k3_xcmplx_0(A,B)) & ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(0,B) ) & ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) ) ) ) ) ), file(xreal_1,t135_xreal_1), [interesting(0.00)]). fof(t27_quin_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(k1_quin_1(A,B,C),0) & r1_xreal_0(k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)),k7_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A))) ) ) ) ) ), file(quin_1,t27_quin_1), [interesting(0.00)]). fof(t26_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => r1_xreal_0(0,k5_toprns_1(A,B)) ) ) ), file(toprns_1,t26_toprns_1), [interesting(0.00)]). fof(t67_euclid_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k7_square_1(k5_toprns_1(A,k17_euclid(A,B,C))) = k2_xcmplx_0(k2_xcmplx_0(k7_square_1(k5_toprns_1(A,B)),k3_xcmplx_0(2,k2_euclid_2(A,C,B))),k7_square_1(k5_toprns_1(A,C))) ) ) ) ), file(euclid_2,t67_euclid_2), [interesting(0.00)]). fof(t41_euclid_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( v1_xreal_0(D) => k2_euclid_2(A,k18_euclid(D,A,B),C) = k3_xcmplx_0(D,k2_euclid_2(A,B,C)) ) ) ) ) ), file(euclid_2,t41_euclid_2), [interesting(0.00)]). fof(t161_complex1,theorem,( ! [A] : ( v1_xreal_0(A) => k7_square_1(k17_complex1(A)) = k5_square_1(A) ) ), file(complex1,t161_complex1), [interesting(0.00)]). fof(t1_jgraph_3,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( k5_square_1(A) = k5_square_1(B) & A != B & A != k4_xcmplx_0(B) ) ) ) ), file(jgraph_3,t1_jgraph_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(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(t51_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,k20_euclid(A,C,D)) = k17_euclid(A,k20_euclid(A,B,C),D) ) ) ) ) ), file(euclid,t51_euclid), [interesting(0.00)]). fof(t1_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,k20_euclid(A,B,C),D) = k20_euclid(A,k20_euclid(A,B,D),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t45_euclid,t9_jordan2c,t45_euclid]), [file(topreal9,t1_topreal9),interesting(0.00)]). fof(t48_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( k19_euclid(A,k20_euclid(A,B,C)) = k20_euclid(A,C,B) & k19_euclid(A,k20_euclid(A,B,C)) = k17_euclid(A,k19_euclid(A,B),C) ) ) ) ) ), file(euclid,t48_euclid), [interesting(0.00)]). fof(t5_polyeq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(0,k1_quin_1(A,B,C)) => ( A = 0 | ! [D] : ( v1_xreal_0(D) => ~ ( k3_polyeq_1(A,B,C,D) = 0 & D != k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)) & D != k7_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)) ) ) ) ) ) ) ) ), file(polyeq_1,t5_polyeq_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(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(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(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(t6_topreal1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( r2_hidden(B,k1_topreal1(A,B,C)) & r2_hidden(C,k1_topreal1(A,B,C)) ) ) ) ) ), file(topreal1,t6_topreal1), [interesting(0.00)]). fof(t69_enumset1,theorem,( ! [A] : k2_tarski(A,A) = k1_tarski(A) ), file(enumset1,t69_enumset1), [interesting(0.00)]). fof(t7_topreal1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => k1_topreal1(A,B,B) = k1_struct_0(k15_euclid(A),B) ) ) ), file(topreal1,t7_topreal1), [interesting(0.00)]). fof(t37_xboole_1,theorem,( ! [A,B] : ( k4_xboole_0(A,B) = k1_xboole_0 <=> r1_tarski(A,B) ) ), file(xboole_1,t37_xboole_1), [interesting(0.00)]). fof(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(t25_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => u1_struct_0(k15_euclid(A)) = k1_euclid(A) ) ), file(euclid,t25_euclid), [interesting(0.00)]). fof(t27_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => m2_finseq_1(B,k1_numbers) ) ) ), file(euclid,t27_euclid), [interesting(0.00)]). fof(d11_euclid,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(B))) => ( D = k18_euclid(A,B,C) <=> ! [E] : ( m2_finseq_2(E,k1_numbers,k1_euclid(B)) => ( E = C => D = k9_euclid(B,A,E) ) ) ) ) ) ) ) ), file(euclid,d11_euclid), [interesting(0.00)]). fof(d10_euclid,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( D = k17_euclid(A,B,C) <=> ! [E] : ( m2_finseq_2(E,k1_numbers,k1_euclid(A)) => ! [F] : ( m2_finseq_2(F,k1_numbers,k1_euclid(A)) => ( ( E = B & F = C ) => D = k7_euclid(A,E,F) ) ) ) ) ) ) ) ) ), file(euclid,d10_euclid), [interesting(0.00)]). fof(t98_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k4_rvsum_1(A,B,C)) = k4_rvsum_1(A,k4_rvsum_1(A,k12_rvsum_1(A,B),k10_rvsum_1(A,2,k14_rvsum_1(A,B,C))),k12_rvsum_1(A,C)) ) ) ) ), file(rvsum_1,t98_rvsum_1), [interesting(0.00)]). fof(t119_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k15_rvsum_1(k4_rvsum_1(A,B,C)) = k9_binop_2(k15_rvsum_1(B),k15_rvsum_1(C)) ) ) ) ), file(rvsum_1,t119_rvsum_1), [interesting(0.00)]). fof(t84_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k10_rvsum_1(A,B,C)) = k10_rvsum_1(A,k7_square_1(B),k12_rvsum_1(A,C)) ) ) ) ), file(rvsum_1,t84_rvsum_1), [interesting(0.00)]). fof(t117_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k9_rvsum_1(A,B)) = k11_binop_2(A,k15_rvsum_1(B)) ) ) ), file(rvsum_1,t117_rvsum_1), [interesting(0.00)]). fof(t94_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,B,k14_rvsum_1(A,C,D)) = k14_rvsum_1(A,k10_rvsum_1(A,B,C),D) ) ) ) ) ), file(rvsum_1,t94_rvsum_1), [interesting(0.00)]). fof(t71_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,k11_binop_2(B,C),D) = k10_rvsum_1(A,B,k10_rvsum_1(A,C,D)) ) ) ) ) ), file(rvsum_1,t71_rvsum_1), [interesting(0.00)]). fof(d1_euclid_2,definition,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k1_euclid_2(A,B) = k15_rvsum_1(k13_rvsum_1(A,B)) ) ) ), file(euclid_2,d1_euclid_2), [interesting(0.00)]). fof(d2_euclid_2,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( v1_xreal_0(D) => ( D = k2_euclid_2(A,B,C) <=> ? [E] : ( m2_finseq_1(E,k1_numbers) & ? [F] : ( m2_finseq_1(F,k1_numbers) & E = B & F = C & D = k1_euclid_2(E,F) ) ) ) ) ) ) ) ), file(euclid_2,d2_euclid_2), [interesting(0.00)]). fof(t16_metric_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( l1_metric_1(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => r1_tarski(k11_metric_1(B,C,A),k10_metric_1(B,C,A)) ) ) ) ), file(metric_1,t16_metric_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(t92_real_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(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) ) & ~ ( ( ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) ) | ( r1_xreal_0(A,B) & ~ r1_xreal_0(D,C) ) ) & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ) ), file(real_1,t92_real_1), [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(t68_euclid_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k7_square_1(k5_toprns_1(A,k20_euclid(A,B,C))) = k2_xcmplx_0(k6_xcmplx_0(k7_square_1(k5_toprns_1(A,B)),k3_xcmplx_0(2,k2_euclid_2(A,C,B))),k7_square_1(k5_toprns_1(A,C))) ) ) ) ), file(euclid_2,t68_euclid_2), [interesting(0.00)]). fof(t121_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k15_rvsum_1(k12_rvsum_1(A,B)) = 0 => B = k4_finseqop(k1_numbers,A,0) ) ) ) ), file(rvsum_1,t121_rvsum_1), [interesting(0.00)]). fof(t59_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k8_rvsum_1(A,B,C) = k4_finseqop(k1_numbers,A,0) => B = C ) ) ) ) ), file(rvsum_1,t59_rvsum_1), [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(t2_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,1) & r1_xreal_0(1,k7_xcmplx_0(1,A)) ) ) ), file(square_1,t2_square_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(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [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(t28_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k5_toprns_1(A,k20_euclid(A,B,C)) = k5_toprns_1(A,k20_euclid(A,C,B)) ) ) ) ), file(toprns_1,t28_toprns_1), [interesting(0.00)]). fof(t43_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => k19_euclid(A,B) = k18_euclid(k1_real_1(1),A,B) ) ) ), file(euclid,t43_euclid), [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(t63_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(2))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(2))) => ! [G] : ( m2_finseq_2(G,k1_numbers,k1_euclid(2)) => ! [H] : ( m2_finseq_2(H,k1_numbers,k1_euclid(2)) => ! [I] : ( m2_finseq_2(I,k1_numbers,k1_euclid(2)) => ~ ( G = k17_euclid(2,k18_euclid(k6_real_1(1,2),2,E),k18_euclid(k6_real_1(1,2),2,F)) & H = F & I = k23_euclid(A,B) & E != F & r2_hidden(E,k5_jgraph_6(A,B,C)) & r2_hidden(F,k7_jgraph_6(A,B,C)) & ! [J] : ( m1_subset_1(J,u1_struct_0(k15_euclid(2))) => ~ ( J != E & k2_struct_0(k15_euclid(2),E,J) = k5_subset_1(u1_struct_0(k15_euclid(2)),k4_topreal9(2,E,F),k5_jgraph_6(A,B,C)) & ( r2_hidden(F,k3_topreal9(2,k23_euclid(A,B),C)) => J = F ) & ( D = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k3_xcmplx_0(2,k2_euclid_2(2,k20_euclid(2,F,k17_euclid(2,k18_euclid(k6_real_1(1,2),2,E),k18_euclid(k6_real_1(1,2),2,F))),k20_euclid(2,k17_euclid(2,k18_euclid(k6_real_1(1,2),2,E),k18_euclid(k6_real_1(1,2),2,F)),k23_euclid(A,B))))),k8_square_1(k1_quin_1(k15_rvsum_1(k11_euclid(2,k8_euclid(2,H,G))),k3_xcmplx_0(2,k2_euclid_2(2,k20_euclid(2,F,k17_euclid(2,k18_euclid(k6_real_1(1,2),2,E),k18_euclid(k6_real_1(1,2),2,F))),k20_euclid(2,k17_euclid(2,k18_euclid(k6_real_1(1,2),2,E),k18_euclid(k6_real_1(1,2),2,F)),k23_euclid(A,B)))),k6_xcmplx_0(k15_rvsum_1(k11_euclid(2,k8_euclid(2,G,I))),k5_square_1(C))))),k4_real_1(2,k15_rvsum_1(k11_euclid(2,k8_euclid(2,H,G))))) => ( r2_hidden(F,k3_topreal9(2,k23_euclid(A,B),C)) | J = k17_euclid(2,k18_euclid(k6_xcmplx_0(1,D),2,k17_euclid(2,k18_euclid(k6_real_1(1,2),2,E),k18_euclid(k6_real_1(1,2),2,F))),k18_euclid(D,2,F)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_topreal3,t47_topreal9,t14_topreal9,t49_topreal9,t15_topreal9,t38_topreal9]), [file(topreal9,t63_topreal9),interesting(0.00)]).