fof(t65_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => r1_xreal_0(0,k3_xcmplx_0(A,A)) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l95_xreal_1]), [file(xreal_1,t65_xreal_1),interesting(1.00)]). fof(t3_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ! [B] : ( v1_xreal_0(B) => r1_xreal_0(B,A) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t3_xreal_1),interesting(0.98)]). fof(t4_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ! [B] : ( v1_xreal_0(B) => r1_xreal_0(A,B) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t4_xreal_1),interesting(0.98)]). fof(l113_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(A,B) & r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l112_xreal_1,l67_xreal_1,t88_xcmplx_1,l112_xreal_1,l67_xreal_1,d7_xcmplx_0]), [file(xreal_1,l113_xreal_1),interesting(0.97)]). fof(t7_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,A) & ~ r1_xreal_0(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1,l19_xreal_1,d9_xcmplx_0,l14_xreal_1,l19_xreal_1,d9_xcmplx_0]), [file(xreal_1,t7_xreal_1),interesting(0.97)]). fof(l123_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(B,A) => ( r1_xreal_0(0,A) | r1_xreal_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l112_xreal_1,l95_xreal_1,d7_xcmplx_0,l112_xreal_1,l95_xreal_1,d7_xcmplx_0]), [file(xreal_1,l123_xreal_1),interesting(0.96)]). fof(l68_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k5_xcmplx_0(A),0) ) ) ), inference(mizar_proof,[status(thm)],[t203_xcmplx_1,l67_xreal_1,d7_xcmplx_0]), [file(xreal_1,l68_xreal_1),interesting(0.95)]). fof(l215_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,1) & r1_xreal_0(1,k5_xcmplx_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[l68_xreal_1,l19_xreal_1,d7_xcmplx_0]), [file(xreal_1,l215_xreal_1),interesting(0.95)]). fof(t169_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(C,1) => r1_xreal_0(A,k3_xcmplx_0(B,C)) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l139_xreal_1,l105_xreal_1,t60_xcmplx_1,l19_xreal_1,t88_xcmplx_1,t2_xreal_1,l70_xreal_1,t60_xcmplx_1,t7_xreal_1,l19_xreal_1,t88_xcmplx_1]), [file(xreal_1,t169_xreal_1),interesting(0.93)]). fof(t212_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(C,1) => r1_xreal_0(k7_xcmplx_0(A,C),B) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l128_xreal_1,t78_xcmplx_1,t79_xreal_1,t211_xreal_1]), [file(xreal_1,t212_xreal_1),interesting(0.93)]). fof(l24_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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1,l8_xreal_1]), [file(xreal_1,l24_xreal_1),interesting(0.92)]). fof(l25_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k4_xcmplx_0(A),k4_xcmplx_0(B)) => r1_xreal_0(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1]), [file(xreal_1,l25_xreal_1),interesting(0.92)]). fof(t171_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ~ r1_xreal_0(1,C) & ~ r1_xreal_0(A,k3_xcmplx_0(C,B)) ) ) => r1_xreal_0(A,0) ) ) ) ), inference(mizar_proof,[status(thm)],[t157_xreal_1,t85_xreal_1,t133_xreal_1,l134_xreal_1,l127_xreal_1,l217_xreal_1,l127_xreal_1,t157_xreal_1,t85_xreal_1,t79_xcmplx_1,t2_xreal_1,t1_xreal_1,t93_xcmplx_1,t85_xreal_1,l134_xreal_1,l127_xreal_1,t100_xreal_1,t93_xcmplx_1,l70_xreal_1,t2_xreal_1,t2_xreal_1,l134_xreal_1,l127_xreal_1,l218_xreal_1,l127_xreal_1,t157_xreal_1,t85_xreal_1,t79_xcmplx_1,t2_xreal_1,t93_xcmplx_1,t85_xreal_1]), [file(xreal_1,t171_xreal_1),interesting(0.92)]). fof(t28_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k4_xcmplx_0(A),B) => r1_xreal_0(k4_xcmplx_0(B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1,l49_xreal_1]), [file(xreal_1,t28_xreal_1),interesting(0.92)]). fof(t27_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,k4_xcmplx_0(B)) => r1_xreal_0(B,k4_xcmplx_0(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1,l47_xreal_1]), [file(xreal_1,t27_xreal_1),interesting(0.92)]). fof(l128_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,A) & r1_xreal_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l127_xreal_1,l19_xreal_1,t88_xcmplx_1,l127_xreal_1,l19_xreal_1,d7_xcmplx_0]), [file(xreal_1,l128_xreal_1),interesting(0.91)]). fof(t5_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ? [C] : ( v1_xreal_0(C) & ~ r1_xreal_0(C,A) & ~ r1_xreal_0(C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l10_xreal_1,t2_xreal_1,l10_xreal_1,t2_xreal_1]), [file(xreal_1,t5_xreal_1),interesting(0.91)]). fof(l122_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ( r1_xreal_0(A,0) | r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l68_xreal_1,l18_xreal_1,d7_xcmplx_0,l68_xreal_1,l18_xreal_1,d7_xcmplx_0]), [file(xreal_1,l122_xreal_1),interesting(0.90)]). 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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1,l6_xreal_1]), [file(xreal_1,t11_xreal_1),interesting(0.90)]). fof(l10_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) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,l10_xreal_1),interesting(0.90)]). fof(l6_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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xreal_0,l4_xreal_1,d2_xreal_0,d2_arytm_0,d2_arytm_0,t7_arytm_1,d2_xreal_0,d2_arytm_0,d2_arytm_0,d2_arytm_1,t11_arytm_1,t20_arytm_2,t3_arytm_1,d2_xreal_0,d2_arytm_1,l5_xreal_1,t106_zfmisc_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xreal_0,d2_arytm_0,d2_arytm_0,t33_zfmisc_1,t33_zfmisc_1,d2_arytm_1,t3_arytm_1,d2_arytm_1,t16_arytm_1,d2_xreal_0,d2_arytm_1,l5_xreal_1,t106_zfmisc_1,d2_arytm_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_arytm_1,l5_xreal_1,t106_zfmisc_1,t17_arytm_1,d2_xreal_0,d2_xreal_0,d2_arytm_0,d2_arytm_0,t33_zfmisc_1,d2_arytm_1,t3_arytm_1,d2_arytm_1,t17_arytm_1,d2_xreal_0,d2_arytm_1,l5_xreal_1,t106_zfmisc_1,d2_arytm_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_arytm_1,l5_xreal_1,t106_zfmisc_1,t16_arytm_1,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_arytm_0,d2_arytm_0,t33_zfmisc_1,l5_xreal_1,t106_zfmisc_1,d2_arytm_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_arytm_1,l5_xreal_1,t106_zfmisc_1,t11_arytm_1,t20_arytm_2,t3_arytm_1,d2_xreal_0,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_arytm_0,t5_arytm_0,t3_xboole_0,d2_arytm_0,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,t7_arytm_1,l5_xreal_1,t106_zfmisc_1,l5_xreal_1,t106_zfmisc_1,d2_xreal_0,d2_xreal_0]), [file(xreal_1,l6_xreal_1),interesting(0.89)]). fof(l8_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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1]), [file(xreal_1,l8_xreal_1),interesting(0.89)]). fof(t126_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l112_xreal_1,l127_xreal_1]), [file(xreal_1,t126_xreal_1),interesting(0.89)]). fof(l14_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),k2_xcmplx_0(C,B)) => r1_xreal_0(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1]), [file(xreal_1,l14_xreal_1),interesting(0.89)]). fof(l47_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) ) ) ) ), inference(mizar_proof,[status(thm)],[l31_xreal_1]), [file(xreal_1,l47_xreal_1),interesting(0.88)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1]), [file(xreal_1,t50_xreal_1),interesting(0.88)]). fof(l49_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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1]), [file(xreal_1,l49_xreal_1),interesting(0.88)]). fof(l71_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k7_xcmplx_0(A,2),0) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1]), [file(xreal_1,l71_xreal_1),interesting(0.88)]). fof(l55_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(0,k6_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1]), [file(xreal_1,l55_xreal_1),interesting(0.88)]). fof(t6_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ? [C] : ( v1_xreal_0(C) & ~ r1_xreal_0(A,C) & ~ r1_xreal_0(B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1,t2_xreal_1,l14_xreal_1,t2_xreal_1]), [file(xreal_1,t6_xreal_1),interesting(0.88)]). fof(l105_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l25_xreal_1,l70_xreal_1,t189_xcmplx_1,t189_xcmplx_1,l24_xreal_1]), [file(xreal_1,l105_xreal_1),interesting(0.87)]). fof(l112_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & r1_xreal_0(0,k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1]), [file(xreal_1,l112_xreal_1),interesting(0.87)]). fof(l9_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)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1,l6_xreal_1,l8_xreal_1,t1_xreal_1]), [file(xreal_1,l9_xreal_1),interesting(0.87)]). fof(l95_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(C,0) ) => r1_xreal_0(k3_xcmplx_0(B,C),k3_xcmplx_0(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,l18_xreal_1,l25_xreal_1]), [file(xreal_1,l95_xreal_1),interesting(0.87)]). fof(t137_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(0,k7_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1,t49_xcmplx_1]), [file(xreal_1,t137_xreal_1),interesting(0.87)]). fof(t139_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,0) ) => r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1,d7_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t139_xreal_1),interesting(0.87)]). fof(t148_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ r1_xreal_0(A,k6_xcmplx_0(A,1)) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,t148_xreal_1),interesting(0.87)]). fof(t16_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(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,l9_xreal_1]), [file(xreal_1,t16_xreal_1),interesting(0.87)]). fof(t211_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ~ r1_xreal_0(1,C) & ~ r1_xreal_0(A,k7_xcmplx_0(B,C)) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l127_xreal_1,l215_xreal_1,t78_xcmplx_1,t169_xreal_1]), [file(xreal_1,t211_xreal_1),interesting(0.87)]). fof(t213_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(1,A) => r1_xreal_0(k5_xcmplx_0(A),1) ) ) ), inference(mizar_proof,[status(thm)],[l122_xreal_1]), [file(xreal_1,t213_xreal_1),interesting(0.87)]). fof(t15_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(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,l7_xreal_1]), [file(xreal_1,t15_xreal_1),interesting(0.87)]). fof(t88_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(B,A) => ( r1_xreal_0(0,A) | r1_xreal_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l123_xreal_1]), [file(xreal_1,t88_xreal_1),interesting(0.87)]). fof(t89_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(A,B) & r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l113_xreal_1]), [file(xreal_1,t89_xreal_1),interesting(0.87)]). fof(l67_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l25_xreal_1,l19_xreal_1,l24_xreal_1]), [file(xreal_1,l67_xreal_1),interesting(0.86)]). fof(l70_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(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l68_xreal_1,l19_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,l70_xreal_1),interesting(0.86)]). fof(l127_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) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1]), [file(xreal_1,l127_xreal_1),interesting(0.86)]). fof(l106_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(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) & r1_xreal_0(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,l67_xreal_1,t88_xcmplx_1,t88_xcmplx_1]), [file(xreal_1,l106_xreal_1),interesting(0.86)]). fof(l7_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)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1,l6_xreal_1,t2_xreal_1]), [file(xreal_1,l7_xreal_1),interesting(0.86)]). fof(t140_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(k7_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1,d7_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t140_xreal_1),interesting(0.86)]). fof(l29_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k6_xcmplx_0(B,C)) => r1_xreal_0(k2_xcmplx_0(A,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1]), [file(xreal_1,l29_xreal_1),interesting(0.85)]). fof(l28_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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1]), [file(xreal_1,l28_xreal_1),interesting(0.85)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l68_xreal_1,l136_xreal_1,d9_xcmplx_0]), [file(xreal_1,t138_xreal_1),interesting(0.85)]). fof(l31_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k6_xcmplx_0(A,B),C) => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l28_xreal_1]), [file(xreal_1,l31_xreal_1),interesting(0.85)]). fof(l30_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) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1]), [file(xreal_1,l30_xreal_1),interesting(0.85)]). fof(t214_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,1) & r1_xreal_0(1,k5_xcmplx_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[l215_xreal_1]), [file(xreal_1,t214_xreal_1),interesting(0.85)]). fof(l72_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k7_xcmplx_0(A,2)) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,l72_xreal_1),interesting(0.85)]). fof(t42_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(k2_xcmplx_0(A,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t42_xreal_1),interesting(0.84)]). fof(t38_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(A,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(C,k2_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t38_xreal_1),interesting(0.84)]). fof(t39_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(B,C) & r1_xreal_0(C,k2_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t39_xreal_1),interesting(0.84)]). fof(t92_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) => ( r1_xreal_0(0,k5_xcmplx_0(A)) | r1_xreal_0(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l123_xreal_1]), [file(xreal_1,t92_xreal_1),interesting(0.84)]). fof(t94_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,k5_xcmplx_0(A)) & ~ r1_xreal_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) & r1_xreal_0(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[l113_xreal_1]), [file(xreal_1,t94_xreal_1),interesting(0.84)]). fof(t86_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(k3_xcmplx_0(C,A),B) & r1_xreal_0(k7_xcmplx_0(B,A),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1,t90_xcmplx_1]), [file(xreal_1,t86_xreal_1),interesting(0.83)]). fof(t84_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(C,k3_xcmplx_0(B,A)) & r1_xreal_0(B,k7_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1,t90_xcmplx_1]), [file(xreal_1,t84_xreal_1),interesting(0.83)]). fof(t133_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,0) ) => r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,l136_xreal_1,l25_xreal_1]), [file(xreal_1,t133_xreal_1),interesting(0.83)]). fof(t223_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k7_xcmplx_0(A,3)) ) ) ), inference(mizar_proof,[status(thm)],[l127_xreal_1,l14_xreal_1,l14_xreal_1,t2_xreal_1]), [file(xreal_1,t223_xreal_1),interesting(0.83)]). fof(t225_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k7_xcmplx_0(A,4)) ) ) ), inference(mizar_proof,[status(thm)],[l127_xreal_1,l14_xreal_1,l14_xreal_1,l14_xreal_1,t2_xreal_1]), [file(xreal_1,t225_xreal_1),interesting(0.83)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,l25_xreal_1]), [file(xreal_1,t26_xreal_1),interesting(0.83)]). fof(t37_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,C) ) => r1_xreal_0(k2_xcmplx_0(B,A),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1]), [file(xreal_1,t37_xreal_1),interesting(0.83)]). fof(l18_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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xreal_0,l16_xreal_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xreal_0,d3_arytm_0,d3_arytm_0,t8_arytm_1,d2_xreal_0,d3_arytm_0,d3_arytm_0,l5_xreal_1,t106_zfmisc_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xreal_0,d3_arytm_0,d3_arytm_0,t33_zfmisc_1,t33_zfmisc_1,l5_xreal_1,t106_zfmisc_1,t8_arytm_1,d2_xreal_0,d2_xreal_0]), [file(xreal_1,l18_xreal_1),interesting(0.82)]). fof(l19_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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t4_xcmplx_1,d7_xcmplx_0,d7_xcmplx_0,t1_xreal_1]), [file(xreal_1,l19_xreal_1),interesting(0.82)]). fof(t103_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(B,C) & r1_xreal_0(k7_xcmplx_0(A,B),k7_xcmplx_0(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l113_xreal_1,l67_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t103_xreal_1),interesting(0.82)]). fof(l69_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,C) ) => r1_xreal_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l19_xreal_1,t88_xcmplx_1,t88_xcmplx_1]), [file(xreal_1,l69_xreal_1),interesting(0.82)]). fof(t82_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(B,k3_xcmplx_0(C,A)) => ( r1_xreal_0(0,A) | r1_xreal_0(C,k7_xcmplx_0(B,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l106_xreal_1,t90_xcmplx_1]), [file(xreal_1,t82_xreal_1),interesting(0.82)]). fof(t80_xreal_1,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(0,A) | r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l106_xreal_1,t90_xcmplx_1]), [file(xreal_1,t80_xreal_1),interesting(0.82)]). fof(t85_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(k3_xcmplx_0(C,A),B) & r1_xreal_0(C,k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1,t90_xcmplx_1]), [file(xreal_1,t85_xreal_1),interesting(0.82)]). fof(t83_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,k3_xcmplx_0(B,A)) & r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1,t90_xcmplx_1]), [file(xreal_1,t83_xreal_1),interesting(0.82)]). fof(t123_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(0,B) | r1_xreal_0(k7_xcmplx_0(A,C),k7_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l123_xreal_1,l95_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t123_xreal_1),interesting(0.82)]). fof(t12_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(C,B),k6_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l25_xreal_1,l8_xreal_1,l24_xreal_1,t11_xreal_1]), [file(xreal_1,t12_xreal_1),interesting(0.81)]). fof(t215_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(A,k4_xcmplx_0(1)) => r1_xreal_0(k4_xcmplx_0(1),k5_xcmplx_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[l123_xreal_1]), [file(xreal_1,t215_xreal_1),interesting(0.81)]). fof(t216_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(k4_xcmplx_0(1),A) & r1_xreal_0(k5_xcmplx_0(A),k4_xcmplx_0(1)) ) ) ), inference(mizar_proof,[status(thm)],[l113_xreal_1]), [file(xreal_1,t216_xreal_1),interesting(0.81)]). fof(t44_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(0,C) => r1_xreal_0(k2_xcmplx_0(A,C),B) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_xreal_1,l56_xreal_1,l72_xreal_1,l14_xreal_1,l28_xreal_1,l71_xreal_1,l56_xreal_1]), [file(xreal_1,t44_xreal_1),interesting(0.81)]). fof(t101_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(0,B) & ~ r1_xreal_0(B,C) & r1_xreal_0(k7_xcmplx_0(A,C),k7_xcmplx_0(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l113_xreal_1,l19_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t101_xreal_1),interesting(0.80)]). fof(t121_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(C,B) ) => ( r1_xreal_0(0,B) | r1_xreal_0(k7_xcmplx_0(A,B),k7_xcmplx_0(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l123_xreal_1,l18_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t121_xreal_1),interesting(0.80)]). fof(t58_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(0,C) => r1_xreal_0(A,k6_xcmplx_0(B,C)) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_xreal_1,l56_xreal_1,l72_xreal_1,l14_xreal_1,l71_xreal_1,l56_xreal_1]), [file(xreal_1,t58_xreal_1),interesting(0.80)]). fof(t87_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ( r1_xreal_0(A,0) | r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l122_xreal_1]), [file(xreal_1,t87_xreal_1),interesting(0.80)]). fof(t90_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,A) & r1_xreal_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l128_xreal_1]), [file(xreal_1,t90_xreal_1),interesting(0.80)]). fof(t13_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k6_xcmplx_0(B,C)) => r1_xreal_0(C,k6_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l29_xreal_1,l28_xreal_1]), [file(xreal_1,t13_xreal_1),interesting(0.79)]). fof(t147_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(A,B) & r1_xreal_0(k2_xcmplx_0(B,1),A) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1,l10_xreal_1,t2_xreal_1,l14_xreal_1]), [file(xreal_1,t147_xreal_1),interesting(0.79)]). fof(t149_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(A,B) & r1_xreal_0(B,k6_xcmplx_0(A,1)) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1,l10_xreal_1,t2_xreal_1]), [file(xreal_1,t149_xreal_1),interesting(0.79)]). fof(t14_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k6_xcmplx_0(A,B),C) => r1_xreal_0(k6_xcmplx_0(A,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l31_xreal_1,l30_xreal_1]), [file(xreal_1,t14_xreal_1),interesting(0.79)]). fof(t170_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ~ r1_xreal_0(1,C) & ~ r1_xreal_0(k3_xcmplx_0(A,C),B) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l127_xreal_1,l215_xreal_1,d9_xcmplx_0,t83_xreal_1,t169_xreal_1]), [file(xreal_1,t170_xreal_1),interesting(0.79)]). fof(t157_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,1) & r1_xreal_0(k3_xcmplx_0(A,B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1]), [file(xreal_1,t157_xreal_1),interesting(0.79)]). fof(l217_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(0,A) ) => r1_xreal_0(k7_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_xreal_1,t60_xcmplx_1]), [file(xreal_1,l217_xreal_1),interesting(0.79)]). fof(l37_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(k2_xcmplx_0(A,B),k2_xcmplx_0(C,D)) => r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l28_xreal_1,l30_xreal_1]), [file(xreal_1,l37_xreal_1),interesting(0.79)]). 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) ) ) ) ), inference(mizar_proof,[status(thm)],[l10_xreal_1]), [file(xreal_1,t31_xreal_1),interesting(0.79)]). fof(t33_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(0,A) => r1_xreal_0(B,k2_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_xreal_1,l47_xreal_1,l56_xreal_1]), [file(xreal_1,t33_xreal_1),interesting(0.79)]). fof(t45_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(0,A) => r1_xreal_0(k6_xcmplx_0(B,A),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_xreal_1]), [file(xreal_1,t45_xreal_1),interesting(0.79)]). fof(t59_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(C,0) => r1_xreal_0(k6_xcmplx_0(A,C),B) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l47_xreal_1,l72_xreal_1,l14_xreal_1,l31_xreal_1,l71_xreal_1]), [file(xreal_1,t59_xreal_1),interesting(0.79)]). 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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1,l14_xreal_1]), [file(xreal_1,t8_xreal_1),interesting(0.79)]). fof(t127_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,k5_xcmplx_0(A)) & ~ r1_xreal_0(k5_xcmplx_0(B),0) & r1_xreal_0(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t126_xreal_1]), [file(xreal_1,t127_xreal_1),interesting(0.78)]). fof(l218_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(0,B) ) => r1_xreal_0(k7_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l19_xreal_1,t88_xcmplx_1]), [file(xreal_1,l218_xreal_1),interesting(0.78)]). fof(l56_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) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1,l14_xreal_1]), [file(xreal_1,l56_xreal_1),interesting(0.78)]). fof(t34_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,0) => r1_xreal_0(k2_xcmplx_0(A,B),B) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1]), [file(xreal_1,t34_xreal_1),interesting(0.78)]). fof(t43_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(C,0) => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) => r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l47_xreal_1,l72_xreal_1,l14_xreal_1,l71_xreal_1]), [file(xreal_1,t43_xreal_1),interesting(0.78)]). fof(t46_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(B,k6_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l25_xreal_1,l14_xreal_1]), [file(xreal_1,t46_xreal_1),interesting(0.78)]). fof(t47_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,0) => r1_xreal_0(B,k6_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1,l28_xreal_1]), [file(xreal_1,t47_xreal_1),interesting(0.78)]). fof(t48_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(k6_xcmplx_0(B,A),B) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1,l31_xreal_1]), [file(xreal_1,t48_xreal_1),interesting(0.78)]). 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) ) ) ) ), inference(mizar_proof,[status(thm)],[l47_xreal_1]), [file(xreal_1,t52_xreal_1),interesting(0.78)]). fof(t81_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(B,k3_xcmplx_0(C,A)) => ( r1_xreal_0(A,0) | r1_xreal_0(k7_xcmplx_0(B,A),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_xreal_1,t90_xcmplx_1]), [file(xreal_1,t81_xreal_1),interesting(0.77)]). fof(t79_xreal_1,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)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_xreal_1,t90_xcmplx_1]), [file(xreal_1,t79_xreal_1),interesting(0.77)]). fof(t17_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(D,C) & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_xreal_1,l25_xreal_1]), [file(xreal_1,t17_xreal_1),interesting(0.77)]). fof(t217_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k7_xcmplx_0(A,2),0) ) ) ), inference(mizar_proof,[status(thm)],[l71_xreal_1]), [file(xreal_1,t217_xreal_1),interesting(0.77)]). fof(t224_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k7_xcmplx_0(A,3),0) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1]), [file(xreal_1,t224_xreal_1),interesting(0.77)]). fof(t226_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k7_xcmplx_0(A,4),0) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1]), [file(xreal_1,t226_xreal_1),interesting(0.77)]). fof(t32_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(B,k2_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,t32_xreal_1),interesting(0.77)]). fof(t49_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(k6_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,t49_xreal_1),interesting(0.77)]). fof(t51_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(0,k6_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_xreal_1]), [file(xreal_1,t51_xreal_1),interesting(0.77)]). fof(t91_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) => ( r1_xreal_0(k5_xcmplx_0(A),0) | r1_xreal_0(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l122_xreal_1]), [file(xreal_1,t91_xreal_1),interesting(0.77)]). fof(t93_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(k5_xcmplx_0(A),0) & ~ r1_xreal_0(k5_xcmplx_0(B),k5_xcmplx_0(A)) & r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l128_xreal_1]), [file(xreal_1,t93_xreal_1),interesting(0.77)]). fof(t142_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(k7_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1]), [file(xreal_1,t142_xreal_1),interesting(0.76)]). fof(t144_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & r1_xreal_0(0,k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l112_xreal_1]), [file(xreal_1,t144_xreal_1),interesting(0.76)]). fof(t100_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,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(A,C) & ~ r1_xreal_0(D,B) & r1_xreal_0(k3_xcmplx_0(C,D),k3_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,l18_xreal_1,t2_xreal_1]), [file(xreal_1,t100_xreal_1),interesting(0.76)]). fof(t68_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(0,A) & r1_xreal_0(A,B) & r1_xreal_0(0,C) & r1_xreal_0(C,D) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l18_xreal_1,t2_xreal_1]), [file(xreal_1,t68_xreal_1),interesting(0.76)]). fof(t77_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1]), [file(xreal_1,t77_xreal_1),interesting(0.76)]). fof(t102_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(A,C),k7_xcmplx_0(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l128_xreal_1,l67_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t102_xreal_1),interesting(0.75)]). 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)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t10_xreal_1),interesting(0.75)]). fof(t125_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(0,k5_xcmplx_0(A)) ) & ~ ( ~ r1_xreal_0(0,k5_xcmplx_0(A)) & r1_xreal_0(0,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t217_xcmplx_1,l112_xreal_1,t217_xcmplx_1,l112_xreal_1]), [file(xreal_1,t125_xreal_1),interesting(0.75)]). fof(t67_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(C,0) ) => r1_xreal_0(k3_xcmplx_0(B,C),k3_xcmplx_0(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1]), [file(xreal_1,t67_xreal_1),interesting(0.75)]). fof(t71_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1]), [file(xreal_1,t71_xreal_1),interesting(0.75)]). fof(t122_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,C) ) => ( r1_xreal_0(B,0) | r1_xreal_0(k7_xcmplx_0(A,B),k7_xcmplx_0(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l122_xreal_1,l95_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t122_xreal_1),interesting(0.74)]). 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) ) ) ) ), inference(mizar_proof,[status(thm)],[l127_xreal_1]), [file(xreal_1,t141_xreal_1),interesting(0.74)]). fof(t143_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & r1_xreal_0(0,k7_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1]), [file(xreal_1,t143_xreal_1),interesting(0.74)]). fof(t190_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(A,B) & r1_xreal_0(k7_xcmplx_0(B,A),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1,t60_xcmplx_1]), [file(xreal_1,t190_xreal_1),interesting(0.74)]). fof(t192_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(A,0) & ~ r1_xreal_0(A,B) & r1_xreal_0(1,k7_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l105_xreal_1,t60_xcmplx_1]), [file(xreal_1,t192_xreal_1),interesting(0.74)]). 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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l28_xreal_1,l29_xreal_1]), [file(xreal_1,t21_xreal_1),interesting(0.74)]). 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) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l30_xreal_1,l31_xreal_1]), [file(xreal_1,t22_xreal_1),interesting(0.74)]). fof(t75_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,C) ) => r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l106_xreal_1]), [file(xreal_1,t75_xreal_1),interesting(0.74)]). fof(t76_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(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1]), [file(xreal_1,t76_xreal_1),interesting(0.74)]). 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)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1]), [file(xreal_1,t9_xreal_1),interesting(0.74)]). fof(t154_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,1) ) => r1_xreal_0(A,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1]), [file(xreal_1,t154_xreal_1),interesting(0.73)]). fof(t156_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(1,B) ) => r1_xreal_0(k3_xcmplx_0(A,B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1]), [file(xreal_1,t156_xreal_1),interesting(0.73)]). fof(t18_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(k6_xcmplx_0(A,B),k6_xcmplx_0(C,D)) => r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l29_xreal_1,l31_xreal_1,l37_xreal_1]), [file(xreal_1,t18_xreal_1),interesting(0.73)]). fof(t19_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(k6_xcmplx_0(A,B),k6_xcmplx_0(C,D)) => r1_xreal_0(k6_xcmplx_0(D,B),k6_xcmplx_0(C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l29_xreal_1,l31_xreal_1,l37_xreal_1]), [file(xreal_1,t19_xreal_1),interesting(0.73)]). fof(t20_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(k6_xcmplx_0(A,B),k6_xcmplx_0(C,D)) => r1_xreal_0(k6_xcmplx_0(D,C),k6_xcmplx_0(B,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l29_xreal_1,l31_xreal_1,l37_xreal_1]), [file(xreal_1,t20_xreal_1),interesting(0.73)]). fof(t218_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k7_xcmplx_0(A,2)) ) ) ), inference(mizar_proof,[status(thm)],[l72_xreal_1]), [file(xreal_1,t218_xreal_1),interesting(0.73)]). fof(t41_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(B,C) & r1_xreal_0(k2_xcmplx_0(A,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t41_xreal_1),interesting(0.73)]). fof(t53_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(C,k6_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t42_xreal_1,l29_xreal_1]), [file(xreal_1,t53_xreal_1),interesting(0.73)]). fof(t55_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(A,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k6_xcmplx_0(C,A),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_xreal_1,l31_xreal_1]), [file(xreal_1,t55_xreal_1),interesting(0.73)]). fof(t56_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(B,C) & r1_xreal_0(k6_xcmplx_0(C,A),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_xreal_1,l31_xreal_1]), [file(xreal_1,t56_xreal_1),interesting(0.73)]). fof(t120_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,B) & r1_xreal_0(A,C) ) => ( r1_xreal_0(A,0) | r1_xreal_0(k7_xcmplx_0(B,C),k7_xcmplx_0(B,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l68_xreal_1,l68_xreal_1,l18_xreal_1,d7_xcmplx_0,l18_xreal_1,d7_xcmplx_0,l18_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t120_xreal_1),interesting(0.72)]). fof(t124_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k5_xcmplx_0(A),0) ) & ~ ( ~ r1_xreal_0(k5_xcmplx_0(A),0) & r1_xreal_0(A,0) ) ) ) ), inference(mizar_proof,[status(thm)],[l68_xreal_1,t217_xcmplx_1,l127_xreal_1]), [file(xreal_1,t124_xreal_1),interesting(0.72)]). fof(t158_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(1,B) & r1_xreal_0(k3_xcmplx_0(A,B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1]), [file(xreal_1,t158_xreal_1),interesting(0.72)]). fof(t160_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,1) & r1_xreal_0(A,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1]), [file(xreal_1,t160_xreal_1),interesting(0.72)]). fof(t29_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) & k2_xcmplx_0(A,B) = 0 ) => A = 0 ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,t29_xreal_1),interesting(0.72)]). fof(t184_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(B,A) => ( r1_xreal_0(0,A) | r1_xreal_0(1,k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l106_xreal_1,t60_xcmplx_1]), [file(xreal_1,t184_xreal_1),interesting(0.72)]). fof(t186_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,0) ) => r1_xreal_0(k7_xcmplx_0(B,A),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l106_xreal_1,t60_xcmplx_1]), [file(xreal_1,t186_xreal_1),interesting(0.72)]). fof(t188_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(A,B) ) => r1_xreal_0(k7_xcmplx_0(B,A),1) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l67_xreal_1,t88_xcmplx_1]), [file(xreal_1,t188_xreal_1),interesting(0.72)]). fof(t191_xreal_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(1,k7_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l70_xreal_1,t60_xcmplx_1]), [file(xreal_1,t191_xreal_1),interesting(0.72)]). fof(t194_xreal_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(1,k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,t88_xcmplx_1]), [file(xreal_1,t194_xreal_1),interesting(0.72)]). fof(t54_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,C) ) => r1_xreal_0(B,k6_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_xreal_1,l28_xreal_1]), [file(xreal_1,t54_xreal_1),interesting(0.72)]). fof(t78_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(A,B),k7_xcmplx_0(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l68_xreal_1,l68_xreal_1,l19_xreal_1,d7_xcmplx_0,l19_xreal_1,d7_xcmplx_0,l19_xreal_1,d9_xcmplx_0,d9_xcmplx_0]), [file(xreal_1,t78_xreal_1),interesting(0.72)]). fof(t40_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,C) ) => r1_xreal_0(B,k2_xcmplx_0(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1]), [file(xreal_1,t40_xreal_1),interesting(0.71)]). fof(t146_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(k7_xcmplx_0(A,B),0) & ~ ( ~ r1_xreal_0(B,0) & ~ r1_xreal_0(A,0) ) & ~ ( ~ r1_xreal_0(0,B) & ~ r1_xreal_0(0,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d7_xcmplx_0,t139_xreal_1,t140_xreal_1]), [file(xreal_1,t146_xreal_1),interesting(0.70)]). fof(t36_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & r1_xreal_0(k2_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t36_xreal_1),interesting(0.70)]). 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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1]), [file(xreal_1,t66_xreal_1),interesting(0.70)]). 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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1]), [file(xreal_1,t70_xreal_1),interesting(0.70)]). fof(t145_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,k7_xcmplx_0(A,B)) & ~ ( ~ r1_xreal_0(0,B) & ~ r1_xreal_0(A,0) ) & ~ ( ~ r1_xreal_0(B,0) & ~ r1_xreal_0(0,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d7_xcmplx_0,t137_xreal_1,t138_xreal_1]), [file(xreal_1,t145_xreal_1),interesting(0.69)]). fof(t161_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(1,A) & r1_xreal_0(1,B) ) => r1_xreal_0(1,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t2_xreal_1]), [file(xreal_1,t161_xreal_1),interesting(0.69)]). fof(t163_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,1) & r1_xreal_0(1,B) & r1_xreal_0(k3_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,t2_xreal_1]), [file(xreal_1,t163_xreal_1),interesting(0.69)]). fof(t35_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,k2_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_xreal_1]), [file(xreal_1,t35_xreal_1),interesting(0.69)]). fof(t74_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,C) ) => r1_xreal_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_xreal_1]), [file(xreal_1,t74_xreal_1),interesting(0.69)]). fof(t151_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(1,A) & r1_xreal_0(k6_xcmplx_0(1,A),0) ) ) ), inference(mizar_proof,[status(thm)],[l47_xreal_1]), [file(xreal_1,t151_xreal_1),interesting(0.68)]). fof(t61_xreal_1,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) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1]), [file(xreal_1,t61_xreal_1),interesting(0.68)]). fof(t62_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k4_xcmplx_0(A),B) => r1_xreal_0(0,k2_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_xreal_1]), [file(xreal_1,t62_xreal_1),interesting(0.68)]). fof(t63_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(k4_xcmplx_0(B),A) & r1_xreal_0(0,k2_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,t63_xreal_1),interesting(0.68)]). fof(t64_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,k4_xcmplx_0(A)) & r1_xreal_0(k2_xcmplx_0(B,A),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_xreal_1]), [file(xreal_1,t64_xreal_1),interesting(0.68)]). fof(t72_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(0,A) & r1_xreal_0(B,A) & ~ r1_xreal_0(0,C) & ~ r1_xreal_0(C,D) & r1_xreal_0(k3_xcmplx_0(B,D),k3_xcmplx_0(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1,l95_xreal_1,t2_xreal_1]), [file(xreal_1,t72_xreal_1),interesting(0.68)]). fof(t23_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(k2_xcmplx_0(A,B),k2_xcmplx_0(C,D)) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l37_xreal_1,l31_xreal_1,l29_xreal_1]), [file(xreal_1,t23_xreal_1),interesting(0.67)]). fof(t24_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(k2_xcmplx_0(A,B),k6_xcmplx_0(C,D)) => r1_xreal_0(k2_xcmplx_0(A,D),k6_xcmplx_0(C,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l29_xreal_1,l28_xreal_1,l29_xreal_1,l28_xreal_1]), [file(xreal_1,t24_xreal_1),interesting(0.67)]). fof(t25_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(k6_xcmplx_0(A,B),k2_xcmplx_0(C,D)) => r1_xreal_0(k6_xcmplx_0(A,D),k2_xcmplx_0(C,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l31_xreal_1,l30_xreal_1,l31_xreal_1,l30_xreal_1]), [file(xreal_1,t25_xreal_1),interesting(0.67)]). fof(t153_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(1,B) ) => r1_xreal_0(A,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1]), [file(xreal_1,t153_xreal_1),interesting(0.66)]). fof(t155_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,1) ) => r1_xreal_0(k3_xcmplx_0(A,B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1]), [file(xreal_1,t155_xreal_1),interesting(0.66)]). fof(t159_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(1,B) & r1_xreal_0(A,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1]), [file(xreal_1,t159_xreal_1),interesting(0.66)]). fof(t183_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ( r1_xreal_0(A,0) | r1_xreal_0(1,k7_xcmplx_0(B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_xreal_1,t60_xcmplx_1]), [file(xreal_1,t183_xreal_1),interesting(0.66)]). fof(t185_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,B) ) => r1_xreal_0(k7_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l217_xreal_1]), [file(xreal_1,t185_xreal_1),interesting(0.66)]). fof(t187_xreal_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(k7_xcmplx_0(B,A),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l218_xreal_1]), [file(xreal_1,t187_xreal_1),interesting(0.65)]). fof(t189_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,A) & r1_xreal_0(k7_xcmplx_0(B,A),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t88_xcmplx_1]), [file(xreal_1,t189_xreal_1),interesting(0.65)]). fof(t193_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(A,B) & r1_xreal_0(1,k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t88_xcmplx_1]), [file(xreal_1,t193_xreal_1),interesting(0.65)]). 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) ) ) ) ), inference(mizar_proof,[status(thm)],[l56_xreal_1]), [file(xreal_1,t60_xreal_1),interesting(0.65)]). fof(t69_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,0) & r1_xreal_0(B,A) & r1_xreal_0(C,0) & r1_xreal_0(D,C) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,t68_xreal_1]), [file(xreal_1,t69_xreal_1),interesting(0.65)]). fof(t109_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(0,A) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k3_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t86_xreal_1,t75_xcmplx_1,t86_xreal_1]), [file(xreal_1,t109_xreal_1),interesting(0.64)]). fof(t136_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(k3_xcmplx_0(A,B),0) & ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) & ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t133_xreal_1]), [file(xreal_1,t136_xreal_1),interesting(0.63)]). fof(t165_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,k4_xcmplx_0(1)) & r1_xreal_0(B,k4_xcmplx_0(1)) ) => r1_xreal_0(1,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,l24_xreal_1,t2_xreal_1]), [file(xreal_1,t165_xreal_1),interesting(0.63)]). fof(t166_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(k4_xcmplx_0(1),A) & r1_xreal_0(B,k4_xcmplx_0(1)) & r1_xreal_0(k3_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1,l24_xreal_1,t2_xreal_1]), [file(xreal_1,t166_xreal_1),interesting(0.63)]). fof(t57_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( A != B & r1_xreal_0(k6_xcmplx_0(A,B),0) & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l31_xreal_1,l31_xreal_1,t1_xreal_1]), [file(xreal_1,t57_xreal_1),interesting(0.63)]). fof(t98_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(0,A) & r1_xreal_0(0,B) & ~ r1_xreal_0(C,A) & ~ r1_xreal_0(D,B) & r1_xreal_0(k3_xcmplx_0(C,D),k3_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,l18_xreal_1,t2_xreal_1]), [file(xreal_1,t98_xreal_1),interesting(0.63)]). fof(t99_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(0,A) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(C,A) & r1_xreal_0(B,D) & r1_xreal_0(k3_xcmplx_0(C,D),k3_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l19_xreal_1,t2_xreal_1]), [file(xreal_1,t99_xreal_1),interesting(0.63)]). fof(t110_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,0) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k3_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t85_xreal_1,t75_xcmplx_1,t84_xreal_1]), [file(xreal_1,t110_xreal_1),interesting(0.62)]). fof(t111_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(0,A) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k3_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t86_xreal_1,t75_xcmplx_1,t85_xreal_1]), [file(xreal_1,t111_xreal_1),interesting(0.62)]). fof(t112_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(0,A) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(k7_xcmplx_0(D,B),k3_xcmplx_0(C,A)) & r1_xreal_0(k7_xcmplx_0(D,A),k3_xcmplx_0(C,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t80_xreal_1,t86_xreal_1]), [file(xreal_1,t112_xreal_1),interesting(0.62)]). fof(t114_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(0,A) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k7_xcmplx_0(C,B)) & r1_xreal_0(k3_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t82_xreal_1,t84_xreal_1]), [file(xreal_1,t114_xreal_1),interesting(0.62)]). fof(t105_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(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)) => ( r1_xreal_0(0,A) | r1_xreal_0(0,B) | r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t82_xreal_1,t75_xcmplx_1,t82_xreal_1]), [file(xreal_1,t105_xreal_1),interesting(0.60)]). fof(t108_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,0) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k3_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t85_xreal_1,t75_xcmplx_1,t83_xreal_1]), [file(xreal_1,t108_xreal_1),interesting(0.60)]). fof(t116_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(0,A) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(k7_xcmplx_0(D,B),k3_xcmplx_0(C,A)) & r1_xreal_0(k3_xcmplx_0(C,B),k7_xcmplx_0(D,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_xreal_1,t84_xreal_1]), [file(xreal_1,t116_xreal_1),interesting(0.60)]). fof(t117_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,0) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(k7_xcmplx_0(D,B),k3_xcmplx_0(C,A)) & r1_xreal_0(k3_xcmplx_0(C,B),k7_xcmplx_0(D,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t80_xreal_1,t85_xreal_1]), [file(xreal_1,t117_xreal_1),interesting(0.60)]). fof(t118_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(0,A) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k7_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(C,A),k3_xcmplx_0(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t79_xreal_1,t86_xreal_1]), [file(xreal_1,t118_xreal_1),interesting(0.60)]). fof(t119_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,0) & ~ r1_xreal_0(0,B) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k7_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(C,A),k3_xcmplx_0(D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t82_xreal_1,t83_xreal_1]), [file(xreal_1,t119_xreal_1),interesting(0.60)]). fof(l16_xreal_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( A = C & B = D ) => k2_arytm_0(A,B) = k3_xcmplx_0(C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_xcmplx_0,l3_xreal_1,l3_xreal_1,t14_arytm_0,t13_arytm_0,t13_arytm_0,t14_arytm_0,t17_arytm_0,d7_arytm_0]), [file(xreal_1,l16_xreal_1),interesting(0.59)]). fof(t198_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(A,k4_xcmplx_0(B)) ) => r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l67_xreal_1,t88_xcmplx_1,t27_xreal_1]), [file(xreal_1,t198_xreal_1),interesting(0.59)]). fof(t202_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(k4_xcmplx_0(B),A) & r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,t88_xcmplx_1,t28_xreal_1]), [file(xreal_1,t202_xreal_1),interesting(0.59)]). fof(t210_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(A,k4_xcmplx_0(B)) & r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,t88_xcmplx_1,t27_xreal_1]), [file(xreal_1,t210_xreal_1),interesting(0.59)]). fof(l3_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( A = k5_arytm_0(B,C) => ( C = 0 & A = B ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xreal_0,d7_arytm_0,t10_arytm_0,d7_arytm_0]), [file(xreal_1,l3_xreal_1),interesting(0.58)]). fof(l4_xreal_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( A = C & B = D ) => k1_arytm_0(A,B) = k2_xcmplx_0(C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_xcmplx_0,l3_xreal_1,l3_xreal_1,t13_arytm_0,d7_arytm_0]), [file(xreal_1,l4_xreal_1),interesting(0.58)]). fof(t106_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(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)) => ( r1_xreal_0(A,0) | r1_xreal_0(0,B) | r1_xreal_0(k7_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_xreal_1,t75_xcmplx_1,t80_xreal_1]), [file(xreal_1,t106_xreal_1),interesting(0.58)]). fof(t107_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(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)) => ( r1_xreal_0(0,A) | r1_xreal_0(B,0) | r1_xreal_0(k7_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t82_xreal_1,t75_xcmplx_1,t81_xreal_1]), [file(xreal_1,t107_xreal_1),interesting(0.58)]). fof(t113_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,0) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(k7_xcmplx_0(D,B),k3_xcmplx_0(C,A)) & r1_xreal_0(k7_xcmplx_0(D,A),k3_xcmplx_0(C,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_xreal_1,t83_xreal_1]), [file(xreal_1,t113_xreal_1),interesting(0.58)]). fof(t115_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,0) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k7_xcmplx_0(C,B)) & r1_xreal_0(k3_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t79_xreal_1,t85_xreal_1]), [file(xreal_1,t115_xreal_1),interesting(0.58)]). fof(t150_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,k4_xcmplx_0(1)) & r1_xreal_0(k2_xcmplx_0(1,A),0) ) ) ), inference(mizar_proof,[status(thm)],[l9_xreal_1]), [file(xreal_1,t150_xreal_1),interesting(0.58)]). fof(t197_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,k4_xcmplx_0(A)) ) => r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l67_xreal_1,t88_xcmplx_1]), [file(xreal_1,t197_xreal_1),interesting(0.58)]). fof(t201_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,t88_xcmplx_1]), [file(xreal_1,t201_xreal_1),interesting(0.58)]). fof(t206_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k4_xcmplx_0(B),A) => ( r1_xreal_0(0,A) | r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1,t88_xcmplx_1,t28_xreal_1]), [file(xreal_1,t206_xreal_1),interesting(0.58)]). fof(t209_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,k4_xcmplx_0(A)) & r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,t88_xcmplx_1]), [file(xreal_1,t209_xreal_1),interesting(0.58)]). fof(t30_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(B,0) & k2_xcmplx_0(A,B) = 0 ) => A = 0 ) ) ) ), inference(mizar_proof,[status(thm)],[l24_xreal_1,t29_xreal_1]), [file(xreal_1,t30_xreal_1),interesting(0.58)]). fof(t196_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(k4_xcmplx_0(B),A) ) => r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l19_xreal_1,t88_xcmplx_1,t28_xreal_1]), [file(xreal_1,t196_xreal_1),interesting(0.57)]). fof(t200_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(A,k4_xcmplx_0(B)) & r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t88_xcmplx_1,t27_xreal_1]), [file(xreal_1,t200_xreal_1),interesting(0.57)]). fof(t205_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(k4_xcmplx_0(A),B) => ( r1_xreal_0(0,A) | r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l67_xreal_1,t88_xcmplx_1]), [file(xreal_1,t205_xreal_1),interesting(0.57)]). fof(t208_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(k4_xcmplx_0(B),A) & r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t88_xcmplx_1,t28_xreal_1]), [file(xreal_1,t208_xreal_1),interesting(0.57)]). fof(t204_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,k4_xcmplx_0(B)) => ( r1_xreal_0(A,0) | r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,t88_xcmplx_1,t27_xreal_1]), [file(xreal_1,t204_xreal_1),interesting(0.56)]). fof(t104_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(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)) => ( r1_xreal_0(A,0) | r1_xreal_0(B,0) | r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_xreal_1,t75_xcmplx_1,t79_xreal_1]), [file(xreal_1,t104_xreal_1),interesting(0.54)]). fof(t162_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(0,B) & r1_xreal_0(B,1) ) => r1_xreal_0(k3_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t2_xreal_1]), [file(xreal_1,t162_xreal_1),interesting(0.54)]). fof(t164_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(1,A) & r1_xreal_0(0,B) & r1_xreal_0(B,1) & r1_xreal_0(1,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t2_xreal_1]), [file(xreal_1,t164_xreal_1),interesting(0.54)]). fof(t73_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(0,A) & r1_xreal_0(0,B) & r1_xreal_0(0,C) & r1_xreal_0(0,D) & k2_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) = 0 & A != 0 & C != 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l18_xreal_1,t29_xreal_1,t6_xcmplx_1]), [file(xreal_1,t73_xreal_1),interesting(0.54)]). fof(t195_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(k4_xcmplx_0(A),B) ) => r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,l19_xreal_1,t88_xcmplx_1]), [file(xreal_1,t195_xreal_1),interesting(0.52)]). fof(t199_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,k4_xcmplx_0(A)) & r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t88_xcmplx_1]), [file(xreal_1,t199_xreal_1),interesting(0.51)]). fof(t203_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(B,k4_xcmplx_0(A)) => ( r1_xreal_0(A,0) | r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,t88_xcmplx_1]), [file(xreal_1,t203_xreal_1),interesting(0.51)]). fof(t207_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t88_xcmplx_1]), [file(xreal_1,t207_xreal_1),interesting(0.51)]). fof(t152_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(0,B) & r1_xreal_0(B,1) & k3_xcmplx_0(A,B) = 1 ) => A = 1 ) ) ) ), inference(mizar_proof,[status(thm)],[d7_xcmplx_0,l122_xreal_1,t1_xreal_1]), [file(xreal_1,t152_xreal_1),interesting(0.50)]). fof(t167_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(k4_xcmplx_0(1),A) & r1_xreal_0(B,0) & r1_xreal_0(k4_xcmplx_0(1),B) ) => r1_xreal_0(k3_xcmplx_0(A,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,l24_xreal_1,t2_xreal_1]), [file(xreal_1,t167_xreal_1),interesting(0.47)]). fof(t168_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(A,0) & ~ r1_xreal_0(A,k4_xcmplx_0(1)) & r1_xreal_0(B,0) & r1_xreal_0(k4_xcmplx_0(1),B) & r1_xreal_0(1,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l95_xreal_1,l25_xreal_1,t2_xreal_1]), [file(xreal_1,t168_xreal_1),interesting(0.47)]). fof(t219_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(A,k7_xcmplx_0(1,2)) => r1_xreal_0(k6_xcmplx_0(k3_xcmplx_0(2,A),1),0) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l30_xreal_1]), [file(xreal_1,t219_xreal_1),interesting(0.39)]). fof(t220_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(A,k7_xcmplx_0(1,2)) => r1_xreal_0(0,k6_xcmplx_0(1,k3_xcmplx_0(2,A))) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l28_xreal_1]), [file(xreal_1,t220_xreal_1),interesting(0.39)]). fof(t221_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(k7_xcmplx_0(1,2),A) => r1_xreal_0(0,k6_xcmplx_0(k3_xcmplx_0(2,A),1)) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l28_xreal_1]), [file(xreal_1,t221_xreal_1),interesting(0.39)]). fof(t222_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(k7_xcmplx_0(1,2),A) => r1_xreal_0(k6_xcmplx_0(1,k3_xcmplx_0(2,A)),0) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l30_xreal_1]), [file(xreal_1,t222_xreal_1),interesting(0.39)]). fof(t174_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(B,C) ) => r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,C)),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_xreal_1,l18_xreal_1,l7_xreal_1]), [file(xreal_1,t174_xreal_1),interesting(0.38)]). fof(t96_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(0,A) => ( r1_xreal_0(0,k3_xcmplx_0(k6_xcmplx_0(B,A),k2_xcmplx_0(B,A))) | ( ~ r1_xreal_0(B,k4_xcmplx_0(A)) & ~ r1_xreal_0(A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l136_xreal_1,l137_xreal_1,l138_xreal_1,l7_xreal_1,l8_xreal_1,l28_xreal_1,l29_xreal_1]), [file(xreal_1,t96_xreal_1),interesting(0.38)]). fof(t173_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(B,C) ) => r1_xreal_0(B,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l7_xreal_1]), [file(xreal_1,t173_xreal_1),interesting(0.37)]). fof(t95_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(k3_xcmplx_0(k6_xcmplx_0(B,A),k2_xcmplx_0(B,A)),0) ) => ( r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l135_xreal_1,l134_xreal_1,l7_xreal_1,l30_xreal_1,l31_xreal_1,l30_xreal_1]), [file(xreal_1,t95_xreal_1),interesting(0.37)]). fof(t97_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & r1_xreal_0(0,k3_xcmplx_0(k6_xcmplx_0(B,A),k2_xcmplx_0(B,A))) & ~ r1_xreal_0(B,k4_xcmplx_0(A)) & ~ r1_xreal_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l139_xreal_1,l7_xreal_1,l8_xreal_1]), [file(xreal_1,t97_xreal_1),interesting(0.36)]). fof(t177_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(0,A) & r1_xreal_0(A,1) & ~ r1_xreal_0(C,B) & ~ r1_xreal_0(D,B) & r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),C),k3_xcmplx_0(A,D)),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_xreal_1,l19_xreal_1,l47_xreal_1,l19_xreal_1,l9_xreal_1]), [file(xreal_1,t177_xreal_1),interesting(0.35)]). fof(t178_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(0,A) & r1_xreal_0(A,1) & ~ r1_xreal_0(C,B) & ~ r1_xreal_0(C,D) & r1_xreal_0(C,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_xreal_1,l19_xreal_1,l47_xreal_1,l19_xreal_1,l9_xreal_1]), [file(xreal_1,t178_xreal_1),interesting(0.35)]). fof(t179_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,0) & ~ r1_xreal_0(1,A) & r1_xreal_0(B,C) & ~ r1_xreal_0(D,B) & r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),C),k3_xcmplx_0(A,D)),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,l47_xreal_1,l18_xreal_1,l9_xreal_1]), [file(xreal_1,t179_xreal_1),interesting(0.35)]). fof(t180_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,0) & ~ r1_xreal_0(1,A) & ~ r1_xreal_0(C,B) & r1_xreal_0(D,C) & r1_xreal_0(C,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,l47_xreal_1,l19_xreal_1,l9_xreal_1]), [file(xreal_1,t180_xreal_1),interesting(0.35)]). fof(t175_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(0,A) & r1_xreal_0(A,1) & r1_xreal_0(B,C) & r1_xreal_0(B,D) ) => r1_xreal_0(B,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),C),k3_xcmplx_0(A,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t50_xreal_1,l18_xreal_1,l7_xreal_1]), [file(xreal_1,t175_xreal_1),interesting(0.34)]). fof(t176_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(0,A) & r1_xreal_0(A,1) & r1_xreal_0(B,C) & r1_xreal_0(D,C) ) => r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,D)),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_xreal_1,t50_xreal_1,l18_xreal_1,l7_xreal_1]), [file(xreal_1,t176_xreal_1),interesting(0.34)]). fof(t181_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(B,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,C))) ) => ( r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,C)),C) | A = 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,t50_xreal_1,l18_xreal_1,l9_xreal_1]), [file(xreal_1,t181_xreal_1),interesting(0.15)]). fof(t182_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,C)),B) ) => ( r1_xreal_0(C,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,A),B),k3_xcmplx_0(A,C))) | A = 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l19_xreal_1,t50_xreal_1,l18_xreal_1,l9_xreal_1]), [file(xreal_1,t182_xreal_1),interesting(0.15)]). fof(t21_arytm_2,theorem, ( r2_hidden(k12_arytm_3,k2_arytm_2) & r2_hidden(k13_arytm_3,k2_arytm_2) ), file(arytm_2,t21_arytm_2), [interesting(0.00)]). fof(l17_xreal_1,theorem,( m1_subset_1(0,k2_arytm_2) ), inference(mizar_proof,[status(thm)],[t21_arytm_2]), [file(xreal_1,l17_xreal_1),interesting(0.00)]). fof(t217_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k7_xcmplx_0(1,A) = k5_xcmplx_0(A) ) ), file(xcmplx_1,t217_xcmplx_1), [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(d4_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( C = k2_xcmplx_0(A,B) <=> ? [D] : ( m1_subset_1(D,k1_numbers) & ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & A = k5_arytm_0(D,E) & B = k5_arytm_0(F,G) & C = k5_arytm_0(k1_arytm_0(D,F),k1_arytm_0(E,G)) ) ) ) ) ) ) ) ), file(xcmplx_0,d4_xcmplx_0), [interesting(0.00)]). fof(d7_arytm_0,definition,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ( ( B = 0 => k5_arytm_0(A,B) = A ) & ( B != 0 => k5_arytm_0(A,B) = k5_funct_4(k1_numbers,0,k13_arytm_3,A,B) ) ) ) ) ), file(arytm_0,d7_arytm_0), [interesting(0.00)]). fof(t10_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ~ r2_hidden(k5_funct_4(k1_numbers,0,k13_arytm_3,A,B),k1_numbers) ) ) ), file(arytm_0,t10_arytm_0), [interesting(0.00)]). fof(t13_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ( B = 0 => k1_arytm_0(A,B) = A ) ) ) ), file(arytm_0,t13_arytm_0), [interesting(0.00)]). fof(d2_xreal_0,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) => ( r1_xreal_0(A,B) <=> ? [C] : ( m1_subset_1(C,k2_arytm_2) & ? [D] : ( m1_subset_1(D,k2_arytm_2) & A = C & B = D & r1_arytm_2(C,D) ) ) ) ) & ( ( r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( r1_xreal_0(A,B) <=> ? [C] : ( m1_subset_1(C,k2_arytm_2) & ? [D] : ( m1_subset_1(D,k2_arytm_2) & A = k4_tarski(0,C) & B = k4_tarski(0,D) & r1_arytm_2(D,C) ) ) ) ) & ~ ( ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) & ~ ( r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) & ~ ( r1_xreal_0(A,B) <=> ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) ) ) ) ) ) ), file(xreal_0,d2_xreal_0), [interesting(0.00)]). fof(d2_arytm_0,definition,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) => ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = D & B = E & C = k7_arytm_2(D,E) ) ) ) ) & ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = D & B = k4_tarski(0,E) & C = k2_arytm_1(D,E) ) ) ) ) & ( ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = k4_tarski(0,D) & B = E & C = k2_arytm_1(E,D) ) ) ) ) & ~ ( ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) & ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) & ~ ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) & ~ ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = k4_tarski(0,D) & B = k4_tarski(0,E) & C = k4_tarski(0,k7_arytm_2(D,E)) ) ) ) ) ) ) ) ) ), file(arytm_0,d2_arytm_0), [interesting(0.00)]). fof(t7_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( r1_arytm_2(A,B) <=> r1_arytm_2(k7_arytm_2(A,C),k7_arytm_2(B,C)) ) ) ) ) ), file(arytm_1,t7_arytm_1), [interesting(0.00)]). fof(d2_arytm_1,definition,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( r1_arytm_2(B,A) => k2_arytm_1(A,B) = k1_arytm_1(A,B) ) & ( ~ r1_arytm_2(B,A) => k2_arytm_1(A,B) = k4_tarski(k1_xboole_0,k1_arytm_1(B,A)) ) ) ) ) ), file(arytm_1,d2_arytm_1), [interesting(0.00)]). fof(t11_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => r1_arytm_2(k1_arytm_1(A,B),A) ) ) ), file(arytm_1,t11_arytm_1), [interesting(0.00)]). fof(t20_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( A = k7_arytm_2(B,C) => r1_arytm_2(C,A) ) ) ) ) ), file(arytm_2,t20_arytm_2), [interesting(0.00)]). fof(t3_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( ( r1_arytm_2(A,B) & r1_arytm_2(B,C) ) => r1_arytm_2(A,C) ) ) ) ) ), file(arytm_1,t3_arytm_1), [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(l5_xreal_1,theorem,( r2_hidden(k1_xboole_0,k1_tarski(k1_xboole_0)) ), inference(mizar_proof,[status(thm)],[d1_tarski]), [file(xreal_1,l5_xreal_1),interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(t5_arytm_0,theorem,( r1_subset_1(k2_arytm_2,k2_zfmisc_1(k1_tarski(k12_arytm_3),k2_arytm_2)) ), file(arytm_0,t5_arytm_0), [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(t33_zfmisc_1,theorem,( ! [A,B,C,D] : ( k4_tarski(A,B) = k4_tarski(C,D) => ( A = C & B = D ) ) ), file(zfmisc_1,t33_zfmisc_1), [interesting(0.00)]). fof(t16_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( r1_arytm_2(A,B) => r1_arytm_2(k1_arytm_1(C,B),k1_arytm_1(C,A)) ) ) ) ) ), file(arytm_1,t16_arytm_1), [interesting(0.00)]). fof(t17_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( r1_arytm_2(A,B) => r1_arytm_2(k1_arytm_1(A,C),k1_arytm_1(B,C)) ) ) ) ) ), file(arytm_1,t17_arytm_1), [interesting(0.00)]). fof(t203_xcmplx_1,theorem,( k5_xcmplx_0(0) = 0 ), file(xcmplx_1,t203_xcmplx_1), [interesting(0.00)]). fof(d5_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( C = k3_xcmplx_0(A,B) <=> ? [D] : ( m1_subset_1(D,k1_numbers) & ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & A = k5_arytm_0(D,E) & B = k5_arytm_0(F,G) & C = k5_arytm_0(k1_arytm_0(k2_arytm_0(D,F),k3_arytm_0(k2_arytm_0(E,G))),k1_arytm_0(k2_arytm_0(D,G),k2_arytm_0(E,F))) ) ) ) ) ) ) ) ), file(xcmplx_0,d5_xcmplx_0), [interesting(0.00)]). fof(t14_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ( B = 0 => k2_arytm_0(A,B) = 0 ) ) ) ), file(arytm_0,t14_arytm_0), [interesting(0.00)]). fof(t17_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k2_arytm_0(k3_arytm_0(A),B) = k3_arytm_0(k2_arytm_0(A,B)) ) ) ), file(arytm_0,t17_arytm_0), [interesting(0.00)]). fof(d3_arytm_0,definition,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) => ( C = k2_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = D & B = E & C = k8_arytm_2(D,E) ) ) ) ) & ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( A = 0 | ( C = k2_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = D & B = k4_tarski(0,E) & C = k4_tarski(0,k8_arytm_2(D,E)) ) ) ) ) ) & ( ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( B = 0 | ( C = k2_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = k4_tarski(0,D) & B = E & C = k4_tarski(0,k8_arytm_2(E,D)) ) ) ) ) ) & ( ( r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( C = k2_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = k4_tarski(0,D) & B = k4_tarski(0,E) & C = k8_arytm_2(E,D) ) ) ) ) & ~ ( ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) & ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) & A != 0 ) & ~ ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) & B != 0 ) & ~ ( r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) & ~ ( C = k2_arytm_0(A,B) <=> C = 0 ) ) ) ) ) ) ), file(arytm_0,d3_arytm_0), [interesting(0.00)]). fof(t8_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( r1_arytm_2(A,B) => r1_arytm_2(k8_arytm_2(A,C),k8_arytm_2(B,C)) ) ) ) ) ), file(arytm_1,t8_arytm_1), [interesting(0.00)]). fof(t4_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k3_xcmplx_0(B,C)) = k3_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t4_xcmplx_1), [interesting(0.00)]). fof(d7_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( ( A != 0 => ( B = k5_xcmplx_0(A) <=> k3_xcmplx_0(A,B) = 1 ) ) & ( A = 0 => ( B = k5_xcmplx_0(A) <=> B = 0 ) ) ) ) ) ), file(xcmplx_0,d7_xcmplx_0), [interesting(0.00)]). fof(d1_numbers,definition,( k1_numbers = k4_xboole_0(k2_xboole_0(k2_arytm_2,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)),k1_tarski(k4_tarski(0,0))) ), file(numbers,d1_numbers), [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(t4_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( r1_arytm_2(A,B) & r1_arytm_2(B,A) ) => A = B ) ) ) ), file(arytm_1,t4_arytm_1), [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(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 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xreal_0,d1_numbers,d4_xboole_0,d2_xreal_0,d2_xreal_0,t4_arytm_1,t5_arytm_0,t3_xboole_0,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xreal_0,d2_xreal_0,t33_zfmisc_1,t4_arytm_1,d2_xboole_0]), [file(xreal_1,t1_xreal_1),interesting(0.00)]). fof(d9_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ), file(xcmplx_0,d9_xcmplx_0), [interesting(0.00)]). fof(t189_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k7_xcmplx_0(A,k4_xcmplx_0(B)) = k4_xcmplx_0(k7_xcmplx_0(A,B)) ) ) ), file(xcmplx_1,t189_xcmplx_1), [interesting(0.00)]). fof(t88_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ), file(xcmplx_1,t88_xcmplx_1), [interesting(0.00)]). fof(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(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(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) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xreal_0,d1_numbers,d4_xboole_0,d2_xreal_0,d2_xreal_0,t3_arytm_1,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xreal_0,d2_xreal_0,t33_zfmisc_1,t3_arytm_1,d2_xreal_0,d2_xboole_0]), [file(xreal_1,t2_xreal_1),interesting(0.00)]). fof(l138_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_xreal_0(B) & ~ v2_xreal_0(B) & ~ v3_xreal_0(B) ) => 0 = k3_xcmplx_0(B,A) ) ) ), file(xreal_1,l138_xreal_1), [interesting(0.00)]). fof(t128_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) & r1_xreal_0(0,A) ) => 0 = k3_xcmplx_0(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[l138_xreal_1]), [file(xreal_1,t128_xreal_1),interesting(0.00)]). fof(l136_xreal_1,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( ( v1_xreal_0(B) & ~ v3_xreal_0(B) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ), file(xreal_1,l136_xreal_1), [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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l136_xreal_1]), [file(xreal_1,t129_xreal_1),interesting(0.00)]). fof(l137_xreal_1,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v2_xreal_0(A) ) => ! [B] : ( ( v1_xreal_0(B) & ~ v2_xreal_0(B) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ), file(xreal_1,l137_xreal_1), [interesting(0.00)]). fof(t130_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(0,k3_xcmplx_0(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l137_xreal_1]), [file(xreal_1,t130_xreal_1),interesting(0.00)]). fof(l134_xreal_1,theorem,( ! [A] : ( ( v1_xreal_0(A) & v2_xreal_0(A) ) => ! [B] : ( ( v1_xreal_0(B) & v2_xreal_0(B) ) => ~ r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ), file(xreal_1,l134_xreal_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) ) ) ) ), inference(mizar_proof,[status(thm)],[l134_xreal_1]), [file(xreal_1,t131_xreal_1),interesting(0.00)]). fof(l135_xreal_1,theorem,( ! [A] : ( ( v1_xreal_0(A) & v3_xreal_0(A) ) => ! [B] : ( ( v1_xreal_0(B) & v3_xreal_0(B) ) => ~ r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ), file(xreal_1,l135_xreal_1), [interesting(0.00)]). fof(t132_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(k3_xcmplx_0(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[l135_xreal_1]), [file(xreal_1,t132_xreal_1),interesting(0.00)]). fof(l139_xreal_1,theorem,( ! [A] : ( ( v1_xreal_0(A) & v2_xreal_0(A) ) => ! [B] : ( ( v1_xreal_0(B) & v3_xreal_0(B) ) => ~ r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ), file(xreal_1,l139_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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l139_xreal_1]), [file(xreal_1,t134_xreal_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) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l136_xreal_1,l137_xreal_1]), [file(xreal_1,t135_xreal_1),interesting(0.00)]). fof(t49_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k7_xcmplx_0(A,0) = 0 ) ), file(xcmplx_1,t49_xcmplx_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(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(t93_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( A != 0 => k7_xcmplx_0(B,C) = k3_xcmplx_0(k7_xcmplx_0(B,k3_xcmplx_0(C,A)),A) ) ) ) ) ), file(xcmplx_1,t93_xcmplx_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(t172_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(0,B) & r1_xreal_0(0,C) & k2_xcmplx_0(k3_xcmplx_0(A,B),k3_xcmplx_0(k6_xcmplx_0(1,A),C)) = 0 & ~ ( A = 0 & C = 0 ) & ~ ( A = 1 & B = 0 ) & ~ ( B = 0 & C = 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l8_xreal_1,t73_xreal_1]), [file(xreal_1,t172_xreal_1),interesting(0.00)]). fof(t78_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,C),B) ) ) ) ), file(xcmplx_1,t78_xcmplx_1), [interesting(0.00)]). fof(t234_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( B != 0 & ! [C] : ( v1_xcmplx_0(C) => A != k7_xcmplx_0(B,C) ) ) ) ) ), file(xcmplx_1,t234_xcmplx_1), [interesting(0.00)]). fof(t50_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( A != 0 & B != 0 & k7_xcmplx_0(A,B) = 0 ) ) ) ), file(xcmplx_1,t50_xcmplx_1), [interesting(0.00)]). fof(t54_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( k7_xcmplx_0(A,B) != 0 => B = k7_xcmplx_0(A,k7_xcmplx_0(A,B)) ) ) ) ), file(xcmplx_1,t54_xcmplx_1), [interesting(0.00)]). fof(t227_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( B != 0 & ! [C] : ( v1_xreal_0(C) => A != k7_xcmplx_0(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t234_xcmplx_1,t50_xcmplx_1,t54_xcmplx_1]), [file(xreal_1,t227_xreal_1),interesting(0.00)]).