:: Heron's Formula and Ptolemy's Theorem :: by Marco Riccardi :: :: Received January 10, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies ARYTM, FUNCT_1, ABSVALUE, ARYTM_1, COMPLEX1, SQUARE_1, RELAT_1, PRE_TOPC, ARYTM_3, MCART_1, EUCLID, BOOLE, ORDINAL2, PROJPL_1, INCSP_1, EUCLID_2, CARD_3, XCMPLX_0, INT_1, JGRAPH_6, RAT_1, SUPINF_1, RCOMP_1, SIN_COS, INCPROJ, COMPTRIG, PROB_2, FINSEQ_6, BORSUK_1, TOPS_2, COMPLEX2, TOPREAL1, EUCLID_3, TOPMETR, PCOMPS_1, METRIC_1, SIN_COS6, RFUNCT_2, EUCLID_6; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, VALUED_1, ORDINAL1, ARYTM_3, ARYTM_1, NUMBERS, XREAL_0, SEQ_1, XXREAL_0, EUCLID_2, XXREAL_1, STRUCT_0, PRE_TOPC, FINSEQ_1, SQUARE_1, EUCLID, INT_1, SIN_COS, ARYTM_0, JGRAPH_6, JORDAN2C, COMPTRIG, COMPLEX2, TOPREAL1, TOPMETR, RCOMP_1, EUCLID_3, TOPS_2, XCMPLX_0, COMPLEX1, REAL_1, METRIC_1, PCOMPS_1, SIN_COS6, RFUNCT_2; constructors ARYTM_1, FRAENKEL, NUMBERS, REAL_1, SQUARE_1, BINOP_2, VALUED_0, VALUED_1, COMPLEX1, FINSEQOP, MONOID_0, SEQ_1, EUCLID_2, ENUMSET1, SETFAM_1, XCMPLX_0, XXREAL_0, ORDINAL1, ARYTM_0, RCOMP_1, FINSOP_1, SIN_COS, JGRAPH_6, FINSEQ_4, COMPTRIG, COMPLEX2, TOPMETR, TOPREAL1, EUCLID_3, TOPS_2, JORDAN2C, METRIC_1, PCOMPS_1, SIN_COS6, RFUNCT_2; registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, BINOP_2, MEMBERED, SEQ_1, MONOID_0, STRUCT_0, EUCLID, ARYTM_3, INT_1, ORDINAL1, JGRAPH_6, FINSEQ_4, XCMPLX_0, TOPREAL5, TOPREALA, TOPMETR, SQUARE_1, FUNCT_2, TOPREAL1, PRE_TOPC, TOPREAL2, JORDAN2C, METRIC_1, PCOMPS_1, BORSUK_1, SIN_COS6, RFUNCT_2, VALUED_0, VALUED_1; requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM; definitions XBOOLE_0, TARSKI, SUBSET_1, EUCLID, COMPLEX1, EUCLID_3, SQUARE_1, VALUED_0, VALUED_1; theorems TARSKI, XCMPLX_1, SQUARE_1, FUNCT_1, COMPLEX1, XBOOLE_0, FUNCT_2, EUCLID, COMPLEX2, XREAL_0, EUCLID_2, TOPREAL1, XREAL_1, COMPTRIG, EUCLID_3, SIN_COS, ZFMISC_1, TOPREAL9, XXREAL_0, SPPOL_1, SIN_COS6, XXREAL_1, RCOMP_1, JGRAPH_6, JORDAN5A, JORDAN2C, RELSET_1, TOPS_2, JORDAN6, BORSUK_1, JGRAPH_1, TOPMETR, METRIC_1, UNIFORM1, TOPREAL3, JGRAPH_2, TOPREAL5, PRE_TOPC, RFUNCT_2, XBOOLE_1, PARTFUN1, VALUED_1; schemes FUNCT_1; begin :: Law of Cosines and Meister-Gauss Formula reserve p1,p2,p3,p4,p5,p6,p,pc for Point of TOP-REAL 2; reserve a,b,c,r,s for real number; Lm1: |.p1-p2.| = 0 iff p1=p2 proof hereby assume |.p1-p2.| = 0; then p1-p2=0.REAL 2 by EUCLID_2:64; hence p1=p2 by EUCLID:47; end; assume p1=p2; then p1-p2=0.REAL 2 by EUCLID:46; hence |.p1-p2.| = 0 by EUCLID_2:61; end; Lm2: |.p1-p2.| = |.p2-p1.| proof thus |.p1-p2.| = |.-(p1 - p2).| by EUCLID:13 .= |.p2 - p1.| by EUCLID:48; end; theorem Th1: sin angle(p1,p2,p3) = sin angle(p4,p5,p6) & cos angle(p1,p2,p3) = cos angle(p4,p5,p6) implies angle(p1,p2,p3) = angle(p4,p5,p6) proof assume A1: sin angle(p1,p2,p3) = sin angle(p4,p5,p6) & cos angle(p1,p2,p3) = cos angle(p4,p5,p6); A2: 2*PI*0<=angle(p1,p2,p3) & angle(p1,p2,p3)<2*PI+2*PI*0 by COMPLEX2:84; 2*PI*0<=angle(p4,p5,p6) & angle(p4,p5,p6)<2*PI+2*PI*0 by COMPLEX2:84; hence thesis by A2,A1,SIN_COS6:61; end; theorem Th2: sin angle(p1,p2,p3) = - sin angle(p3,p2,p1) proof per cases; suppose A1: angle(p1,p2,p3)=0; then angle(p3,p2,p1)=0 by EUCLID_3:45; hence thesis by A1,SIN_COS:34; end; suppose angle(p1,p2,p3)<>0; then angle(p3,p2,p1)=2*PI-angle(p1,p2,p3) by EUCLID_3:46; then sin angle(p1,p2,p3) = sin(-angle(p3,p2,p1)+2*PI) .= sin(-angle(p3,p2,p1)) by SIN_COS:84 .= -sin(angle(p3,p2,p1)) by SIN_COS:34; hence thesis; end; end; theorem Th3: cos angle(p1,p2,p3) = cos angle(p3,p2,p1) proof per cases; suppose angle(p1,p2,p3)=0; hence thesis by EUCLID_3:45; end; suppose angle(p1,p2,p3)<>0; then angle(p3,p2,p1)=2*PI-angle(p1,p2,p3) by EUCLID_3:46; then cos angle(p1,p2,p3) = cos(-angle(p3,p2,p1)+2*PI) .= cos(-angle(p3,p2,p1)) by SIN_COS:84 .= cos(angle(p3,p2,p1)) by SIN_COS:34; hence thesis; end; end; Lm3: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+2*PI proof assume A1: angle(p1,p2,p3) = 2*angle(p4,p5,p6)+2*PI; angle(p4,p5,p6)>=0 & angle(p1,p2,p3)<2*PI by COMPLEX2:84; then angle(p4,p5,p6)*2 >= (0 qua Real)*2 by XREAL_1:66; then angle(p4,p5,p6)*2+2*PI>=0+2*PI by XREAL_1:9; hence contradiction by A1,COMPLEX2:84; end; Lm4: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+4*PI proof assume A1: angle(p1,p2,p3) = 2*angle(p4,p5,p6)+4*PI; A2: 4*PI>=2*PI by XREAL_1:66; angle(p4,p5,p6)>=0 & angle(p1,p2,p3)<2*PI by COMPLEX2:84; then angle(p4,p5,p6)*2 >= (0 qua Real)*2 by XREAL_1:66; then angle(p4,p5,p6)*2+4*PI>=0+4*PI by XREAL_1:9; then angle(p4,p5,p6)*2+4*PI>=2*PI by A2,XXREAL_0:2; hence contradiction by A1,COMPLEX2:84; end; Lm5: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-4*PI proof assume A1: angle(p1,p2,p3) = 2*angle(p4,p5,p6)-4*PI; angle(p4,p5,p6)<2*PI & angle(p1,p2,p3)>=0 by COMPLEX2:84; then angle(p4,p5,p6)*2 < 2*PI*2 by XREAL_1:70; then angle(p4,p5,p6)*2-4*PI<4*PI-4*PI by XREAL_1:11; hence contradiction by A1,COMPLEX2:84; end; Lm6: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-6*PI proof assume A1: angle(p1,p2,p3) = 2*angle(p4,p5,p6)-6*PI; A2: PI*(-2)<=(0 qua Real)*(-2); angle(p4,p5,p6)<2*PI & angle(p1,p2,p3)>=0 by COMPLEX2:84; then angle(p4,p5,p6)*2 < 2*PI*2 by XREAL_1:70; then angle(p4,p5,p6)*2-6*PI<4*PI-6*PI by XREAL_1:11; hence contradiction by A1,A2,COMPLEX2:84; end; Lm7: for c1,c2 being Element of COMPLEX st c1=euc2cpx(p1-p2) & c2=euc2cpx(p3-p2) holds angle(p1,p2,p3) = angle(c1,c2) proof let c1,c2 be Element of COMPLEX; assume A1: c1 = euc2cpx(p1-p2) & c2 = euc2cpx(p3-p2); thus angle(p1,p2,p3) = angle(p1-p2,0.REAL 2,p3-p2) by EUCLID_3:44 .= angle(c1,c2) by COMPLEX2:87,A1,EUCLID_3:21; end; Lm8: for c1,c2 being Element of COMPLEX st c2=0 holds Arg(Rotate(c2, -Arg c1)) = 0 proof let c1,c2 be Element of COMPLEX; assume c2=0; then Rotate(c2, -Arg c1) = 0 by COMPLEX2:66; hence Arg(Rotate(c2, -Arg c1)) = 0 by COMPTRIG:def 1; end; Lm9: for c1,c2 being Element of COMPLEX st c2=0 & Arg c1 = 0 holds angle(c1,c2) = 0 proof let c1,c2 be Element of COMPLEX; assume A1: c2=0 & Arg c1 = 0; hence angle(c1,c2) = Arg(Rotate(c2, -Arg c1)) by COMPLEX2:def 5 .= 0 by A1,Lm8; end; Lm10: for c1,c2 being Element of COMPLEX st c2<>0 & Arg c2 - Arg c1 >= 0 holds Arg(Rotate(c2, -Arg c1)) = Arg c2 - Arg c1 proof let c1,c2 be Element of COMPLEX; assume A1: c2<>0 & Arg c2 - Arg c1 >= 0; set z = Rotate(c2, -Arg c1); set a = -Arg c1 + Arg c2; z = [*|.c2.|*cos a,|.c2.|*sin a*] by COMPLEX2:def 4; then A2: z = |.c2.|*cos a + |.c2.|*sin a * by COMPLEX1:27; Arg c2<2*PI & 0<=Arg c1 by COMPTRIG:52; then Arg c2+0<2*PI+Arg c1 by XREAL_1:10; then A3: Arg c2-Arg c1<2*PI+Arg c1-Arg c1 by XREAL_1:11; A4: |.z.| = |.c2.| by COMPLEX2:67; then z<>0 by A1,COMPLEX1:131,130; hence thesis by A1,A3,A2,A4,COMPTRIG:def 1; end; Lm11: for c1,c2 being Element of COMPLEX st c2<>0 & Arg c2 - Arg c1 >= 0 holds angle(c1,c2) = Arg c2 - Arg c1 proof let c1,c2 be Element of COMPLEX; assume A1: c2<>0 & Arg c2 - Arg c1 >= 0; hence angle(c1,c2) = Arg(Rotate(c2, -Arg c1)) by COMPLEX2:def 5 .= Arg c2 - Arg c1 by A1,Lm10; end; Lm12: for c1,c2 being Element of COMPLEX st c2<>0 & Arg c2 - Arg c1 < 0 holds Arg(Rotate(c2, -Arg c1)) = 2*PI - Arg c1 + Arg c2 proof let c1,c2 be Element of COMPLEX; assume A1: c2<>0 & Arg c2 - Arg c1 < 0; set z = Rotate(c2, -Arg c1); set a = -Arg c1 + Arg c2; z = [*|.c2.|*cos a,|.c2.|*sin a*] by COMPLEX2:def 4; then z = |.c2.|*cos a + |.c2.|*sin a * by COMPLEX1:27; then A2: z = |.c2.|*cos(2*PI*1+a) + |.c2.|*sin a * by COMPLEX2:10 .= |.c2.|*cos(2*PI+a) + |.c2.|*sin(2*PI*1+a) * by COMPLEX2:9; 0<=Arg c2 & Arg c1<=2*PI by COMPTRIG:52; then Arg c1+0<=2*PI+Arg c2 by XREAL_1:9; then A3: Arg c1-Arg c1<=2*PI+Arg c2-Arg c1 by XREAL_1:11; A4: a+2*PI<0+2*PI by A1,XREAL_1:8; A5: |.z.| = |.c2.| by COMPLEX2:67; then z<>0 by A1,COMPLEX1:131,130; hence thesis by A3,A4,A2,A5,COMPTRIG:def 1; end; Lm13: for c1,c2 being Element of COMPLEX st c2<>0 & Arg c2 - Arg c1 < 0 holds angle(c1,c2) = 2*PI - Arg c1 + Arg c2 proof let c1,c2 be Element of COMPLEX; assume A1: c2<>0 & Arg c2 - Arg c1 < 0; hence angle(c1,c2) = Arg(Rotate(c2, -Arg c1)) by COMPLEX2:def 5 .= 2*PI - Arg c1 + Arg c2 by A1,Lm12; end; Lm14: for c1,c2,c3 being Element of COMPLEX holds angle(c1,c2) + angle(c2,c3) = angle(c1,c3) or angle(c1,c2) + angle(c2,c3) = angle(c1,c3) + 2*PI proof let c1,c2,c3 be Element of COMPLEX; per cases; suppose A1: c2=0 & c3=0; then A2: Arg c2=0 by COMPTRIG:def 1; per cases; suppose Arg c1=0; then angle(c1,c2) + angle(c2,c3) = 0 + angle(c2,c3) by A1,Lm9; hence thesis by A1,A2,Lm9; end; suppose A3: Arg c1<>0; then angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + angle(c2,c3) by A1,COMPLEX2:def 5 .= 2*PI - Arg c1 + 0 by A1,A2,Lm9; hence thesis by A1,A3,COMPLEX2:def 5; end; end; suppose A4: c2<>0 & c3=0; per cases; suppose A5: Arg c1=0 & Arg c2=0; per cases; suppose Arg c2 - Arg c1 < 0; hence thesis by A5; end; suppose Arg c2 - Arg c1 >= 0; then angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1 + angle(c2,c3) by A4,Lm11 .= 0 by A5,A4,Lm9; hence thesis by A5,A4,Lm9; end; end; suppose A6: Arg c1<>0 & Arg c2=0; per cases; suppose Arg c2 - Arg c1 < 0; then angle(c1,c2) + angle(c2,c3) = 2*PI -Arg c1 +Arg c2 + angle(c2,c3) by A4,Lm13 .= 2*PI -Arg c1 by A6,A4,Lm9; hence thesis by A6,A4,COMPLEX2:def 5; end; suppose Arg c2 - Arg c1 >= 0; then --Arg c1 <= -0 by A6,XREAL_1:26; hence thesis by A6,COMPTRIG:52; end; end; suppose A7: Arg c1=0 & Arg c2<>0; per cases; suppose Arg c2 - Arg c1 < 0; hence thesis by A7,COMPTRIG:52; end; suppose Arg c2 - Arg c1 >= 0; then A8: angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1 + angle(c2,c3) by A4,Lm11 .= Arg c2 + (2*PI - Arg c2) by A7,A4,COMPLEX2:def 5; angle(c1,c3) = 0 by A7,A4,Lm9; hence thesis by A8; end; end; suppose A9: Arg c1<>0 & Arg c2<>0; per cases; suppose Arg c2 - Arg c1 < 0; then A10: angle(c1,c2) + angle(c2,c3) = 2*PI -Arg c1 +Arg c2 + angle(c2,c3) by A4,Lm13 .= 2*PI -Arg c1 + Arg c2 + (2*PI - Arg c2) by A9,A4,COMPLEX2:def 5 .= 2*PI + 2*PI -Arg c1; angle(c1,c3) = 2*PI -Arg c1 by A9,A4,COMPLEX2:def 5; hence thesis by A10; end; suppose Arg c2 - Arg c1 >= 0; then A11: angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1 + angle(c2,c3) by A4,Lm11 .= Arg c2 - Arg c1 + (2*PI - Arg c2) by A9,A4,COMPLEX2:def 5; angle(c1,c3) = 2*PI -Arg c1 by A9,A4,COMPLEX2:def 5; hence thesis by A11; end; end; end; suppose A12: c2=0 & c3<>0; per cases; suppose Arg c3 - Arg c2<0 & Arg c3 - Arg c1<0; then Arg c3 - 0 < 0 by A12,COMPTRIG:def 1; hence thesis by COMPTRIG:52; end; suppose A13: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1<0; per cases; suppose Arg c1=0; hence thesis by A13,COMPTRIG:52; end; suppose Arg c1<>0; then angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + angle(c2,c3) by A12,COMPLEX2:def 5 .= 2*PI - Arg c1 + (Arg c3 - Arg c2) by A13,A12,Lm11 .= 2*PI - Arg c1 + (Arg c3 - 0) by A12,COMPTRIG:def 1 .= 2*PI - Arg c1 + Arg c3; hence thesis by A13,A12,Lm13; end; end; suppose Arg c3 - Arg c2<0 & Arg c3 - Arg c1>=0; then Arg c3 - 0 < 0 by A12,COMPTRIG:def 1; hence thesis by COMPTRIG:52; end; suppose A14: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1>=0; per cases; suppose A15: Arg c1=0; then angle(c1,c2) + angle(c2,c3) = 0 + angle(c2,c3) by A12,Lm9 .= 0 + (Arg c3 - Arg c2) by A14,A12,Lm11 .= 0 + (Arg c3 - 0) by A12,COMPTRIG:def 1; hence thesis by A15,A14,A12,Lm11; end; suppose Arg c1<>0; then A16: angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + angle(c2,c3) by A12,COMPLEX2:def 5 .= 2*PI - Arg c1 + (Arg c3 - Arg c2) by A14,A12,Lm11 .= 2*PI - Arg c1 + (Arg c3 - 0) by A12,COMPTRIG:def 1; angle(c1,c3) = Arg c3 - Arg c1 by A14,A12,Lm11; hence thesis by A16; end; end; end; suppose A17: c2<>0 & c3<>0; per cases; suppose A18: Arg c3 - Arg c2<0 & Arg c3 - Arg c1<0; per cases; suppose Arg c2 - Arg c1 < 0; then A19: angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + Arg c2+ angle(c2,c3) by A17,Lm13 .= 2*PI - Arg c1 + Arg c2 + (2*PI - Arg c2 + Arg c3) by A17,A18,Lm13 .= 2*PI +2*PI - Arg c1 + Arg c3; angle(c1,c3) = 2*PI - Arg c1 + Arg c3 by A17,A18,Lm13; hence thesis by A19; end; suppose Arg c2 - Arg c1 >= 0; then angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1+ angle(c2,c3) by A17,Lm11 .= Arg c2 - Arg c1 + (2*PI - Arg c2 + Arg c3) by A17,A18,Lm13 .= 2*PI - Arg c1 + Arg c3; hence thesis by A17,A18,Lm13; end; end; suppose A20: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1<0; per cases; suppose Arg c2 - Arg c1 < 0; then angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + Arg c2+ angle(c2,c3 ) by A17,Lm13 .= 2*PI - Arg c1 + Arg c2 + (Arg c3 - Arg c2) by A17,A20,Lm11 .= 2*PI - Arg c1 + Arg c3; hence thesis by A17,A20,Lm13; end; suppose Arg c2 - Arg c1 >= 0; then Arg c2 - Arg c1 +(Arg c3 - Arg c2) >= 0+0 by A20,XREAL_1:9; hence thesis by A20; end; end; suppose A21: Arg c3 - Arg c2<0 & Arg c3 - Arg c1>=0; per cases; suppose Arg c2 - Arg c1 < 0; then Arg c2 - Arg c1 +(Arg c3 - Arg c2) < 0+0 by A21,XREAL_1:10; hence thesis by A21; end; suppose Arg c2 - Arg c1 >= 0; then A22: angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1+ angle(c2,c3 ) by A17,Lm11 .= Arg c2 - Arg c1 + (2*PI -Arg c2 +Arg c3) by A17,A21,Lm13 .= 2*PI - Arg c1 + Arg c3; angle(c1,c3) = Arg c3 - Arg c1 by A17,A21,Lm11; hence thesis by A22; end; end; suppose A23: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1>=0; per cases; suppose Arg c2 - Arg c1 < 0; then A24: angle(c1,c2) + angle(c2,c3) = 2*PI -Arg c1 + Arg c2+ angle (c2,c3) by A17,Lm13 .= 2*PI +Arg c2 - Arg c1 + (Arg c3 - Arg c2) by A17,A23,Lm11 .= 2*PI - Arg c1 + Arg c3; angle(c1,c3) = Arg c3 - Arg c1 by A17,A23,Lm11; hence thesis by A24; end; suppose Arg c2 - Arg c1 >= 0; then angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1+ angle(c2,c3) by A17,Lm11 .= Arg c2 - Arg c1 + (Arg c3 -Arg c2) by A17,A23,Lm11 .= - Arg c1 + Arg c3; hence thesis by A17,A23,Lm11; end; end; end; end; theorem Th4: angle(p1,p4,p2)+angle(p2,p4,p3)=angle(p1,p4,p3) or angle(p1,p4,p2)+angle(p2,p4,p3)=angle(p1,p4,p3) + 2*PI proof set c1 = euc2cpx(p1-p4); set c2 = euc2cpx(p2-p4); set c3 = euc2cpx(p3-p4); A1: angle(p1,p4,p2)+angle(p2,p4,p3)=angle(c1,c2)+angle(p2,p4,p3) by Lm7 .= angle(c1,c2)+angle(c2,c3) by Lm7; angle(c1,c2) + angle(c2,c3) = angle(c1,c3) or angle(c1,c2) + angle(c2,c3) = angle(c1,c3) + 2*PI by Lm14; hence thesis by A1,Lm7; end; Lm15: (p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2 proof A1: euc2cpx(p1-p2) = euc2cpx(p1)-euc2cpx(p2) by EUCLID_3:19 .= euc2cpx(p1)+(-euc2cpx(p2)) .= euc2cpx(p1)+euc2cpx(-p2) by EUCLID_3:17; A2: (-p2)`1 = -p2`1 by VALUED_1:8; A3: (-p2)`2 = -p2`2 by VALUED_1:8; thus (p1-p2)`1 = Re (euc2cpx(p1)+euc2cpx(-p2)) by A1,EUCLID_3:8 .= Re euc2cpx(p1) + Re euc2cpx(-p2) by COMPLEX1:19 .= p1`1 + Re euc2cpx(-p2) by EUCLID_3:8 .= p1`1 + (-p2)`1 by EUCLID_3:8 .= p1`1 - p2`1 by A2; thus (p1-p2)`2 = Im (euc2cpx(p1)+euc2cpx(-p2)) by A1,EUCLID_3:8 .= Im euc2cpx(p1) + Im euc2cpx(-p2) by COMPLEX1:19 .= p1`2 + Im euc2cpx(-p2) by EUCLID_3:8 .= p1`2 + (-p2)`2 by EUCLID_3:8 .= p1`2 - p2`2 by A3; end; Lm16: for c1,c2 being Element of COMPLEX st c1 = euc2cpx(p1-p2) & c2 = euc2cpx(p3-p2) holds Re (c1.|.c2) = (p1`1 - p2`1)*(p3`1 - p2`1)+(p1`2 - p2`2)*(p3`2 - p2`2) & Im (c1.|.c2) = -(p1`1 - p2`1)*(p3`2 - p2`2)+(p1`2 - p2`2)*(p3`1 - p2`1) & |.c1.| = sqrt((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) & |.p1-p2.|=|.c1.| proof let c1,c2 be Element of COMPLEX; assume A1: c1 = euc2cpx(p1-p2) & c2 = euc2cpx(p3-p2); then A2: Re c1 = (p1-p2)`1 by EUCLID_3:8 .= p1`1 - p2`1 by Lm15; A3: Re c2 = (p3-p2)`1 by A1,EUCLID_3:8 .= p3`1 - p2`1 by Lm15; A4: Im c1 = (p1-p2)`2 by A1,EUCLID_3:8 .= p1`2 - p2`2 by Lm15; A5: Im c2 = (p3-p2)`2 by A1,EUCLID_3:8 .= p3`2 - p2`2 by Lm15; hence Re (c1.|.c2) = (p1`1 - p2`1)*(p3`1 - p2`1)+(p1`2 - p2`2)*(p3`2 - p2`2) by A2,A3,A4,EUCLID_3:48; thus Im (c1.|.c2) = -(p1`1 - p2`1)*(p3`2 - p2`2)+(p1`2 - p2`2)*(p3`1 - p2`1) by A2,A3,A4,A5,EUCLID_3:49; thus |.c1.| = sqrt((p1-p2)`1^2 + (Im c1)^2) by A1,EUCLID_3:8 .= sqrt((p1-p2)`1^2 + (p1-p2)`2^2) by A1,EUCLID_3:8 .= sqrt((p1`1 - p2`1)^2 + (p1-p2)`2^2) by Lm15 .= sqrt((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by Lm15; thus |.p1-p2.|=|.c1.| by A1,EUCLID_3:31; end; :: Meister-Gauss formula definition let p1,p2,p3; func the_area_of_polygon3(p1,p2,p3) -> real number equals (1/2)*((p1`1*p2`2-p2`1*p1`2)+(p2`1*p3`2-p3`1*p2`2)+(p3`1*p1`2-p1`1*p3`2)); correctness; end; definition let p1,p2,p3; func the_perimeter_of_polygon3(p1,p2,p3) -> real number equals |.p2-p1.| + |.p3-p2.| + |.p1-p3.|; correctness; end; :: Area theorem Th5: the_area_of_polygon3(p1,p2,p3) = |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) / 2 proof per cases; suppose A1: p1=p2; then |.p1-p2.| = |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID_2:61; hence the_area_of_polygon3(p1,p2,p3) = |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) / 2 by A1; end; suppose A2: p1<>p2; per cases; suppose A3: p2=p3; then |.p3-p2.| = |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID_2:61; hence the_area_of_polygon3(p1,p2,p3) = |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) / 2 by A3; end; suppose A4: p2<>p3; set a = euc2cpx(p1-p2); set b = euc2cpx(p3-p2); A5: now assume A6: a=0 or b=0; per cases by A6; suppose a=0; hence contradiction by A2,EUCLID:47,EUCLID_3:22; end; suppose b=0; hence contradiction by A4,EUCLID:47,EUCLID_3:22; end; end; A7: now assume A8: |.a.|*|.b.|=0; per cases by A8,XCMPLX_1:6; suppose |.a.|=0; hence contradiction by A5,COMPLEX1:131; end; suppose |.b.|=0; hence contradiction by A5,COMPLEX1:131; end; end; |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) / 2 = |.p1-p2.|*|.p3-p2.|*(-sin angle(p1,p2,p3)) / 2 by Th2 .= |.p1-p2.|*|.p3-p2.|*(- sin angle(a,b)) / 2 by Lm7 .= |.p1-p2.|*|.p3-p2.|*(-(-Im(a.|.b)/(|.a.|*|.b.|)))/2 by A5,COMPLEX2:83 .= |.a.|*|.p3-p2.|*(Im (a.|.b)/(|.a.|*|.b.|))/2 by Lm16 .= |.a.|*|.b.|*(Im (a.|.b)/(|.a.|*|.b.|))/2 by Lm16 .= (Im (a.|.b)/((|.a.|*|.b.|)/(|.a.|*|.b.|))/2) by XCMPLX_1:82 .= (Im (a.|.b)/1/2) by A7,XCMPLX_1:60 .= (-(p1`1 - p2`1)*(p3`2 - p2`2)+(p1`2 - p2`2)*(p3`1 - p2`1))/2 by Lm16 .= ((p1`1*p2`2 - p2`1*p1`2) + (p2`1*p3`2 - p3`1*p2`2) + (p3`1*p1`2 - p1`1*p3`2)) / 2; hence thesis; end; end; end; theorem Th6: p2<>p1 implies |.p3-p2.| * sin angle(p3,p2,p1) = |.p3-p1.| * sin angle(p2,p1,p3) proof assume p2<>p1; then A1: |.p1-p2.|<>0 by Lm1; the_area_of_polygon3(p1,p2,p3) = the_area_of_polygon3(p3,p1,p2); then |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) / 2 = the_area_of_polygon3(p3,p1,p2) by Th5; then |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) / 2 = |.p3-p1.|*|.p2-p1.|*sin angle(p2,p1,p3) / 2 by Th5; then |.p1-p2.|*|.p3-p2.|*sin angle(p3,p2,p1) = |.p3-p1.|*|.p1-p2.|*sin angle(p2,p1,p3) by Lm2; then |.p3-p2.|*sin angle(p3,p2,p1)*|.p1-p2.| = |.p3-p1.|*sin angle(p2,p1,p3)*|.p1-p2.|; hence |.p3-p2.| * sin angle(p3,p2,p1) = |.p3-p1.| * sin angle(p2,p1,p3) by A1,XCMPLX_1:5; end; :: Law of Cosines theorem Th7: a = |.p1-p2.| & b = |.p3-p2.| & c = |.p3-p1.| implies c^2 = a^2 + b^2 - 2*a*b * cos angle(p1,p2,p3) proof assume A1: a = |.p1-p2.| & b = |.p3-p2.| & c = |.p3-p1.|; per cases; suppose A2: p1=p2; then |.p1-p2.| = |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID_2:61; hence thesis by A1,A2; end; suppose A3: p1<>p2; per cases; suppose A4: p2=p3; then |.p3-p2.| = |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID_2:61; then |.p1-p2.|^2 + |.p3-p2.|^2 - 2*|.p1-p2.|*|.p3-p2.|*cos angle(p1,p2, p3) = |.-(p1 - p2).|^2 by EUCLID:13 .= |.p2 - p1.|^2 by EUCLID:48; hence thesis by A1,A4; end; suppose A5: p2<>p3; set c1 = euc2cpx(p1-p2); set c2 = euc2cpx(p3-p2); A6: now assume A7: c1=0 or c2=0; per cases by A7; suppose c1=0; hence contradiction by A3,EUCLID:47,EUCLID_3:22; end; suppose c2=0; hence contradiction by A5,EUCLID:47,EUCLID_3:22; end; end; A8: now assume A9: |.c1.|*|.c2.|=0; per cases by A9,XCMPLX_1:6; suppose |.c1.|=0; hence contradiction by A6,COMPLEX1:131; end; suppose |.c2.|=0; hence contradiction by A6,COMPLEX1:131; end; end; A10: |.p1-p2.|*|.p3-p2.|*cos angle(p1,p2,p3) = |.p1-p2.|*|.p3-p2.|*cos angle(c1,c2) by Lm7 .= |.c1.|*|.p3-p2.|*cos angle(c1,c2) by Lm16 .= |.c1.|*|.c2.|*cos angle(c1,c2) by Lm16 .= |.c1.|*|.c2.|*(Re (c1.|.c2)/(|.c1.|*|.c2.|)) by A6,COMPLEX2:83 .= (Re (c1.|.c2)/((|.c1.|*|.c2.|)/(|.c1.|*|.c2.|))) by XCMPLX_1:82 .= Re (c1.|.c2)/1 by A8,XCMPLX_1:60 .= (p1`1 - p2`1)*(p3`1 - p2`1)+(p1`2 - p2`2)*(p3`2 - p2`2) by Lm16 .= p1`1*p3`1+p1`2*p3`2 -p1`1*p2`1-p2`1*p3`1+p2`1*p2`1+ (-p1`2*p2`2-p2`2*p3`2+p2`2*p2`2) .= |(p1,p3)|-p1`1*p2`1-p2`1*p3`1+p2`1*p2`1+ (-p1`2*p2`2-p2`2*p3`2+p2`2*p2`2) by EUCLID_3:50 .= |(p1,p3)|-(p1`1*p2`1+p1`2*p2`2)-p2`1*p3`1+p2`1*p2`1+ (-p2`2*p3`2+p2`2*p2`2) .= |(p1,p3)|- |(p1,p2)|-p2`1*p3`1+p2`1*p2`1+ (-p2`2*p3`2+p2`2*p2`2) by EUCLID_3:50 .= |(p1,p3)|- |(p1,p2)|-(p2`1*p3`1+p2`2*p3`2)+p2`1*p2`1+p2`2*p2`2 .= |(p1,p3)|- |(p1,p2)|- |(p2,p3)|+p2`1*p2`1+p2`2*p2`2 by EUCLID_3:50 .= |(p1,p3)|- |(p1,p2)|- |(p2,p3)|+(p2`1*p2`1+p2`2*p2`2) .= |(p1,p3)|- |(p1,p2)|- |(p2,p3)|+|(p2,p2)| by EUCLID_3:50 .= |(p1,p3)|- |(p1,p2)|- |(p2,p3)|+|.p2.|^2 by EUCLID_2:58; a^2+b^2-c^2 = |.p1.|^2-2*|(p2, p1)|+|.p2.|^2+|.p3-p2.|^2- |.p3-p1.|^2 by A1,EUCLID_2:68 .= |.p1.|^2-2*|(p2, p1)|+|.p2.|^2 + |.p3-p2.|^2 -(|.p3.|^2-2*|(p1, p3)|+|.p1.|^2) by EUCLID_2:68 .= -2*|(p2, p1)|+|.p2.|^2 + |.p3-p2.|^2 - |.p3.|^2 + 2*|(p1, p3)| .= -2*|(p2, p1)|+|.p2.|^2 + (|.p3.|^2-2*|(p2, p3)|+|.p2.|^2) - |.p3.|^2 + 2*|(p1, p3)| by EUCLID_2:68 .= 2*(- |(p2,p1)|+|.p2.|^2 - |(p2, p3)|+ |(p1, p3)|); hence thesis by A1,A10; end; end; end; begin :: Some elementary facts about Euclidean geometry theorem Th8: p in LSeg(p1,p2) & p<>p1 & p<>p2 implies angle(p1,p,p2) = PI proof assume p in LSeg(p1,p2); then consider l be Real such that A1: 0<=l & l<=1 & p=(1-l)*p1+l*p2 by SPPOL_1:21; assume A2: p<>p1; assume A3: p<>p2; set c1=euc2cpx(p1-p); set c2=euc2cpx(p2-p); A4: p1-p = p1-((1+(-l))*p1 +l*p2) by A1 .= p1-((1)*p1+(-l)*p1 +l*p2) by EUCLID:37 .= p1+((-1)*((1)*p1+(-l)*p1)+(-1)*(l*p2)) by EUCLID:36 .= p1+((-1)*(p1+(-l)*p1)+(-1)*(l*p2)) by EUCLID:33 .= p1+((-1)*(p1+(-l)*p1)+((-1)*l)*p2) by EUCLID:34 .= p1+((-1)*p1+(-1)*((-l)*p1)+(-l)*p2) by EUCLID:36 .= p1+((-1)*p1+((-1)*(-l))*p1+(-l)*p2) by EUCLID:34 .= p1+((-1)*p1+(l*p1+(-l)*p2)) by EUCLID:30 .= (p1+(-p1))+(l*p1+(-l)*p2) by EUCLID:30 .= 0.REAL 2 +(l*p1+(-l)*p2) by EUCLID:40 .= l*p1+(l*(-1))*p2 by EUCLID:31 .= l*p1+l*((-1)*p2) by EUCLID:34 .= l*(p1-p2) by EUCLID:36; A5: p2-p = p2-((1+(-l))*p1 +l*p2) by A1 .= p2-((1)*p1+(-l)*p1 +l*p2) by EUCLID:37 .= p2+((-1)*((1)*p1+(-l)*p1)+(-1)*(l*p2)) by EUCLID:36 .= p2+((-1)*(p1+(-l)*p1)+(-1)*(l*p2)) by EUCLID:33 .= p2+((-1)*(p1+(-l)*p1)+((-1)*l)*p2) by EUCLID:34 .= p2+((-1)*p1+(-1)*((-l)*p1)+(-l)*p2) by EUCLID:36 .= p2+((-1)*p1+((-1)*(-l))*p1+(-l)*p2) by EUCLID:34 .= p2+((-1)*p1+(l*p1+(-l)*p2)) by EUCLID:30 .= (-p1+p2)+(l*(--p1)+(-l)*p2) by EUCLID:30 .= (-p1+p2)+(l*(-1)*(-p1)+(-l)*p2) by EUCLID:34 .= (-p1+p2)+(-l)*(-p1+p2) by EUCLID:36 .= (1)*(-p1+p2)+(-l)*(-p1+p2) by EUCLID:33 .= (1+(-l))*(-p1+p2) by EUCLID:37 .= (1-l)*(-p1+p2); set r = -l/(1-l); A6: l<>0 proof assume l=0; then p =1*p1+0.REAL 2 by A1,EUCLID:33 .=1*p1 by EUCLID:31 .=p1 by EUCLID:33; hence contradiction by A2; end; l<>1 proof assume l=1; then p = 0.REAL 2+1*p2 by A1,EUCLID:33 .= 1*p2 by EUCLID:31 .= p2 by EUCLID:33; hence contradiction by A3; end; then l<1 by A1,XXREAL_0:1; then -1 < -l by XREAL_1:26; then A7: -1+1 < -l+1 by XREAL_1:8; then 0/(1-l)0 proof assume -c2 = 0; then |.p2-p.| = 0 by EUCLID_3:31,COMPLEX1:130; then p2-p = 0.REAL 2 by EUCLID_2:64; hence contradiction by A3,EUCLID:47; end; angle(c1,-c2) = 0 proof per cases; suppose Arg(-c2) - Arg c1 < 0; hence thesis by A9; end; suppose Arg(-c2) - Arg c1 >= 0; hence thesis by A9,A10,Lm11; end; end; then angle(c1,-(-c2)) = PI by A10,COMPLEX2:82; hence angle(p1,p,p2) = PI by Lm7; end; theorem Th9: p in LSeg(p2,p3) & p<>p2 implies angle(p3,p2,p1)=angle(p,p2,p1) proof assume p in LSeg(p2,p3); then consider l be Real such that A1: 0<=l & l<=1 & p=(1-l)*p2+l*p3 by SPPOL_1:21; A2: p - p2 = (1+(-l))*p2 +l*p3 -p2 by A1 .= (1)*p2+(-l)*p2 +l*p3 -p2 by EUCLID:37 .= p2 +(-l)*p2 +l*p3 -p2 by EUCLID:33 .= (p2 +(-l)*p2)+ (l*p3 + -p2) by EUCLID:30 .= p2 +((-l)*p2 +(l*p3 + -p2)) by EUCLID:30 .= p2 +(-p2 + ((-l)*p2 + l*p3)) by EUCLID:30 .= (p2 + -p2) + ((-l)*p2 + l*p3) by EUCLID:30 .= 0.REAL 2 + ((-l)*p2 + l*p3) by EUCLID:40 .= (l*(-1))*p2 + l*p3 by EUCLID:31 .= l*((-1)*p2) + l*p3 by EUCLID:34 .= l*(p3-p2) by EUCLID:36; assume A3: p<>p2; set c = euc2cpx(p-p2); set c1 = euc2cpx(p1-p2); set c3 = euc2cpx(p3-p2); A4: l <> 0 proof assume l=0; then p = 1*p2+0.REAL 2 by A1,EUCLID:33 .= 1*p2 by EUCLID:31 .= p2 by EUCLID:33; hence contradiction by A3; end; cpx2euc(c3 * [*l,(0 qua Real)*]) = l*cpx2euc(c3) by EUCLID_3:23 .= l*(p3-p2) by EUCLID_3:2 .= cpx2euc(c) by A2,EUCLID_3:2; then c = c3 * [*l,(0 qua Real)*] by EUCLID_3:5; then A5: Arg c = Arg c3 by A4,A1,COMPLEX2:40; angle(c3,c1) = angle(c,c1) proof per cases; suppose A6: Arg c3 = 0 or c1 <> 0; then angle(c3,c1)=Arg(Rotate(c1, -Arg c3)) by COMPLEX2:def 5 .= angle(c,c1) by A5,A6,COMPLEX2:def 5; hence thesis; end; suppose A7: not (Arg c3 = 0 or c1 <> 0); then angle(c3,c1)=2*PI - Arg c3 by COMPLEX2:def 5 .= angle(c,c1) by A5,A7,COMPLEX2:def 5; hence thesis; end; end; hence angle(p3,p2,p1) = angle(c,c1) by Lm7 .= angle(p,p2,p1) by Lm7; end; theorem Th10: p in LSeg(p2,p3) & p<>p2 implies angle(p1,p2,p3) = angle(p1,p2,p) proof assume A1: p in LSeg(p2,p3); assume A2: p<>p2; then A3: angle(p3,p2,p1) = angle(p,p2,p1) by Th9,A1; per cases; suppose A4: angle(p1,p2,p3) = 0; then angle(p3,p2,p1) = 0 by EUCLID_3:45; then A5: angle(p,p2,p1) = 0 by Th9,A1,A2; thus angle(p1,p2,p3) = angle(p3,p2,p1) by A4,EUCLID_3:45 .= angle(p,p2,p1) by Th9,A1,A2 .= angle(p1,p2,p) by A5,EUCLID_3:45; end; suppose A6: angle(p1,p2,p3) <> 0; then A7: angle(p,p2,p1) <> 0 by A3,EUCLID_3:45; thus angle(p1,p2,p3) = 2*PI - angle(p3,p2,p1) by A6,EUCLID_3:47 .= 2*PI - angle(p,p2,p1) by Th9,A1,A2 .= angle(p1,p2,p) by A7,EUCLID_3:46; end; end; Lm17: p1 in inside_of_circle(a,b,r) & p2 in outside_of_circle(a,b,r) implies ex p st p in LSeg(p1,p2) /\ circle(a,b,r) proof assume p1 in inside_of_circle(a,b,r); then p1 in {p:|.p - |[a,b]|.| < r} by JGRAPH_6:def 6; then consider p1' be Point of TOP-REAL 2 such that A1: p1=p1' & |.p1' - |[a,b]|.| < r; assume p2 in outside_of_circle(a,b,r); then p2 in {p:|.p - |[a,b]|.| > r} by JGRAPH_6:def 8; then consider p2' be Point of TOP-REAL 2 such that A2: p2=p2' & |.p2' - |[a,b]|.| > r; set pc1 = p1 - |[a,b]|; set pc2 = p2 - |[a,b]|; consider f be Function of I[01], (TOP-REAL 2) | LSeg(pc1,pc2) such that A3: (for x being Real st x in [.0,1.] holds f.x = (1-x)*pc1 + x*pc2) and A4: f is_homeomorphism & f.0 = pc1 & f.1 = pc2 by A1,A2,JORDAN5A:4; reconsider g=f as Function of I[01], TOP-REAL 2 by JORDAN6:4; reconsider r'=r as Real by XREAL_0:def 1; f is continuous by A4,TOPS_2:def 5; then A5: g is continuous by JORDAN6:4; 0 in the carrier of I[01] by XXREAL_1:1,BORSUK_1:83; then 0 in dom g by FUNCT_2:def 1; then A6: pi(g,0) = pc1 by A4,PARTFUN1:def 8; 1 in the carrier of I[01] by XXREAL_1:1,BORSUK_1:83; then 1 in dom g by FUNCT_2:def 1; then pi(g,1) = pc2 by A4,PARTFUN1:def 8; then consider s be Point of I[01] such that A7: |.pi(g,s).| = r' by A2,A5,A6,A1,JORDAN2C:94; A8: s in the carrier of I[01]; s in [.0,1.] by BORSUK_1:83; then s in {s' where s' is Element of ExtREAL:0 <= s' & s' <= 1} by XXREAL_1: def 1; then consider s' be Element of ExtREAL such that A9: s=s' & 0 <= s' & s' <= 1; reconsider s as Real by A9,XXREAL_0:45; set p' = f.s; A10: rng g c= the carrier of TOP-REAL 2 by RELSET_1:12; s in dom g by A8,FUNCT_2:def 1; then g.s in rng g by FUNCT_1:12; then reconsider p' as Point of TOP-REAL 2 by A10; A11: f.s = (1-s)*pc1 + s*pc2 by A3,BORSUK_1:83 .= (1-s)*p1 - (1-s)*|[a,b]| + s*(p2 - |[a,b]|) by EUCLID:53 .= (1-s)*p1 - (1-s)*|[a,b]| + (s*p2 - s*|[a,b]|) by EUCLID:53 .= (1-s)*p1 + (-(1-s))*|[a,b]| + (s*p2 - s*|[a,b]|) by EUCLID:44 .= (1-s)*p1 + (-1+s)*|[a,b]| + (s*p2 - s*|[a,b]|) .= (1-s)*p1 + ((-1)*|[a,b]| +s*|[a,b]|) + (s*p2 - s*|[a,b]|) by EUCLID:37 .= ((1-s)*p1 + (-1)*|[a,b]|) +s*|[a,b]| + (s*p2 + -s*|[a,b]|) by EUCLID:30 .= ((1-s)*p1 + (-1)*|[a,b]|) + (s*|[a,b]|+(s*p2 + -s*|[a,b]|)) by EUCLID:30 .= ((1-s)*p1 + (-1)*|[a,b]|) + (s*|[a,b]| +(-s*|[a,b]|) +s*p2) by EUCLID:30 .= ((1-s)*p1 + (-1)*|[a,b]|) + (s*|[a,b]|+(-s)*|[a,b]|+s*p2) by EUCLID:44 .= ((1-s)*p1 + (-1)*|[a,b]|) + ((s+(-s))*|[a,b]|+s*p2) by EUCLID:37 .= ((1-s)*p1 + (-1)*|[a,b]|) + ((0.REAL 2)+s*p2) by EUCLID:33 .= ((1-s)*p1 + (-1)*|[a,b]|) + s*p2 by EUCLID:31 .= (1-s)*p1 + s*p2 + (-1)*|[a,b]| by EUCLID:30; set p = p' + |[a,b]|; A12: p = ((1-s)*p1 + s*p2) + (- |[a,b]| +|[a,b]|) by A11,EUCLID:30 .= ((1-s)*p1 + s*p2) + 0.REAL 2 by EUCLID:40 .= (1-s)*p1 + s*p2 by EUCLID:31; A13: (1-s)*p1 + s*p2 in LSeg(p1,p2) by A9,SPPOL_1:22; r = |. p' + 0.REAL 2 .| by EUCLID:31,A7 .= |. p' +(|[a,b]| - |[a,b]|) .| by EUCLID:46 .= |. p' + |[a,b]| + - |[a,b]| .| by EUCLID:30 .= |. p - |[a,b]| .|; then p in {p'' where p'' is Point of (TOP-REAL 2):|. p'' - |[a,b]|.| = r}; then A14: p in circle(a,b,r) by JGRAPH_6:def 5; take p; thus p in LSeg(p1,p2) /\ circle(a,b,r) by A13,A12,A14,XBOOLE_0:def 3; end; theorem Th11: angle(p1,p,p2) = PI implies p in LSeg(p1,p2) proof assume A1: angle(p1,p,p2) = PI; set a = p1`1; set b = p1`2; A2: p1 = |[a,b]| by EUCLID:57; set r = |.p-p1.|; per cases; suppose p=p1 or p=p2; hence thesis by TOPREAL1:6; end; suppose A3: p<>p1 & p<>p2; then A4: r<>0 by Lm1; |.p1 - |[a,b]|.|=0 by A2,Lm1; then |.p1 - |[a,b]|.|r proof assume |.p2-p1.|<=r; then |.p2-p1.|^2<=r^2 by SQUARE_1:77; then (r+|.p2-p.|)^2 <= r^2 by A6,Lm2; then r^2+2*r*|.p2-p.|+|.p2-p.|^2-r^2<=r^2-r^2 by XREAL_1:11; then A7: (2*r+|.p2-p.|)*|.p2-p.|<=0; |.p2-p.|<>0 by A3,Lm1; then A8: 0<|.p2-p.|; then A9: 2*r+|.p2-p.|<=0/|.p2-p.| by A7,XREAL_1:79; 2*r+|.p2-p.| > 0+0 by A8,XREAL_1:10; hence contradiction by A9; end; then p2 in {p4 : |.p4- |[a,b]| .|>r} by A2; then p2 in outside_of_circle(a,b,r) by JGRAPH_6:def 8; then consider p3 such that A10: p3 in LSeg(p1,p2) /\ circle(a,b,r) by A5,Lm17; A11: p3 in LSeg(p1,p2) & p3 in circle(a,b,r) by A10,XBOOLE_0:def 3; then p3 in {p4: |.p4- |[a,b]| .|=r} by JGRAPH_6:def 5; then consider p4 such that A12: p3=p4 & |.p4 - |[a,b]|.| = r; A13: |.p3-p1.|=r by A12,EUCLID:57; r<>0 by A3,Lm1; then A14: p3<>p1 by A12,A2,Lm1; A15: euc2cpx(p)<> euc2cpx(p1) & euc2cpx(p)<> euc2cpx(p2) & euc2cpx(p1)<> euc2cpx(p2) by A3,EUCLID_3:6,A1,COMPLEX2:93; A16: angle(p,p1,p2) = 0 proof assume angle(p,p1,p2) <> 0; then A17: angle(p,p1,p2) > 0 & angle(p,p1,p2)<2*PI by COMPLEX2:84; per cases by A15,COMPLEX2:102; suppose angle(p,p1,p2)+angle(p1,p2,p)+angle(p2,p,p1) = PI; then A18: angle(p,p1,p2)+angle(p1,p2,p)+PI = PI by COMPLEX2:96,A1; angle(p1,p2,p)>=0 by COMPLEX2:84; then angle(p,p1,p2)+angle(p1,p2,p) > 0+0 by A17,XREAL_1:10; hence contradiction by A18; end; suppose angle(p,p1,p2)+angle(p1,p2,p)+angle(p2,p,p1) = 5*PI; then A19: angle(p,p1,p2)+angle(p1,p2,p)+PI = 5*PI by COMPLEX2:96,A1; angle(p1,p2,p)<2*PI by COMPLEX2:84; then angle(p,p1,p2)+angle(p1,p2,p) < 2*PI+2*PI by A17,XREAL_1:10; hence contradiction by A19; end; end; |.p3-p.|^2 = |.p-p1.|^2 + |.p3-p1.|^2 - 2*|.p-p1.|*|.p3-p1.|* cos angle(p,p1,p3) by Th7 .= r^2+r^2 -2*r*r*cos 0 by A13,A16,A11,A14,Th10 .= 0 by SIN_COS:34; then |.p3-p.|=0 by XCMPLX_1:6; hence thesis by A11,Lm1; end; end; theorem Th12: p in LSeg(p1,p3) & p in LSeg(p1,p4) & p3<>p4 & p<>p1 implies p3 in LSeg(p1,p4) or p4 in LSeg(p1,p3) proof assume p in LSeg(p1,p3); then p in {(1-l1)*p1+l1*p3 where l1 is Real: 0<=l1 & l1<=1} by TOPREAL1:def 3; then consider l1 be Real such that A1: p=(1-l1)*p1+l1*p3 & 0<=l1 & l1<=1; assume p in LSeg(p1,p4); then p in {(1-l2)*p1+l2*p4 where l2 is Real: 0<=l2 & l2<=1} by TOPREAL1:def 3; then consider l2 be Real such that A2: p=(1-l2)*p1+l2*p4 & 0<=l2 & l2<=1; assume A3: p3<>p4 & p<>p1; (1+(-l1))*p1+l1*p3 = (1+(-l2))*p1+l2*p4 by A1,A2; then 1*p1+(-l1)*p1+l1*p3 = (1+(-l2))*p1+l2*p4 by EUCLID:37; then 1*p1+(-l1)*p1+l1*p3 = 1*p1+(-l2)*p1+l2*p4 by EUCLID:37; then p1+(-l1)*p1+l1*p3 = 1*p1+(-l2)*p1+l2*p4 by EUCLID:33; then p1+(-l1)*p1+l1*p3 = p1+(-l2)*p1+l2*p4 by EUCLID:33; then -p1+(p1+((-l1)*p1+l1*p3)) = -p1+(p1+(-l2)*p1+l2*p4) by EUCLID:30; then (-p1+p1)+((-l1)*p1+l1*p3) = -p1+(p1+(-l2)*p1+l2*p4) by EUCLID:30; then 0.REAL 2+((-l1)*p1+l1*p3) = -p1+(p1+(-l2)*p1+l2*p4) by EUCLID:40; then (-l1)*p1+l1*p3 = -p1+(p1+(-l2)*p1+l2*p4) by EUCLID:31; then (-l1)*p1+l1*p3 = -p1+(p1+((-l2)*p1+l2*p4)) by EUCLID:30; then (-l1)*p1+l1*p3 = (-p1+p1)+((-l2)*p1+l2*p4) by EUCLID:30; then (-l1)*p1+l1*p3 = 0.REAL 2+((-l2)*p1+l2*p4) by EUCLID:40; then A4: (-l1)*p1+l1*p3 = (-l2)*p1+l2*p4 by EUCLID:31; per cases; suppose A5: l1<=l2; per cases by A5,XXREAL_0:1; suppose A6: l1l2; then l2/l1p1 & p<>p3 implies angle(p1,p,p2)+angle(p2,p,p3)=PI or angle(p1,p,p2)+angle(p2,p,p3)=3*PI proof assume A1: p in LSeg(p1,p3) & p<>p1 & p<>p3; A2: angle(p1,p,p2)+angle(p2,p,p3) = angle(p1,p,p3) or angle(p1,p,p2)+angle(p2,p,p3) = angle(p1,p,p3) + 2*PI by Th4; angle(p1,p,p3) = PI by A1,Th8; hence thesis by A2; end; theorem Th14: p in LSeg(p1,p2) & p<>p1 & p<>p2 & (angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI) implies angle(p1,p,p3)=angle(p3,p,p2) proof assume A1: p in LSeg(p1,p2) & p<>p1 & p<>p2; assume A2: angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI; A3: angle(p3,p,p1)=angle(p2,p,p3) proof per cases by A1,A2,Th13; suppose (angle(p2,p,p3)+angle(p3,p,p1)=PI & angle(p3,p,p1)=PI/2) or (angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)=3/2*PI); hence angle(p3,p,p1)=angle(p2,p,p3); end; suppose A4: angle(p2,p,p3)+angle(p3,p,p1)=PI & angle(p3,p,p1)=3/2*PI; (-PI)/2 < 0/2; hence thesis by A4,COMPLEX2:84; end; suppose A5: angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)=PI/2; 0+2*PI < PI/2+2*PI by XREAL_1:8; hence thesis by A5,COMPLEX2:84; end; end; per cases; suppose A6: angle(p3,p,p1)=0; then angle(p1,p,p3) = 0 by EUCLID_3:45; hence angle(p1,p,p3)=angle(p3,p,p2) by A6,A3,EUCLID_3:45; end; suppose A7: angle(p3,p,p1)<>0; then angle(p1,p,p3)=2*PI-angle(p3,p,p1) by EUCLID_3:46; hence angle(p1,p,p3)=angle(p3,p,p2) by A3,A7,EUCLID_3:46; end; end; :: Vertical angles theorem Th15: p in LSeg(p1,p3) & p in LSeg(p2,p4) & p<>p1 & p<>p2 & p<>p3 & p<>p4 implies angle(p1,p,p2)=angle(p3,p,p4) proof assume A1: p in LSeg(p1,p3); assume A2: p in LSeg(p2,p4); assume A3: p<>p1; assume A4: p<>p2; assume A5: p<>p3; assume A6: p<>p4; per cases by A1,A3,A5,A2,A4,A6,Th13; suppose angle(p1,p,p2)+angle(p2,p,p3)=PI & angle(p2,p,p3)+angle(p3,p,p4)=PI; hence thesis; end; suppose A7: angle(p1,p,p2)+angle(p2,p,p3)=3*PI & angle(p2,p,p3)+angle(p3,p,p4)=PI; angle(p3,p,p4)>=0 by COMPLEX2:84; then angle(p3,p,p4)+2*PI>=0+2*PI by XREAL_1:8; hence thesis by A7,COMPLEX2:84; end; suppose A8: angle(p1,p,p2)+angle(p2,p,p3)=PI & angle(p2,p,p3)+angle(p3,p,p4)=3*PI; angle(p3,p,p4)<2*PI by COMPLEX2:84; then angle(p3,p,p4)-2*PI<2*PI-2*PI by XREAL_1:11; hence thesis by A8,COMPLEX2:84; end; suppose angle(p1,p,p2)+angle(p2,p,p3)=3*PI & angle(p2,p,p3)+angle(p3,p,p4)=3*PI; hence thesis; end; end; :: The Isosceles Triangle Theorem A theorem Th16: |.p3-p1.|=|.p2-p3.| & p1<>p2 implies angle(p3,p1,p2)=angle(p1,p2,p3) proof assume A1: |.p3-p1.|=|.p2-p3.|; assume A2: p1<>p2; per cases; suppose p1,p2,p3 are_mutually_different; then p1<>p2 & p1<>p3 & p2<>p3 by ZFMISC_1:def 5; then A3: |.p3-p1.|<>0 & |.p1-p2.|<>0 & |.p2-p3.|<>0 by Lm1; |.p3-p1.| * sin angle(p3,p1,p2) = |.p3-p2.| * sin angle(p1,p2,p3) by A2,Th6 .= |.p3-p1.| * sin angle(p1,p2,p3) by A1,Lm2; then A4: sin angle(p3,p1,p2) = sin angle(p1,p2,p3) by A3,XCMPLX_1:5; |.p3-p1.|^2 = |.p1-p2.|^2 + |.p3-p2.|^2 - 2*|.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) by Th7; then |.p1-p2.|^2 + |.p3-p2.|^2 - 2*|.p1-p2.|*|.p3-p2.| * cos angle(p1,p2, p3) = |.p3-p1.|^2 + |.p2-p1.|^2 - 2*|.p3-p1.|*|.p2-p1.| * cos angle(p3,p1,p2) by A1,Th7; then |.p3-p2.|^2 - 2*|.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) + |.p1-p2.| ^2 = |.p3-p1.|^2 - 2*|.p3-p1.|*|.p2-p1.| * cos angle(p3,p1,p2) + |.p2-p1.|^2; then |.p3-p2.|^2 - 2*|.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) + |.p1-p2.| ^2 = |.p3-p1.|^2 - 2*|.p3-p1.|*|.p2-p1.| * cos angle(p3,p1,p2) + |.p1-p2.|^2 by Lm2; then - 2*|.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) + |.p3-p2.|^2 = - 2*|.p2-p3.|*|.p2-p1.| * cos angle(p3,p1,p2) + |.p2-p3.|^2 by A1; then - 2*|.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) + |.p3-p2.|^2 = - 2*|.p2-p3.|*|.p2-p1.| * cos angle(p3,p1,p2) + |.p3-p2.|^2 by Lm2; then |.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) = |.p2-p3.|*|.p2-p1.| * cos angle(p3,p1,p2); then |.p1-p2.|*|.p3-p2.| * cos angle(p1,p2,p3) = |.p2-p3.|*|.p1-p2.| * cos angle(p3,p1,p2) by Lm2; then |.p3-p2.| * cos angle(p1,p2,p3)* |.p1-p2.| = |.p2-p3.| * cos angle(p3,p1,p2)* |.p1-p2.|; then |.p3-p2.| * cos angle(p1,p2,p3) = |.p2-p3.| * cos angle(p3,p1,p2) by A3,XCMPLX_1:5; then |.p2-p3.| * cos angle(p1,p2,p3) = |.p2-p3.| * cos angle(p3,p1,p2) by Lm2; then cos angle(p1,p2,p3) = cos angle(p3,p1,p2) by A3,XCMPLX_1:5; hence thesis by A4,Th1; end; suppose A5: not p1,p2,p3 are_mutually_different; per cases by A5,ZFMISC_1:def 5; suppose p1=p2; hence thesis by A2; end; suppose A6: p1=p3; then |.p2-p3.| = 0 by A1,Lm1; then p2=p3 by Lm1; hence thesis by A6; end; suppose A7: p2=p3; then |.p3-p1.| = 0 by A1,Lm1; then p3=p1 by Lm1; hence thesis by A7; end; end; end; theorem Th17: for p1,p2,p3,p st p in LSeg(p1,p2) & p<>p2 holds |(p3-p,p2-p1)| = 0 iff |(p3-p,p2-p)| = 0 proof let p1,p2,p3,p; assume p in LSeg(p1,p2); then consider l be Real such that A1: 0<=l & l<=1 & p=(1-l)*p2+l*p1 by SPPOL_1:21; assume A2: p<>p2; A3: p2-p = p2-((1-l)*p2)-l*p1 by A1,EUCLID:50 .= p2-(1*p2-l*p2)-l*p1 by EUCLID:54 .= p2-(p2-l*p2)-l*p1 by EUCLID:33 .= p2-p2+l*p2-l*p1 by EUCLID:51 .= 0.REAL 2+l*p2-l*p1 by EUCLID:46 .= l*p2-l*p1 by EUCLID:31 .= l*(p2-p1) by EUCLID:53; hereby assume A4: |(p3-p,p2-p1)| = 0; thus |(p3-p,p2-p)| = l*|(p3-p,p2-p1)| by A3,EUCLID_2:42 .= 0 by A4; end; assume |(p3-p,p2-p)| = 0; then A5: l*|(p3-p,p2-p1)| = 0 by A3,EUCLID_2:42; per cases by A5,XCMPLX_1:6; suppose l=0; then p = 1*p2+0.REAL 2 by A1,EUCLID:33 .= 1*p2 by EUCLID:31 .= p2 by EUCLID:33; hence thesis by A2; end; suppose |(p3-p,p2-p1)| = 0; hence thesis; end; end; theorem Th18: |.p1-p3.|=|.p2-p3.| & p in LSeg(p1,p2) & p<>p3 & p<>p1 & (angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI) implies angle(p1,p3,p)=angle(p,p3,p2) proof assume A1: |.p1-p3.|=|.p2-p3.|; then A2: |.p3-p1.|=|.p2-p3.| by Lm2; assume A3: p in LSeg(p1,p2); assume A4: p<>p3 & p<>p1; assume A5: angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI; per cases; suppose A6: p1=p2; then LSeg(p1,p2) = {p1} by TOPREAL1:7; then p=p1 & p=p2 by A3,A6,TARSKI:def 1; hence angle(p1,p3,p)=angle(p,p3,p2); end; suppose A7: p1<>p2; per cases; suppose A8: p<>p2; A9: angle(p3,p1,p) = angle(p3,p1,p2) by A4,A3,Th10 .= angle(p1,p2,p3) by A7,A2,Th16 .= angle(p,p2,p3) by A3,A8,Th9; A10: angle(p1,p,p3) = angle(p3,p,p2) by A4,A5,A8,A3,Th14; A11: p1<>p3 proof assume A12: p1=p3; then |.p2-p3.|=0 by Lm1,A1; hence contradiction by Lm1,A12,A7; end; p2<>p3 proof assume A13: p2=p3; then |.p3-p1.|=0 by Lm1,A2; hence contradiction by Lm1,A13,A7; end; then A14: euc2cpx(p)<> euc2cpx(p1) & euc2cpx(p)<> euc2cpx(p3) & euc2cpx(p1)<> euc2cpx(p3) & euc2cpx(p2)<> euc2cpx(p3) & euc2cpx(p)<> euc2cpx(p2) by EUCLID_3:6,A8,A4,A11; A15: angle(p,p3,p1)=angle(p2,p3,p) proof per cases by A9,A10,A14,COMPLEX2:102; suppose (angle(p,p2,p3)+angle(p,p3,p1)+angle(p3,p,p2) = PI & angle(p,p2,p3)+angle(p2,p3,p)+angle(p3,p,p2) = PI) or (angle(p,p2,p3)+angle(p,p3,p1)+angle(p3,p,p2) = 5*PI & angle(p,p2,p3)+angle(p2,p3,p)+angle(p3,p,p2) = 5*PI); hence thesis; end; suppose angle(p,p2,p3)+angle(p,p3,p1)+angle(p3,p,p2) = PI & angle(p,p2,p3)+angle(p2,p3,p)+angle(p3,p,p2) = 5*PI; then A16: angle(p2,p3,p)-angle(p,p3,p1) = 4*PI; angle(p2,p3,p)<2*PI & angle(p,p3,p1)>=0 by COMPLEX2:84; then angle(p2,p3,p)-angle(p,p3,p1) < 2*PI-0 by XREAL_1:16; hence thesis by A16,XREAL_1:66; end; suppose angle(p,p2,p3)+angle(p,p3,p1)+angle(p3,p,p2) = 5*PI & angle(p,p2,p3)+angle(p2,p3,p)+angle(p3,p,p2) = PI; then A17: angle(p,p3,p1)-angle(p2,p3,p) = 4*PI; angle(p,p3,p1)<2*PI & angle(p2,p3,p)>=0 by COMPLEX2:84; then angle(p,p3,p1)-angle(p2,p3,p) < 2*PI-0 by XREAL_1:16; hence thesis by A17,XREAL_1:66; end; end; per cases; suppose A18: angle(p,p3,p1)=0; then angle(p1,p3,p)=0 by EUCLID_3:45; hence thesis by A15,EUCLID_3:45,A18; end; suppose A19: angle(p,p3,p1)<>0; then angle(p1,p3,p)=2*PI-angle(p,p3,p1) by EUCLID_3:46; hence thesis by A15,EUCLID_3:46,A19; end; end; suppose A20: p=p2; then |.p3-p1.|=|.p-p3.| by A1,Lm2 .= |.p3-p.| by Lm2; then |.p3-p1.|^2+|.p1-p.|^2=|.p3-p1.|^2 by A5,A4,EUCLID_3:55; then |.p1-p.|=0 by XCMPLX_1:6; hence angle(p1,p3,p)=angle(p,p3,p2) by Lm1,A20; end; end; end; :: The Isosceles Triangle Theorem B theorem for p1,p2,p3,p st |.p1-p3.|=|.p2-p3.| & p in LSeg(p1,p2) & p<>p3 holds (angle(p1,p3,p)=angle(p,p3,p2) implies |.p1-p.| = |.p-p2.|) & (|.p1-p.| = |.p-p2.| implies |(p3-p,p2-p1)| = 0) & (|(p3-p,p2-p1)| = 0 implies angle(p1,p3,p)=angle(p,p3,p2)) proof let p1,p2,p3,p; assume A1: |.p1-p3.|=|.p2-p3.|; assume A2: p in LSeg(p1,p2); assume A3: p<>p3; per cases; suppose A4: p1=p2; then LSeg(p1,p2) = {p1} by TOPREAL1:7; then A5: p=p1 & p=p2 by A2,A4,TARSKI:def 1; p2-p1=0.REAL 2 by EUCLID:46,A4; hence thesis by A5,EUCLID_2:54; end; suppose p1<>p2; thus (angle(p1,p3,p)=angle(p,p3,p2) implies |.p1-p.| = |.p-p2.|) proof assume A6: angle(p1,p3,p)=angle(p,p3,p2); A7: |.p-p1.|^2 = |.p1-p3.|^2 + |.p-p3.|^2 - 2*|.p1-p3.|*|.p-p3.| * cos angle(p1,p3,p) by Th7 .= |.p-p3.|^2 + |.p2-p3.|^2 - 2*|.p-p3.|*|.p2-p3.| * cos angle(p,p3,p2) by A6,A1 .= |.p2-p.|^2 by Th7; thus |.p1-p.| = |.p-p1.| by Lm2 .= sqrt |.p2-p.|^2 by A7,SQUARE_1:89 .= |.p2-p.| by SQUARE_1:89 .= |.p-p2.| by Lm2; end; thus |.p1-p.| = |.p-p2.| implies |(p3-p,p2-p1)| = 0 proof assume A8: |.p1-p.| = |.p-p2.|; per cases; suppose A9: p=p2; then |.p1-p.| = 0 by A8,Lm1; hence |(p3-p,p2-p1)| = |(p3-p,p-p)| by A9,Lm1 .= |(p3-p,0.REAL 2)| by EUCLID:46 .= 0 by EUCLID_2:54; end; suppose A10: p<>p2; then A11: |.p2-p.|<>0 by Lm1; |.p1-p.|<>0 by A10,A8,Lm1; then A12: p<>p1 by Lm1; A13: |.p3-p.|<>0 by A3,Lm1; A14: |.p3-p1.|^2 = |.p1-p.|^2 + |.p3-p.|^2 - 2*|.p1-p.|*|.p3-p.| * cos angle(p1,p,p3) by Th7; A15: |.p2-p3.|^2 = |.p3-p.|^2 + |.p2-p.|^2 - 2*|.p3-p.|*|.p2-p.| * cos angle(p3,p,p2) by Th7; A16: |.p3-p1.| = |.p2-p3.| by A1,Lm2; A17: |.p1-p.| = |.p2-p.| by A8,Lm2; then 2*|.p1-p.|*cos angle(p1,p,p3)*|.p3-p.| = 2*|.p2-p.|*cos angle(p3,p,p2)*|.p3-p.| by A14,A16,A15; then 2*cos angle(p1,p,p3)*|.p2-p.|=2*cos angle(p3,p,p2)*|.p2-p.| by A17,A13,XCMPLX_1:5; then A18: 2*cos angle(p1,p,p3)=2*cos angle(p3,p,p2) by A11,XCMPLX_1: 5; A19: cos angle(p1,p,p3) = - cos angle(p3,p,p2) proof per cases by Th13,A10,A12,A2; suppose angle(p1,p,p3) + angle(p3,p,p2) = PI; hence cos angle(p1,p,p3) = cos(PI+(-angle(p3,p,p2))) .= - cos(-angle(p3,p,p2)) by SIN_COS:84 .= - cos angle(p3,p,p2) by SIN_COS:34; end; suppose angle(p1,p,p3) + angle(p3,p,p2) = 3*PI; hence cos angle(p1,p,p3) = cos((PI-angle(p3,p,p2)+2*PI)) .= cos(PI+(-angle(p3,p,p2))) by SIN_COS:84 .= - cos(-angle(p3,p,p2)) by SIN_COS:84 .= - cos angle(p3,p,p2) by SIN_COS:34; end; end; 0<=angle(p3,p,p2) & angle(p3,p,p2)<2*PI by COMPLEX2:84; then angle(p3,p,p2)=PI/2 or angle(p3,p,p2)=3/2*PI by A18,A19,COMPTRIG: 34; then |(p3-p,p2-p)| = 0 by A10,A3,EUCLID_3:54; hence |(p3-p,p2-p1)| = 0 by A10,A2,Th17; end; end; thus (|(p3-p,p2-p1)| = 0 implies angle(p1,p3,p)=angle(p,p3,p2)) proof assume A20: |(p3-p,p2-p1)| = 0; then A21: 0 = -|(p3-p,p2-p1)| .= |(p3-p,-(p2-p1))| by EUCLID_2:44 .= |(p3-p,p1-p2)| by EUCLID:48; per cases; suppose p2=p & p1=p; hence angle(p1,p3,p)=angle(p,p3,p2); end; suppose A22: p1<>p; then |(p3-p,p1-p)| = 0 by A21,A2,Th17; then angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI by A22,A3,EUCLID_3: 54; hence angle(p1,p3,p)=angle(p,p3,p2) by A22,A1,A3,A2,Th18; end; suppose A23: p2<>p; then |(p3-p,p2-p)| = 0 by A20,A2,Th17; then angle(p3,p,p2)=PI/2 or angle(p3,p,p2)=3/2*PI by A23,A3,EUCLID_3: 54; then A24: angle(p2,p3,p)=angle(p,p3,p1) by A23,A1,A3,A2,Th18; per cases; suppose A25: angle(p2,p3,p)=0; then angle(p,p3,p2) = 0 by EUCLID_3:45; hence angle(p1,p3,p)=angle(p,p3,p2) by A25,A24,EUCLID_3:45; end; suppose A26: angle(p2,p3,p)<>0; then angle(p,p3,p2)=2*PI-angle(p2,p3,p) by EUCLID_3:46; hence angle(p1,p3,p)=angle(p,p3,p2) by A24,A26,EUCLID_3:46; end; end; end; end; end; definition let p1,p2,p3; pred p1,p2,p3 is_collinear means :Def3: p1 in LSeg(p2,p3) or p2 in LSeg(p3,p1) or p3 in LSeg(p1,p2); end; notation let p1,p2,p3; antonym p1,p2,p3 is_a_triangle for p1,p2,p3 is_collinear; end; theorem Th20: p1,p2,p3 is_a_triangle iff p1,p2,p3 are_mutually_different & angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI proof hereby assume p1,p2,p3 is_a_triangle; then A1: not p1 in LSeg(p2,p3) & not p2 in LSeg(p3,p1) & not p3 in LSeg(p1,p2) by Def3; then p1<>p2 & p1<>p3 & p2<>p3 by TOPREAL1:6; hence p1,p2,p3 are_mutually_different by ZFMISC_1:def 5; thus angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI by Th11,A1; end; assume p1,p2,p3 are_mutually_different; then A2: p1<>p2 & p1<>p3 & p2<>p3 by ZFMISC_1:def 5; assume angle(p1,p2,p3)<>PI; then A3: not p2 in LSeg(p1,p3) by A2,Th8; assume angle(p2,p3,p1)<>PI; then A4: not p3 in LSeg(p2,p1) by A2,Th8; assume angle(p3,p1,p2)<>PI; then not p1 in LSeg(p3,p2) by A2,Th8; hence p1,p2,p3 is_a_triangle by A3,A4,Def3; end; Lm18: p3<>p2 & p3<>p1 & p2<>p1 & p5<>p6 & p5<>p4 & p6<>p4 & angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI & angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI & angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p6,p4,p5) implies |.p3-p2.|*|.p4-p6.| = |.p1-p3.|*|.p6-p5.| proof assume A1: p3<>p2 & p3<>p1 & p2<>p1; then A2: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by EUCLID_3:6; assume A3: p5<>p6 & p5<>p4 & p6<>p4; then A4: euc2cpx(p5)<> euc2cpx(p6) & euc2cpx(p5)<> euc2cpx(p4) & euc2cpx(p6)<> euc2cpx(p4) by EUCLID_3:6; assume A5: angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI; assume A6: angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI; assume A7: angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p6,p4,p5); then A8: sin angle(p2,p1,p3)*sin angle(p6,p5,p4) = sin angle(p2,p1,p3)*(-sin angle(p1,p2,p3)) by Th2 .= (-sin angle(p6,p4,p5))*(-sin angle(p1,p2,p3)) by A7,Th2 .= sin angle(p5,p4,p6)*(-sin angle(p1,p2,p3)) by Th2 .= sin angle(p3,p2,p1)*sin angle(p5,p4,p6) by Th2; per cases; suppose A9: sin angle(p3,p2,p1)*sin angle(p5,p4,p6)<>0; A10: |.p3-p2.|*|.p4-p6.|*sin angle(p3,p2,p1)*sin angle(p5,p4,p6) = (|.p3-p2.|*sin angle(p3,p2,p1))*(|.p4-p6.|*sin angle(p5,p4,p6)) .= (|.p3-p1.|*sin angle(p2,p1,p3))*(|.p4-p6.|*sin angle(p5,p4,p6)) by A1,Th6 .= (|.p3-p1.|*sin angle(p2,p1,p3))*(|.p6-p4.|*sin angle(p5,p4,p6)) by Lm2 .= (|.p3-p1.|*sin angle(p2,p1,p3))*(|.p6-p5.|*sin angle(p6,p5,p4)) by Th6,A3 .= |.p3-p1.|*|.p6-p5.|*sin angle(p2,p1,p3)*sin angle(p6,p5,p4); thus |.p3-p2.|*|.p4-p6.| = (|.p3-p2.|*|.p4-p6.|)*(sin angle(p3,p2,p1)*sin angle(p5,p4,p6))/ (sin angle(p3,p2,p1)*sin angle(p5,p4,p6)) by A9,XCMPLX_1:90 .= ((|.p3-p1.|*|.p6-p5.|)*(sin angle(p2,p1,p3)*sin angle(p6,p5,p4)))/ (sin angle(p3,p2,p1)*sin angle(p5,p4,p6)) by A10 .= |.p3-p1.|*|.p6-p5.| by A8,A9,XCMPLX_1:90 .= |.p1-p3.|*|.p6-p5.| by Lm2; end; suppose A11: sin angle(p3,p2,p1)*sin angle(p5,p4,p6)=0; per cases by A11,XCMPLX_1:6; suppose sin angle(p3,p2,p1) = 0; then A12: - sin angle(p1,p2,p3) = 0 by Th2; 2*PI*0 <= angle(p1,p2,p3) & angle(p1,p2,p3) < 2*PI+2*PI*0 by COMPLEX2:84; then angle(p1,p2,p3)=2*PI*0 or angle(p1,p2,p3)=PI+2*PI*0 by A12,SIN_COS6 :21; hence thesis by A5,A2,COMPLEX2:101; end; suppose sin angle(p5,p4,p6) = 0; then A13: - sin angle(p6,p4,p5) = 0 by Th2; 2*PI*0 <= angle(p6,p4,p5) & angle(p6,p4,p5) < 2*PI+2*PI*0 by COMPLEX2:84; then angle(p6,p4,p5)=2*PI*0 or angle(p6,p4,p5)=PI+2*PI*0 by A13,SIN_COS6 :21; hence thesis by A6,A4,COMPLEX2:101; end; end; end; theorem Th21: p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p6,p4,p5) implies |.p3-p2.|*|.p4-p6.| = |.p1-p3.|*|.p6-p5.| & |.p3-p2.|*|.p5-p4.| = |.p2-p1.|*|.p6-p5.| & |.p1-p3.|*|.p5-p4.| = |.p2-p1.|*|.p4-p6.| proof assume p1,p2,p3 is_a_triangle; then p1,p2,p3 are_mutually_different & angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI by Th20; then A1: p3<>p2 & p3<>p1 & p2<>p1 by ZFMISC_1:def 5; assume p4,p5,p6 is_a_triangle; then A2: p4,p5,p6 are_mutually_different & angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI by Th20; then A3: p5<>p6 & p5<>p4 & p6<>p4 by ZFMISC_1:def 5; assume A4: angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p6,p4,p5); A5: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by A1,EUCLID_3:6; A6: euc2cpx(p5)<> euc2cpx(p6) & euc2cpx(p5)<> euc2cpx(p4) & euc2cpx(p6)<> euc2cpx(p4) by A3,EUCLID_3:6; A7: angle(p2,p3,p1) = angle(p5,p6,p4) proof per cases by A5,A6,COMPLEX2:102; suppose angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1) = PI & angle(p6,p4,p5)+angle(p4,p5,p6)+angle(p5,p6,p4) = PI; hence thesis by A4; end; suppose angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1) = 5*PI & angle(p6,p4,p5)+angle(p4,p5,p6)+angle(p5,p6,p4) = 5*PI; hence thesis by A4; end; suppose angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1) = PI & angle(p6,p4,p5)+angle(p4,p5,p6)+angle(p5,p6,p4) = 5*PI; then A8: angle(p2,p3,p1)-angle(p5,p6,p4) = -4*PI by A4; A9: angle(p2,p3,p1)>=0 & angle(p5,p6,p4)<2*PI by COMPLEX2:84; then -angle(p5,p6,p4) > -2*PI by XREAL_1:26; then angle(p2,p3,p1)+(-angle(p5,p6,p4)) > 0+(-2*PI) by A9,XREAL_1:10; then 4*PI < 2*PI by A8,XREAL_1:26; then 4*PI/PI < 2*PI/PI by XREAL_1:76; then 4 < 2*PI/PI by XCMPLX_1:90; then 4 < 2 by XCMPLX_1:90; hence thesis; end; suppose A10: angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1)=5*PI & angle(p6,p4,p5)+angle(p4,p5,p6)+angle(p5,p6,p4)=PI; A11: angle(p2,p3,p1)<2*PI & angle(p5,p6,p4)>=0 by COMPLEX2:84; then -angle(p5,p6,p4) <= -0 by XREAL_1:26; then angle(p2,p3,p1)+(-angle(p5,p6,p4)) < 2*PI+(-0) by A11,XREAL_1:10; then 4*PI/PI < 2*PI/PI by A10,A4,XREAL_1:76; then 4 < 2*PI/PI by XCMPLX_1:90; then 4 < 2 by XCMPLX_1:90; hence thesis; end; end; hence |.p3-p2.|*|.p4-p6.| = |.p1-p3.|*|.p6-p5.| by A2,A1,A3,A4,Lm18; thus |.p3-p2.|*|.p5-p4.| = |.p2-p1.|*|.p6-p5.| by A2,A1,A3,A4,A7,Lm18; thus |.p1-p3.|*|.p5-p4.| = |.p2-p1.|*|.p4-p6.| by A2,A1,A3,A4,A7,Lm18; end; Lm19: p3<>p2 & p3<>p1 & p2<>p1 & p4<>p5 & p4<>p6 & p5<>p6 & angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI & angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI & angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p5,p6,p4) implies |.p2-p3.|*|.p4-p6.| = |.p3-p1.|*|.p5-p4.| proof assume A1: p3<>p2 & p3<>p1 & p2<>p1; then A2: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by EUCLID_3:6; assume A3: p4<>p5 & p4<>p6 & p5<>p6; then A4: euc2cpx(p4)<> euc2cpx(p5) & euc2cpx(p4)<> euc2cpx(p6) & euc2cpx(p5)<> euc2cpx(p6) by EUCLID_3:6; assume A5: angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI; assume A6: angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI; assume A7: angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p5,p6,p4); then A8: sin angle(p1,p2,p3)*sin angle(p4,p6,p5) = sin angle(p4,p5,p6)*(-sin angle(p5,p6,p4)) by Th2 .= (-sin angle(p6,p5,p4))*(-sin angle(p3,p1,p2)) by A7,Th2 .= sin angle(p6,p5,p4)*sin angle(p3,p1,p2); per cases; suppose A9: sin angle(p1,p2,p3)*sin angle(p4,p6,p5)<>0; A10: |.p4-p5.|*sin angle(p6,p5,p4)=|.p4-p6.|*sin angle(p4,p6,p5) by Th6,A3; A11: |.p3-p2.|*|.p4-p6.|*sin angle(p1,p2,p3)*sin angle(p4,p6,p5) = (|.p3-p2.|*sin angle(p1,p2,p3))*(|.p4-p6.|*sin angle(p4,p6,p5)) .= (|.p3-p1.|*sin angle(p3,p1,p2))*(|.p4-p5.|*sin angle(p6,p5,p4)) by A1,Th6,A10 .= |.p3-p1.|*|.p4-p5.|*sin angle(p6,p5,p4)*sin angle(p3,p1,p2); thus |.p2-p3.|*|.p4-p6.| = |.p3-p2.|*|.p4-p6.| by Lm2 .= (|.p3-p2.|*|.p4-p6.|)*(sin angle(p1,p2,p3)*sin angle(p4,p6,p5))/ (sin angle(p1,p2,p3)*sin angle(p4,p6,p5)) by A9,XCMPLX_1:90 .= ((|.p3-p1.|*|.p4-p5.|)*(sin angle(p6,p5,p4)*sin angle(p3,p1,p2)))/ (sin angle(p6,p5,p4)*sin angle(p3,p1,p2)) by A11,A8 .= |.p3-p1.|*|.p4-p5.| by A8,A9,XCMPLX_1:90 .= |.p3-p1.|*|.p5-p4.| by Lm2; end; suppose A12: sin angle(p1,p2,p3)*sin angle(p4,p6,p5)=0; per cases by A12,XCMPLX_1:6; suppose A13: sin angle(p1,p2,p3) = 0; 2*PI*0 <= angle(p1,p2,p3) & angle(p1,p2,p3) < 2*PI+2*PI*0 by COMPLEX2:84; then angle(p1,p2,p3)=2*PI*0 or angle(p1,p2,p3)=PI+2*PI*0 by A13,SIN_COS6 :21; hence thesis by A5,A2,COMPLEX2:101; end; suppose A14: sin angle(p4,p6,p5) = 0; 2*PI*0 <= angle(p4,p6,p5) & angle(p4,p6,p5) < 2*PI+2*PI*0 by COMPLEX2:84; then angle(p4,p6,p5)=2*PI*0 or angle(p4,p6,p5)=PI+2*PI*0 by A14,SIN_COS6 :21; then angle(p6,p5,p4) = 0 & angle(p5,p4,p6) = PI or angle(p6,p5,p4) = PI & angle(p5,p4,p6) = 0 by A4,COMPLEX2:101,A6,COMPLEX2:96; hence thesis by A6,COMPLEX2:96; end; end; end; theorem Th22: p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p5,p6,p4) implies |.p2-p3.| * |.p4-p6.| = |.p3-p1.| * |.p5-p4.| & |.p2-p3.| * |.p6-p5.| = |.p1-p2.| * |.p5-p4.| & |.p3-p1.| * |.p6-p5.| = |.p1-p2.| * |.p4-p6.| proof assume p1,p2,p3 is_a_triangle; then A1: p1,p2,p3 are_mutually_different & angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI by Th20; then A2: p3<>p2 & p3<>p1 & p2<>p1 by ZFMISC_1:def 5; assume p4,p5,p6 is_a_triangle; then A3: p4,p5,p6 are_mutually_different & angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI by Th20; then A4: p4<>p5 & p4<>p6 & p5<>p6 by ZFMISC_1:def 5; assume A5: angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p5,p6,p4); A6: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by A2,EUCLID_3:6; A7: euc2cpx(p4)<> euc2cpx(p5) & euc2cpx(p4)<> euc2cpx(p6) & euc2cpx(p5)<> euc2cpx(p6) by A4,EUCLID_3:6; A8: angle(p2,p3,p1) = angle(p6,p4,p5) proof per cases by A6,A7,COMPLEX2:102; suppose angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1) = PI & angle(p5,p6,p4)+angle(p6,p4,p5)+angle(p4,p5,p6) = PI; hence thesis by A5; end; suppose angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1) = 5*PI & angle(p5,p6,p4)+angle(p6,p4,p5)+angle(p4,p5,p6) = 5*PI; hence thesis by A5; end; suppose angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1) = PI & angle(p5,p6,p4)+angle(p6,p4,p5)+angle(p4,p5,p6) = 5*PI; then A9: angle(p2,p3,p1)-angle(p6,p4,p5) = -4*PI by A5; A10: angle(p2,p3,p1)>=0 & angle(p6,p4,p5)<2*PI by COMPLEX2:84; then -angle(p6,p4,p5) > -2*PI by XREAL_1:26; then angle(p2,p3,p1)+(-angle(p6,p4,p5)) > 0+(-2*PI) by A10,XREAL_1:10; then 4*PI < 2*PI by A9,XREAL_1:26; then 4*PI/PI < 2*PI/PI by XREAL_1:76; then 4 < 2*PI/PI by XCMPLX_1:90; then 4 < 2 by XCMPLX_1:90; hence thesis; end; suppose A11: angle(p3,p1,p2)+angle(p1,p2,p3)+angle(p2,p3,p1)=5*PI & angle(p5,p6,p4)+angle(p6,p4,p5)+angle(p4,p5,p6)=PI; A12: angle(p2,p3,p1)<2*PI & angle(p6,p4,p5)>=0 by COMPLEX2:84; then -angle(p6,p4,p5) <= -0 by XREAL_1:26; then angle(p2,p3,p1)+(-angle(p6,p4,p5)) < 2*PI+(-0) by A12,XREAL_1:10; then 4*PI/PI < 2*PI/PI by A11,A5,XREAL_1:76; then 4 < 2*PI/PI by XCMPLX_1:90; then 4 < 2 by XCMPLX_1:90; hence thesis; end; end; thus |.p2-p3.|*|.p4-p6.| = |.p3-p1.|*|.p5-p4.| by A1,A3,A2,A4,A5,Lm19; thus |.p2-p3.|*|.p6-p5.| = |.p1-p2.|*|.p5-p4.| by A3,A2,A4,A5,A8,Lm19; thus |.p3-p1.|*|.p6-p5.| = |.p1-p2.|*|.p4-p6.| by A3,A2,A4,A5,A8,Lm19; end; theorem Th23: p1,p2,p3 are_mutually_different & angle(p1,p2,p3)<=PI implies angle(p2,p3,p1)<=PI & angle(p3,p1,p2)<=PI proof assume p1,p2,p3 are_mutually_different; then p1<>p2 & p1<>p3 & p2<>p3 by ZFMISC_1:def 5; then euc2cpx(p1)<> euc2cpx(p2) & euc2cpx(p1)<> euc2cpx(p3) & euc2cpx(p2)<> euc2cpx(p3) by EUCLID_3:6; then A1: angle(p1,p2,p3)+angle(p2,p3,p1)+angle(p3,p1,p2)=PI or angle(p1,p2,p3)+angle(p2,p3,p1)+angle(p3,p1,p2)=5*PI by COMPLEX2:102; assume A2: angle(p1,p2,p3)<=PI; angle(p2,p3,p1)< 2*PI & angle(p3,p1,p2)<2*PI by COMPLEX2:84; then angle(p2,p3,p1)+angle(p3,p1,p2)<2*PI+2*PI by XREAL_1:10; then A3: angle(p1,p2,p3)+(angle(p2,p3,p1)+angle(p3,p1,p2))=0 & angle(p2,p3,p1)>= 0 & angle(p3,p1,p2)>=0 by COMPLEX2:84; thus angle(p2,p3,p1)<=PI proof assume angle(p2,p3,p1)>PI; then angle(p1,p2,p3)+angle(p2,p3,p1)>0+PI by A4,XREAL_1:10; hence contradiction by A3,A1,A4,XREAL_1:10; end; thus angle(p3,p1,p2)<=PI proof assume angle(p3,p1,p2)>PI; then angle(p2,p3,p1)+angle(p3,p1,p2)>0+PI by A4,XREAL_1:10; hence contradiction by A3,A1,A4,XREAL_1:10; end; end; theorem Th24: p1,p2,p3 are_mutually_different & angle(p1,p2,p3)>PI implies angle(p2,p3,p1)>PI & angle(p3,p1,p2)>PI proof assume p1,p2,p3 are_mutually_different; then A1: p1<>p2 & p1<>p3 & p2<>p3 by ZFMISC_1:def 5; assume A2: angle(p1,p2,p3)>PI; A3: p2,p3,p1 are_mutually_different by A1,ZFMISC_1:def 5; A4: p3,p1,p2 are_mutually_different by A1,ZFMISC_1:def 5; thus angle(p2,p3,p1)>PI by A2,Th23,A3; thus angle(p3,p1,p2)>PI by A2,Th23,A4; end; ::LIKE JORDAN2C:91 Lm20: for n being Element of NAT, q1 being Point of TOP-REAL n for f being Function of TOP-REAL n,R^1 st (for q being Point of TOP-REAL n holds f.q=|.q-q1.|) holds f is continuous proof let n be Element of NAT; let q1 be Point of TOP-REAL n; let f be Function of TOP-REAL n,R^1; assume A1: (for q being Point of TOP-REAL n holds f.q=|.q-q1.|); reconsider f1=f as Function of TopSpaceMetr(Euclid n),TopSpaceMetr(RealSpace) by TOPMETR:def 7; now let r be real number,u be Element of the carrier of Euclid n,u1 be Element of RealSpace; assume A2: r>0 & u1=f1.u; set s1=r; for w being Element of Euclid n, w1 being Element of RealSpace st w1=f1.w & dist(u,w)0 & for w being Element of Euclid n, w1 being Element of RealSpace st w1=f1.w & dist(u,w)PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI by Th20; then A4: p1<>p2 & p2<>p3 & p1<>p3 by ZFMISC_1:def 5; not p1 in LSeg(p2,p3) & not p2 in LSeg(p3,p1) & not p3 in LSeg(p1,p2) by Def3,A2; then A5: p1,p3,p2 is_a_triangle by Def3; assume A6: angle(p1,p3,p2) = angle(p,p3,p2); assume A7: p1<>p; A8: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by A4,EUCLID_3:6; A9: p<>p2 proof assume p=p2; then angle(p1,p3,p2)=0 by A6,COMPLEX2:93; then angle(p3,p2,p1) = 0 & angle(p2,p1,p3) = PI or angle(p3,p2,p1) = PI & angle(p2,p1,p3) = 0 by A8,COMPLEX2:101; hence contradiction by A3,COMPLEX2:96; end; then A10: p<>p3 & p<>p2 by Def3,A2,A1; A11: angle(p3,p2,p1) = angle(p3,p2,p) by A1,Th10,A9; A12: euc2cpx(p)<> euc2cpx(p3) & euc2cpx(p)<> euc2cpx(p2) by A10,EUCLID_3:6; A13: angle(p2,p1,p3) = angle(p2,p,p3) proof per cases by A8,A12,COMPLEX2:102; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = PI; hence thesis by A6,A11; end; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = 5*PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = 5*PI; hence thesis by A6,A11; end; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = 5*PI; then A14: angle(p2,p1,p3)-angle(p2,p,p3) = -4*PI by A6,A11; A15: angle(p2,p1,p3)>=0 & angle(p2,p,p3)<2*PI by COMPLEX2:84; then -angle(p2,p,p3) > -2*PI by XREAL_1:26; then angle(p2,p1,p3)+(-angle(p2,p,p3)) > 0+(-2*PI) by A15,XREAL_1:10; then 4*PI < 2*PI by A14,XREAL_1:26; then 4*PI/PI < 2*PI/PI by XREAL_1:76; then 4 < 2*PI/PI by XCMPLX_1:90; then 4 < 2 by XCMPLX_1:90; hence thesis; end; suppose A16: angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3)=5*PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3)=PI; A17: angle(p2,p1,p3)<2*PI & angle(p2,p,p3)>=0 by COMPLEX2:84; then -angle(p2,p,p3) <= -0 by XREAL_1:26; then angle(p2,p1,p3)+(-angle(p2,p,p3)) < 2*PI+(-0) by A17,XREAL_1:10; then 4*PI/PI < 2*PI/PI by A16,A6,A11,XREAL_1:76; then 4 < 2*PI/PI by XCMPLX_1:90; then 4 < 2 by XCMPLX_1:90; hence thesis; end; end; p2<>p3 by A3,ZFMISC_1:def 5; then A18: |.p2-p3.|<>0 by Lm1; A19: p,p3,p2 are_mutually_different by A10,A4,ZFMISC_1:def 5; angle(p,p3,p2)<>PI & angle(p3,p2,p)<>PI & angle(p2,p,p3)<>PI by A3,A6,A13,A11,COMPLEX2:96; then p,p3,p2 is_a_triangle by A19,Th20; then |.p2-p3.|*|.p-p2.| = |.p1-p2.|*|.p2-p3.| & |.p2-p3.|*|.p3-p.| = |.p3-p1.|*|.p2-p3.| & |.p1-p2.|*|.p3-p.| = |.p3-p1.|*|.p-p2.| by A5,A6,A13,Th21; then |.p-p2.| = |.p1-p2.| by A18,XCMPLX_1:5; then A20: |.p2-p.| = |.p1-p2.| by Lm2 .= |.p2-p1.| by Lm2; |.p2-p1.|^2 = |.p1-p.|^2 + |.p2-p.|^2 -2*|.p1-p.|*|.p2-p.|*cos angle(p1,p,p2) by Th7 .= |.p1-p.|^2 + |.p2-p.|^2 -2*|.p1-p.|*|.p2-p.|*(-1) by A1,A7,A9,Th8,SIN_COS:82; then A21: 0 = |.p1-p.|*(|.p1-p.| + 2*|.p2-p.|) by A20; per cases by A21,XCMPLX_1:6; suppose |.p1-p.|=0; hence contradiction by A7,Lm1; end; suppose |.p1-p.| + 2*|.p2-p.|=0; then |.p1-p.|=0 by XREAL_1:29; hence contradiction by A7,Lm1; end; end; theorem Th26: p in LSeg(p1,p2) & not p3 in LSeg(p1,p2) & angle(p1,p3,p2) <= PI implies angle(p,p3,p2) <= angle(p1,p3,p2) proof assume A1: p in LSeg(p1,p2); assume A2: not p3 in LSeg(p1,p2); assume A3: angle(p1,p3,p2) <= PI; assume A4: angle(p,p3,p2) > angle(p1,p3,p2); per cases; suppose p=p1; hence contradiction by A4; end; suppose p=p2; then angle(p,p3,p2) = 0 by COMPLEX2:93; hence contradiction by A4,COMPLEX2:84; end; suppose A5: p1=p2; then p in {p2} by A1,TOPREAL1:7; hence contradiction by A4,A5,TARSKI:def 1; end; suppose A6: p<>p2 & p1<>p2 & p<>p1; A7: p3<>p1 & p3<>p2 by A2,TOPREAL1:6; then A8: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by A6,EUCLID_3:6; A9: euc2cpx(p)<> euc2cpx(p3) & euc2cpx(p)<> euc2cpx(p2) & euc2cpx(p)<> euc2cpx(p1) by A1,A2,A6,EUCLID_3:6; A10: angle(p3,p2,p1) = angle(p3,p2,p) by A6,A1,Th10; angle(p1,p3,p2)+angle(p2,p1,p3) = angle(p,p3,p2)+angle(p2,p,p3) proof per cases by A8,A9,COMPLEX2:102; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = PI; hence thesis by A10; end; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = 5*PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = 5*PI; hence thesis by A10; end; suppose A11: angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = 5*PI; A12: angle(p1,p3,p2)>=0 & angle(p2,p1,p3)>=0 & angle(p,p3,p2)<2*PI & angle(p2,p,p3)<2*PI by COMPLEX2:84; then -angle(p2,p,p3) > -2*PI & -angle(p,p3,p2) > -2*PI by XREAL_1:26; then A13: -angle(p,p3,p2)+(-angle(p2,p,p3)) > -2*PI+(-2*PI) by XREAL_1:10; angle(p1,p3,p2)+angle(p2,p1,p3) >= 0+0 by A12,XREAL_1:9; then angle(p1,p3,p2)+angle(p2,p1,p3)+(-angle(p,p3,p2)-angle(p2,p,p3)) > 0+0+(-2*PI-2*PI) by A13,XREAL_1:10; hence thesis by A11,A10; end; suppose A14: angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3)=5*PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3)=PI; A15: angle(p2,p1,p3)<2*PI & angle(p1,p3,p2)<2*PI & angle(p,p3,p2)>=0 & angle(p2,p,p3)>=0 by COMPLEX2:84; then A16: angle(p2,p1,p3)+angle(p1,p3,p2) <2*PI+2*PI by XREAL_1:10; -angle(p2,p,p3) <= -0 & -angle(p,p3,p2) <= -0 by A15,XREAL_1:26; then -angle(p,p3,p2)+(-angle(p2,p,p3)) <= 0+0 by XREAL_1:9; then angle(p2,p1,p3)+angle(p1,p3,p2)+(-angle(p,p3,p2)-angle(p2,p,p3)) < 2*PI+2*PI+(0+0) by A16,XREAL_1:10; hence thesis by A14,A10; end; end; then A17: angle(p2,p1,p3) > angle(p2,p,p3) by XREAL_1:10,A4; per cases by Th13,A1,A8,A9,COMPLEX2:102; suppose angle(p2,p,p3)+angle(p3,p,p1)=PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = PI; then angle(p1,p3,p)+angle(p,p1,p3) < 0+angle(p,p1,p3) by A1,Th9,A17; then angle(p1,p3,p) < 0 by XREAL_1:8; hence contradiction by COMPLEX2:84; end; suppose angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = PI; then A18: angle(p2,p,p3) = angle(p,p1,p3)+angle(p1,p3,p)+2*PI; angle(p,p1,p3)>=0 & angle(p1,p3,p)>=0 by COMPLEX2:84; then angle(p,p1,p3)+angle(p1,p3,p) >= 0+0 by XREAL_1:9; then angle(p2,p,p3) >= 0+2*PI by A18,XREAL_1:8; hence contradiction by COMPLEX2:84; end; suppose A19: angle(p2,p,p3)+angle(p3,p,p1)=PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = 5*PI; angle(p,p1,p3)<2*PI & angle(p1,p3,p)<2*PI by COMPLEX2:84; then angle(p,p1,p3)+angle(p1,p3,p) < 2*PI+2*PI by XREAL_1:10; then angle(p2,p,p3)+4*PI < 0+4*PI by A19; then angle(p2,p,p3) < 0 by XREAL_1:8; hence contradiction by COMPLEX2:84; end; suppose A20: angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = 5*PI; p1,p3,p2 are_mutually_different by A6,A7,ZFMISC_1:def 5; then angle(p2,p1,p3) <= PI by A3,Th23; then A21: angle(p,p1,p3) <= PI by Th9,A1,A6; p,p1,p3 are_mutually_different by A1,A2,A6,A7,ZFMISC_1:def 5; then angle(p1,p3,p)<=PI & angle(p3,p,p1)<=PI by A21,Th23; then angle(p3,p,p1)+angle(p1,p3,p) <= PI+PI by XREAL_1:9; then angle(p3,p,p1)+angle(p1,p3,p)+angle(p,p1,p3) <= 2*PI+PI by A21,XREAL_1:9; hence contradiction by A20,XREAL_1:70; end; end; end; theorem Th27: p in LSeg(p1,p2) & not p3 in LSeg(p1,p2) & angle(p1,p3,p2) > PI & p<>p2 implies angle(p,p3,p2) >= angle(p1,p3,p2) proof assume A1: p in LSeg(p1,p2); assume A2: not p3 in LSeg(p1,p2); assume A3: angle(p1,p3,p2) > PI; assume A4: p<>p2; assume A5: angle(p,p3,p2) < angle(p1,p3,p2); per cases; suppose p=p1; hence contradiction by A5; end; suppose A6: p1=p2; then p in {p2} by A1,TOPREAL1:7; hence contradiction by A5,A6,TARSKI:def 1; end; suppose A7: p1<>p2 & p<>p1; A8: p3<>p1 & p3<>p2 by A2,TOPREAL1:6; then A9: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p1) by A7,EUCLID_3:6; A10: euc2cpx(p)<> euc2cpx(p3) & euc2cpx(p)<> euc2cpx(p2) & euc2cpx(p)<> euc2cpx(p1) by A1,A4,A2,A7,EUCLID_3:6; A11: angle(p3,p2,p1) = angle(p3,p2,p) by A4,A1,Th10; angle(p1,p3,p2)+angle(p2,p1,p3) = angle(p,p3,p2)+angle(p2,p,p3) proof per cases by A9,A10,COMPLEX2:102; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = PI; hence thesis by A11; end; suppose angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = 5*PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = 5*PI; hence thesis by A11; end; suppose A12: angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3) = PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3) = 5*PI; A13: angle(p1,p3,p2)>=0 & angle(p2,p1,p3)>=0 & angle(p,p3,p2)<2*PI & angle(p2,p,p3)<2*PI by COMPLEX2:84; then -angle(p2,p,p3) > -2*PI & -angle(p,p3,p2) > -2*PI by XREAL_1:26; then A14: -angle(p,p3,p2)+(-angle(p2,p,p3)) > -2*PI+(-2*PI) by XREAL_1:10; angle(p1,p3,p2)+angle(p2,p1,p3) >= 0+0 by A13,XREAL_1:9; then angle(p1,p3,p2)+angle(p2,p1,p3)+(-angle(p,p3,p2)-angle(p2,p,p3)) > 0+0+(-2*PI-2*PI) by A14,XREAL_1:10; hence thesis by A12,A11; end; suppose A15: angle(p1,p3,p2)+angle(p3,p2,p1)+angle(p2,p1,p3)=5*PI & angle(p,p3,p2)+angle(p3,p2,p)+angle(p2,p,p3)=PI; A16: angle(p2,p1,p3)<2*PI & angle(p1,p3,p2)<2*PI & angle(p,p3,p2)>=0 & angle(p2,p,p3)>=0 by COMPLEX2:84; then A17: angle(p2,p1,p3)+angle(p1,p3,p2) <2*PI+2*PI by XREAL_1:10; -angle(p2,p,p3) <= -0 & -angle(p,p3,p2) <= -0 by A16,XREAL_1:26; then -angle(p,p3,p2)+(-angle(p2,p,p3)) <= 0+0 by XREAL_1:9; then angle(p2,p1,p3)+angle(p1,p3,p2)+(-angle(p,p3,p2)-angle(p2,p,p3)) < 2*PI+2*PI+(0+0) by A17,XREAL_1:10; hence thesis by A15,A11; end; end; then angle(p2,p1,p3) < angle(p2,p,p3) by XREAL_1:10,A5; then A18: angle(p,p1,p3) < angle(p2,p,p3) by A1,Th9; per cases by Th13,A1,A9,A10,COMPLEX2:102; suppose A19: angle(p2,p,p3)+angle(p3,p,p1) = PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = PI; p1,p3,p2 are_mutually_different by A7,A8,ZFMISC_1:def 5; then angle(p2,p1,p3) > PI by A3,Th24; then A20: angle(p,p1,p3) > PI by Th9,A1,A7; p,p1,p3 are_mutually_different by A1,A2,A7,A8,ZFMISC_1:def 5; then angle(p1,p3,p)>PI & angle(p3,p,p1)>PI by A20,Th24; then angle(p3,p,p1)+angle(p1,p3,p) > PI+PI by XREAL_1:10; then A21: angle(p3,p,p1)+angle(p1,p3,p)+angle(p,p1,p3) > 2*PI+PI by A20,XREAL_1:10; 1*PI<3*PI by XREAL_1:70; hence contradiction by A19,A21; end; suppose angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = PI; then A22: angle(p2,p,p3) = angle(p,p1,p3)+angle(p1,p3,p)+2*PI; angle(p,p1,p3)>=0 & angle(p1,p3,p)>=0 by COMPLEX2:84; then angle(p,p1,p3)+angle(p1,p3,p) >= 0+0 by XREAL_1:9; then angle(p2,p,p3) >= 0+2*PI by A22,XREAL_1:8; hence contradiction by COMPLEX2:84; end; suppose A23: angle(p2,p,p3)+angle(p3,p,p1)=PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = 5*PI; angle(p,p1,p3)<2*PI & angle(p1,p3,p)<2*PI by COMPLEX2:84; then angle(p,p1,p3)+angle(p1,p3,p) < 2*PI+2*PI by XREAL_1:10; then angle(p2,p,p3)+4*PI < 0+4*PI by A23; then angle(p2,p,p3) < 0 by XREAL_1:8; hence contradiction by COMPLEX2:84; end; suppose angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)+angle(p,p1,p3)+angle(p1,p3,p) = 5*PI; then angle(p2,p,p3)+2*PI = angle(p,p1,p3)+angle(p1,p3,p); then angle(p2,p,p3)+2*PI < angle(p2,p,p3)+angle(p1,p3,p) by A18,XREAL_1: 8; then 2*PI < angle(p1,p3,p) by XREAL_1:8; hence contradiction by COMPLEX2:84; end; end; end; theorem Th28: p in LSeg(p1,p2) & not p3 in LSeg(p1,p2) implies ex p4 st p4 in LSeg(p1,p2) & angle(p1,p3,p4) = angle(p,p3,p2) proof assume A1: p in LSeg(p1,p2); assume A2: not p3 in LSeg(p1,p2); per cases; suppose A3: p1=p2; then LSeg(p1,p2) = {p1} by TOPREAL1:7; then A4: p=p1 & p=p2 by A1,A3,TARSKI:def 1; set p4=p; take p4; thus p4 in LSeg(p1,p2) by A1; thus angle(p1,p3,p4) = angle(p,p3,p2) by A4; end; suppose A5: p=p2 or p1 in LSeg(p2,p3); set p4=p1; take p4; thus p4 in LSeg(p1,p2) by TOPREAL1:6; per cases by A5; suppose A6: p=p2; thus angle(p1,p3,p4) = 0 by COMPLEX2:93 .= angle(p,p3,p2) by A6,COMPLEX2:93; end; suppose A7: p1 in LSeg(p2,p3); p2 in LSeg(p3,p2) by TOPREAL1:6; then A8: LSeg(p1,p2) c= LSeg(p3,p2) by A7,TOPREAL1:12; thus angle(p1,p3,p4) = 0 by COMPLEX2:93 .= angle(p2,p3,p2) by COMPLEX2:93 .= angle(p,p3,p2) by A1,A2,A8,Th9; end; end; suppose A9: p=p1 or p2 in LSeg(p1,p3); set p4=p2; take p4; thus p4 in LSeg(p1,p2) by TOPREAL1:6; per cases by A9; suppose p=p1; hence angle(p1,p3,p4) = angle(p,p3,p2); end; suppose A10: p2 in LSeg(p1,p3); p1 in LSeg(p1,p3) by TOPREAL1:6; then LSeg(p1,p2) c= LSeg(p1,p3) by A10,TOPREAL1:12; hence angle(p1,p3,p4) = angle(p,p3,p2) by A1,A2,Th9; end; end; suppose A11: p1<>p2 & p<>p1 & p<>p2 & not p1 in LSeg(p2,p3) & not p2 in LSeg(p1,p3); then consider f be Function of I[01], (TOP-REAL 2) | LSeg(p1,p2) such that A12: (for x being Real st x in [.0,1.] holds f.x = (1-x)*p1 + x*p2) and A13: f is_homeomorphism & f.0 = p1 & f.1 = p2 by JORDAN5A:4; consider f1 be Function of TOP-REAL 2, R^1 such that A14: for q being Point of TOP-REAL 2 holds f1.q=|.q-p1.| and A15: f1 is continuous by Lm21; consider f2 be Function of TOP-REAL 2, R^1 such that A16: for q being Point of TOP-REAL 2 holds f2.q=|.p1-p3.| and A17: f2 is continuous by JGRAPH_2:30; consider f3 be Function of TOP-REAL 2, R^1 such that A18: for q being Point of TOP-REAL 2 holds f3.q=|.q-p3.| and A19: f3 is continuous by Lm21; consider f12 be Function of TOP-REAL 2, R^1 such that A20: for q being Point of TOP-REAL 2,r1,r2 being real number st f1.q=r1 & f1.q=r2 holds f12.q=r1*r2 and A21: f12 is continuous by A15,JGRAPH_2:35; consider f22 be Function of TOP-REAL 2, R^1 such that A22: for q being Point of TOP-REAL 2,r1,r2 being real number st f2.q=r1 & f2.q=r2 holds f22.q=r1*r2 and A23: f22 is continuous by A17,JGRAPH_2:35; consider f32 be Function of TOP-REAL 2, R^1 such that A24: for q being Point of TOP-REAL 2,r1,r2 being real number st f3.q=r1 & f3.q=r2 holds f32.q=r1*r2 and A25: f32 is continuous by A19,JGRAPH_2:35; consider f0 be Function of (TOP-REAL 2) | LSeg(p1,p2),TOP-REAL 2 such that A26: for q being Point of (TOP-REAL 2) | LSeg(p1,p2) holds f0.q=q and A27: f0 is continuous by JGRAPH_6:14; consider f4 be Function of TOP-REAL 2, R^1 such that A28: for q being Point of TOP-REAL 2,r1,r2 being real number st f12.q=r1 & f22.q=r2 holds f4.q=r1-r2 and A29: f4 is continuous by A21,A23,JGRAPH_2:31; consider f5 be Function of TOP-REAL 2, R^1 such that A30: for q being Point of TOP-REAL 2,r1,r2 being real number st f4.q=r1 & f32.q=r2 holds f5.q=r1-r2 and A31: f5 is continuous by A29,A25,JGRAPH_2:31; consider f6 be Function of TOP-REAL 2, R^1 such that A32: for q being Point of TOP-REAL 2,r1,r2 being real number st f2.q=r1 & f3.q=r2 holds f6.q=r1*r2 and A33: f6 is continuous by A17,A19,JGRAPH_2:35; reconsider f7=f5*f0 as continuous Function of (TOP-REAL 2) | LSeg(p1,p2), R^1 by A27,A31,TOPS_2:58,FUNCT_2:19; reconsider f8=f6*f0 as continuous Function of (TOP-REAL 2) | LSeg(p1,p2), R^1 by A27,A33,TOPS_2:58,FUNCT_2:19; A34: for q being Point of (TOP-REAL 2) | LSeg(p1,p2) holds q is Point of TOP-REAL 2 & q in LSeg(p1,p2) proof let q be Point of (TOP-REAL 2) | LSeg(p1,p2); A35: q in the carrier of (TOP-REAL 2) | LSeg(p1,p2); then q in LSeg(p1,p2) by PRE_TOPC:29; hence q is Point of TOP-REAL 2; thus q in LSeg(p1,p2) by A35,PRE_TOPC:29; end; A36: for q being Point of (TOP-REAL 2) | LSeg(p1,p2), q1 being Point of TOP-REAL 2 st q=q1 holds f8.q = |.p1-p3.|*|.q1-p3.| proof let q be Point of (TOP-REAL 2) | LSeg(p1,p2); let q1 be Point of TOP-REAL 2; assume A37: q=q1; dom f8 = the carrier of (TOP-REAL 2) | LSeg(p1,p2) by FUNCT_2:def 1; then A38: f8.q = f6.(f0.q) by FUNCT_1:22 .= f6.q by A26; f6.q = f2.q*f3.q & f2.q = |.p1-p3.| & f3.q = |.q1-p3.| by A37,A18,A16,A32; hence f8.q = |.p1-p3.|*|.q1-p3.| by A38; end; A39: p1<>p3 by A2,TOPREAL1:6; for q being Point of (TOP-REAL 2) | LSeg(p1,p2) holds f8.q<>0 proof let q be Point of (TOP-REAL 2) | LSeg(p1,p2); reconsider q1=q as Point of TOP-REAL 2 by A34; A40: f8.q = |.p1-p3.|*|.q1-p3.| by A36; assume A41: f8.q=0; per cases by A41,A40,XCMPLX_1:6; suppose |.p1-p3.|=0; hence contradiction by A39,Lm1; end; suppose |.q1-p3.|=0; then q = p3 by Lm1; hence contradiction by A2,A34; end; end; then consider f9 be Function of (TOP-REAL 2) | LSeg(p1,p2), R^1 such that A42: for q being Point of (TOP-REAL 2) | LSeg(p1,p2), r1,r2 being real number st f7.q=r1 & f8.q=r2 holds f9.q=r1/r2 and A43: f9 is continuous by JGRAPH_2:37; f is continuous by A13,TOPS_2:def 5; then reconsider g=f9*f as continuous Function of Closed-Interval-TSpace(0,1), R^1 by A43,TOPS_2:58,FUNCT_2:19,TOPMETR:27; A44: dom g = [.0,1.] by BORSUK_1:83,TOPMETR:27,FUNCT_2:def 1; A45: for q being Point of (TOP-REAL 2) | LSeg(p1,p2), q1 being Point of TOP-REAL 2 st q=q1 holds f9.q = (|.q1-p1.|^2-|.p1-p3.|^2-|.q1-p3.|^2)/(|.p1-p3.|*|.q1-p3.|) proof let q be Point of (TOP-REAL 2) | LSeg(p1,p2); let q1 be Point of TOP-REAL 2; assume A46: q=q1; A47: q is Point of TOP-REAL 2 by A34; A48: f9.q = f7.q/f8.q by A42; dom f7 = the carrier of (TOP-REAL 2) | LSeg(p1,p2) by FUNCT_2:def 1; then A49: f7.q = f5.(f0.q) by FUNCT_1:22 .= f5.q by A26 .= f4.q-f32.q by A47,A30 .= (f12.q-f22.q)-f32.q by A47,A28 .= f12.q-f22.q-f3.q*f3.q by A47,A24 .= f1.q*f1.q-f22.q-f3.q*f3.q by A47,A20 .= f1.q*f1.q-f2.q*f2.q-f3.q*f3.q by A47,A22; f1.q=|.q1-p1.| & f2.q=|.p1-p3.| & f3.q=|.q1-p3.| by A46,A14,A18,A16; hence f9.q =(|.q1-p1.|^2-|.p1-p3.|^2-|.q1-p3.|^2)/(|.p1-p3.|*|.q1-p3.|) by A49,A46,A36,A48; end; A50: |.p1-p3.|<>0 by A39,Lm1; A51: p2<>p3 by A2,TOPREAL1:6; then A52: |.p2-p3.|<>0 by Lm1; A53: |.p-p3.|<>0 by A2,A1,Lm1; set a=g.0; 0 in {r where r is Real:0 <= r & r <= 1}; then 0 in dom g by A44,RCOMP_1:def 1; then A54: g.0 = f9.p1 by A13,FUNCT_1:22; p1 in LSeg(p1,p2) by TOPREAL1:6; then reconsider q1=p1 as Point of (TOP-REAL 2) | LSeg(p1,p2) by PRE_TOPC:29; A55: f9.q1 = (|.p1-p1.|^2-|.p1-p3.|^2-|.p1-p3.|^2)/(|.p1-p3.|*|.p1-p3.|) by A45 .= (0^2-|.p1-p3.|^2-|.p1-p3.|^2)/(|.p1-p3.|*|.p1-p3.|) by Lm1 .= (-2)*|.p1-p3.|^2/(|.p1-p3.|*|.p1-p3.|) .= -2 by A50,XCMPLX_1:90,XCMPLX_1:6; set b=g.1; 1 in {r where r is Real:0 <= r & r <= 1}; then 1 in dom g by A44,RCOMP_1:def 1; then A56: g.1 = f9.p2 by A13,FUNCT_1:22; p2 in LSeg(p1,p2) by TOPREAL1:6; then reconsider q2=p2 as Point of (TOP-REAL 2) | LSeg(p1,p2) by PRE_TOPC:29; A57: f9.q2 = (|.p2-p1.|^2-|.p1-p3.|^2-|.p2-p3.|^2)/(|.p1-p3.|*|.p2-p3.|) by A45; |.p2-p1.|^2 = |.p1-p3.|^2 + |.p2-p3.|^2 - 2*|.p1-p3.|*|.p2-p3.|* cos angle(p1,p3,p2) by Th7; then A58: f9.q2 = (-2)*(|.p1-p3.|*|.p2-p3.|* cos angle(p1,p3,p2))/(|.p1-p3.|*|.p2-p3.|) by A57 .= (-2)*((|.p1-p3.|*|.p2-p3.|* cos angle(p1,p3,p2))/(|.p1-p3.|*|.p2-p3.|)) by XCMPLX_1:75 .= (-2)*cos angle(p1,p3,p2) by XCMPLX_1:90,A50,A52,XCMPLX_1:6; set d = (|.p2-p.|^2 - |.p-p3.|^2 - |.p2-p3.|^2)/(|.p-p3.|*|.p2-p3.|); |.p2-p.|^2 = |.p-p3.|^2 + |.p2-p3.|^2 - 2*|.p-p3.|*|.p2-p3.|* cos angle(p,p3,p2) by Th7; then A59: d = (-2)*(|.p-p3.|*|.p2-p3.|* cos angle(p,p3,p2))/(|.p-p3.|*|.p2- p3.|) .= (-2)*((|.p-p3.|*|.p2-p3.|* cos angle(p,p3,p2))/(|.p-p3.|*|.p2-p3.|)) by XCMPLX_1:75 .= (-2)*cos angle(p,p3,p2) by XCMPLX_1:90,A52,A53,XCMPLX_1:6; A60: cos angle(p,p3,p2) <> 1 proof assume A61: cos angle(p,p3,p2) = 1; 0 <= angle(p,p3,p2) & angle(p,p3,p2) < 2*PI by COMPLEX2:84; then A62: angle(p,p3,p2) = 0 by A61,COMPTRIG:79; A63: euc2cpx(p)<> euc2cpx(p3) & euc2cpx(p)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p2) by A2,A1,A11,A51,EUCLID_3:6; per cases by A63,A62,COMPLEX2:101; suppose angle(p3,p2,p) = 0 & angle(p2,p,p3) = PI; then p in LSeg(p2,p3) by Th11; hence contradiction by A2,A1,A39,A11,Th12; end; suppose angle(p3,p2,p) = PI & angle(p2,p,p3) = 0; then angle(p3,p2,p1) = PI by A1,A11,Th10; hence contradiction by A11,Th11; end; end; then A64: a<>d by A59,A55,A54; 1*(-2) <= cos angle(p,p3,p2)*(-2) by XREAL_1:67,SIN_COS6:6; then A65: a PI; then A74: angle(p,p3,p2) >= angle(p1,p3,p2) by A1,A2,A11,Th27; p1,p2,p3 is_a_triangle by Def3,A11,A2; then A75: angle(p,p3,p2) > angle(p1,p3,p2) by A74,XXREAL_0:1,A11,A1, Th25; A76: [.PI,2*PI.] /\ (dom cos) = [.PI,2*PI.] by XBOOLE_1:28,SIN_COS:27; PI <= angle(p,p3,p2) & angle(p,p3,p2) <= 2*PI by COMPLEX2:84,A73,A74,XXREAL_0:2; then A77: angle(p,p3,p2) in [.PI,2*PI.] /\ (dom cos) by A76,XXREAL_1 :1; angle(p1,p3,p2) <= 2*PI by COMPLEX2:84; then A78: angle(p1,p3,p2) in [.PI,2*PI.] /\ (dom cos) by A76,A73, XXREAL_1:1; A79: cos.angle(p1,p3,p2) = cos angle(p1,p3,p2) & cos.angle(p,p3,p2) = cos angle(p,p3,p2) by SIN_COS:def 23; cos is_increasing_on [.PI+2*PI*0,2*PI+2*PI*0.] by SIN_COS6:56; then cos.angle(p1,p3,p2) < cos.angle(p,p3,p2) by A75,A77,A78,RFUNCT_2:def 2; hence thesis by A56,A59,A58,A79,XREAL_1:71; end; end; then consider rc be Element of REAL such that A80: g.rc = d & 00 by A2,A83,Lm1; A87: d = (-2)*(r2* cos angle(p1,p3,p4))/r2 by A85,A84,A80,A82,A81,FUNCT_1:22 .= (-2)*((r2* cos angle(p1,p3,p4))/r2) by XCMPLX_1:75 .= (-2)*cos angle(p1,p3,p4) by A86,XCMPLX_1:90,A50,XCMPLX_1:6; A88: p1<>p4 proof assume A89: p1=p4; 0 = 0 * |.p1-p1.| .= 2*|.p1-p3.|*|.p1-p3.| - 2*|.p1-p3.|*|.p1-p3.|*cos angle(p1,p3,p4) by A89,A85,Lm1; then A90: |.p1-p3.|*|.p1-p3.| = |.p1-p3.|*|.p1-p3.|*cos angle(p1,p3,p4); |.p1-p3.|<>0 by Lm1,A39; hence contradiction by A60,A87,A90,A59,XCMPLX_1:7,XCMPLX_1:6; end; A91: p3<>p4 by A80,SPPOL_1:22,A2; per cases; suppose A92: angle(p,p3,p2) <= PI; p,p3,p2 are_mutually_different by A2,A1,A11,A51,ZFMISC_1:def 5; then angle(p3,p2,p) <= PI by A92,Th23; then A93: angle(p3,p2,p1) <= PI by A11,A1,Th10; p3,p2,p1 are_mutually_different by A51,A11,A39,ZFMISC_1:def 5; then angle(p2,p1,p3) <= PI by A93,Th23; then A94: angle(p4,p1,p3) <= PI by A88,Th9,A80,SPPOL_1:22; p4,p1,p3 are_mutually_different by A39,A88,A91,ZFMISC_1:def 5; then A95: angle(p1,p3,p4) <= PI by A94,Th23; A96: 0 <= angle(p,p3,p2) & 0 <= angle(p1,p3,p4) by COMPLEX2:84; hence angle(p1,p3,p4) = arccos cos angle(p1,p3,p4) by A95,SIN_COS6:94 .= angle(p,p3,p2) by A87,A59,A92,A96,SIN_COS6:94; end; suppose A97: angle(p,p3,p2) > PI; then -angle(p,p3,p2)<-PI by XREAL_1:26; then A98: -angle(p,p3,p2)+2*PI < -PI+2*PI by XREAL_1:8; A99: cos(2*PI - angle(p1,p3,p4)) = cos.(-angle(p1,p3,p4)+2*PI*1) by SIN_COS:def 23 .= cos.(-angle(p1,p3,p4)) by SIN_COS6:10 .= cos.(angle(p1,p3,p4)) by SIN_COS:33 .= cos angle(p,p3,p2) by A87,A59,SIN_COS:def 23 .= cos.(angle(p,p3,p2)) by SIN_COS:def 23 .= cos.(-angle(p,p3,p2)) by SIN_COS:33 .= cos.(-angle(p,p3,p2)+2*PI*1) by SIN_COS6:10 .= cos(2*PI-angle(p,p3,p2)) by SIN_COS:def 23; p,p3,p2 are_mutually_different by A2,A1,A11,A51,ZFMISC_1:def 5; then angle(p3,p2,p) > PI by A97,Th24; then A100: angle(p3,p2,p1) > PI by A11,A1,Th10; p3,p2,p1 are_mutually_different by A51,A11,A39,ZFMISC_1:def 5; then angle(p2,p1,p3) > PI by A100,Th24; then A101: angle(p4,p1,p3) > PI by A88,Th9,A80,SPPOL_1:22; p4,p1,p3 are_mutually_different by A39,A88,A91,ZFMISC_1:def 5; then angle(p1,p3,p4) > PI by A101,Th24; then -angle(p1,p3,p4)<-PI by XREAL_1:26; then A102: -angle(p1,p3,p4)+2*PI < -PI+2*PI by XREAL_1:8; angle(p,p3,p2) < 2*PI & angle(p1,p3,p4) < 2*PI by COMPLEX2:84; then -angle(p,p3,p2) > -2*PI & -angle(p1,p3,p4) > -2*PI by XREAL_1:26; then A103: -angle(p,p3,p2)+2*PI > -2*PI+2*PI & -angle(p1,p3,p4)+2*PI > -2*PI+2*PI by XREAL_1:8; then 2*PI - angle(p1,p3,p4) = arccos cos(2*PI-angle(p1,p3,p4)) by A102,SIN_COS6:94 .= 2*PI - angle(p,p3,p2) by A98,A103,A99,SIN_COS6:94; hence thesis; end; end; end; theorem p1 in inside_of_circle(a,b,r) & p2 in outside_of_circle(a,b,r) implies ex p st p in LSeg(p1,p2) /\ circle(a,b,r) by Lm17; theorem Th30: p1 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p1,p4) & p3<>p4 implies p=p1 proof assume A1: p1 in circle(a,b,r); assume A2: p3 in circle(a,b,r); assume A3: p4 in circle(a,b,r); assume A4: p in LSeg(p1,p3); assume A5: p in LSeg(p1,p4); assume A6: p3<>p4; per cases; suppose A7: p1=p3 or p1=p4; per cases by A7; suppose p1=p3; then p in {p1} by A4,TOPREAL1:7; hence thesis by TARSKI:def 1; end; suppose p1=p4; then p in {p1} by A5,TOPREAL1:7; hence thesis by TARSKI:def 1; end; end; suppose A8: p1<>p3 & p1<>p4; per cases; suppose A9: p<>p1; A10: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; per cases by A9,Th12,A4,A5,A6; suppose A11: p3 in LSeg(p1,p4); A12: LSeg(p1,p4) \ {p1,p4} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60; not p3 in {p1,p4} by A8,A6,TARSKI:def 2; then p3 in LSeg(p1,p4) \ {p1,p4} by A11,XBOOLE_0:def 4; then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A12,A2,XBOOLE_0:def 3; hence thesis by A10,XBOOLE_0:def 7; end; suppose A13: p4 in LSeg(p1,p3); A14: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A2,TOPREAL9:60; not p4 in {p1,p3} by A8,A6,TARSKI:def 2; then p4 in LSeg(p1,p3) \ {p1,p3} by A13,XBOOLE_0:def 4; then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A14,A3,XBOOLE_0:def 3; hence thesis by A10,XBOOLE_0:def 7; end; end; suppose p=p1; hence thesis; end; end; end; theorem Th31: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p in circle(a,b,r) & pc = |[a,b]| & pc in LSeg(p,p2) & p1<>p implies 2*angle(p1,p,p2) = angle(p1,pc,p2) or 2*(angle(p1,p,p2) - PI) = angle(p1,pc,p2) proof assume A1: p1 in circle(a,b,r); assume A2: p2 in circle(a,b,r); assume A3: p in circle(a,b,r); assume A4: pc = |[a,b]| & pc in LSeg(p,p2); assume A5: p1<>p; per cases; suppose r=0; then |.p1-pc.|=0 & |.p2-pc.|=0 & |.p-pc.|=0 by A1,A2,A3,A4,TOPREAL9:43; then A6: p1=pc & p2=pc & p=pc by Lm1; then 2*angle(p1,p,p2) = 2*0 by COMPLEX2:93 .= angle(pc,pc,pc) by COMPLEX2:93; hence thesis by A6; end; suppose A7: r<>0; A8: |.p1-pc.|=r & |.p2-pc.|=r & |.p-pc.|=r by A1,A2,A3,A4,TOPREAL9:43; then A9: pc<>p & pc<>p1 & pc<>p2 by A7,Lm1; then A10: euc2cpx(pc)<> euc2cpx(p) & euc2cpx(pc)<> euc2cpx(p1) & euc2cpx(pc)<> euc2cpx(p2) by EUCLID_3:6; euc2cpx(p1)<> euc2cpx(p) by A5,EUCLID_3:6; then A11: angle(pc,p1,p)+angle(p1,p,pc)+angle(p,pc,p1)=PI or angle(pc,p1,p)+angle(p1,p,pc)+angle(p,pc,p1)=5*PI by A10,COMPLEX2:102; |.pc-p1.|=|.p-pc.| by A8,Lm2; then A12: angle(pc,p1,p)=angle(p1,p,pc) by A5,Th16; A13: angle(p1,p,p2)=angle(p1,p,pc) by A9,A4,Th10; per cases by A9,A4,Th13,A11,A12,A13; suppose angle(p,pc,p1)+angle(p1,pc,p2)=PI & 2*angle(p1,p,p2)+angle(p,pc,p1)=PI; hence thesis; end; suppose A14: angle(p,pc,p1)+angle(p1,pc,p2)=3*PI & 2*angle(p1,p,p2)+angle(p,pc,p1)=PI; A15: angle(p1,pc,p2)<2*PI & angle(p1,p,p2)>=0 by COMPLEX2:84; then angle(p1,p,p2)*(-2) <= (0 qua Real)*(-2) by XREAL_1:67; then -2*angle(p1,p,p2)+angle(p1,pc,p2)<0+2*PI by A15,XREAL_1:10; hence thesis by A14; end; suppose A16: angle(p,pc,p1)+angle(p1,pc,p2)=PI & 2*angle(p1,p,p2)+angle(p,pc,p1)=5*PI; A17: angle(p1,p,p2) < 2*PI & angle(p1,pc,p2)>=0 by COMPLEX2:84; then A18: -angle(p1,pc,p2) <= -0 by XREAL_1:26; angle(p1,p,p2)*2 < (2*PI)*2 by A17,XREAL_1:70; then 2*angle(p1,p,p2)+(-angle(p1,pc,p2))<(2*PI)*2+0 by A18,XREAL_1:10; hence thesis by A16; end; suppose angle(p,pc,p1)+angle(p1,pc,p2)=3*PI & 2*angle(p1,p,p2)+angle(p,pc,p1)=5*PI; hence thesis; end; end; end; :: opposite point on circle theorem Th32: p1 in circle(a,b,r) & r>0 implies ex p2 st p1<>p2 & p2 in circle(a,b,r) & |[a,b]| in LSeg(p1,p2) proof set pc = |[a,b]|; set p2 = 2*pc - p1; assume A1: p1 in circle(a,b,r); then A2: |. p1 - pc .| = r by TOPREAL9:43; assume A3: r>0; take p2; thus p1<>p2 proof assume p1=p2; then 1*p1 + p1 = 2*pc -p1 + p1 by EUCLID:33; then 1*p1 + 1*p1 = 2*pc -p1 + p1 by EUCLID:33; then (1+1)*p1 = 2*pc -p1 +p1 by EUCLID:37; then 2*p1 = 2*pc -(p1-p1) by EUCLID:51; then 2*p1 = 2*pc -0.REAL 2 by EUCLID:46; then 2*p1 = 2*pc + 0.REAL 2 by EUCLID:32; then 2*p1 = 2*pc by EUCLID:31; then p1 = pc by EUCLID:38; then |. pc - pc .| = r by A1,TOPREAL9:43; hence contradiction by A3,Lm1; end; |. p2 - pc .| = |. 2*pc +(-pc) +(-p1) .| by EUCLID:30 .= |. (2+(-1))*pc +(-p1) .| by EUCLID:37 .= |. pc - p1 .| by EUCLID:33 .= r by A2,Lm2; hence p2 in circle(a,b,r) by TOPREAL9:43; (1-1/2)*p1+(1/2)*p2 = (1/2)*(p1+p2) by EUCLID:36 .= (1/2)*(p1+(-p1)+2*pc) by EUCLID:30 .= (1/2)*(0.REAL 2+2*pc) by EUCLID:40 .= (1/2)*(2*pc) by EUCLID:31 .= ((1/2)*2)*pc by EUCLID:34 .= pc by EUCLID:33; hence |[a,b]| in LSeg(p1,p2) by SPPOL_1:22; end; :: The centre angle and the inscribed angle theorem Th33: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p in circle(a,b,r) & pc = |[a,b]| & p1<>p & p2<>p implies 2*angle(p1,p,p2) = angle(p1,pc,p2) or 2*(angle(p1,p,p2) - PI) = angle(p1,pc,p2) proof assume A1: p1 in circle(a,b,r); assume A2: p2 in circle(a,b,r); assume A3: p in circle(a,b,r); assume A4: pc = |[a,b]|; assume A5: p1<>p & p2<>p; per cases; suppose r=0; then |.p1-pc.|=0 & |.p2-pc.|=0 & |.p-pc.|=0 by A1,A2,A3,A4,TOPREAL9:43; then A6: p1=pc & p2=pc & p=pc by Lm1; then 2*angle(p1,p,p2) = 2*0 by COMPLEX2:93 .= angle(pc,pc,pc) by COMPLEX2:93; hence thesis by A6; end; suppose A7: r<>0; A8: |.p1-pc.|=r & |.p2-pc.|=r & |.p-pc.|=r by A1,A2,A3,A4,TOPREAL9:43; |.p1 - pc.| >= 0; then r > 0 by A7,A1,A4,TOPREAL9:43; then consider p3 such that A9: p<>p3 & p3 in circle(a,b,r) & |[a,b]| in LSeg(p,p3) by A3,Th32; per cases; suppose p2=p3; hence thesis by Th31,A1,A9,A3,A4,A5; end; suppose A10: p2<>p3; A11: angle(p2,pc,p3)<>0 proof set z2=euc2cpx(p2-pc); set z3=euc2cpx(p3-pc); assume angle(p2,pc,p3)=0; then A12: Arg(p2-pc)=Arg(p3-pc) by EUCLID_3:45; A13: |.p2-pc.|=|.p3-pc.| by A8,A9,A4,TOPREAL9:43; A14: |.z2.| = |.p2-pc.| by EUCLID_3:31 .= |.z3.| by A13,EUCLID_3:31; A15: z2 = [* |.z2.|*cos Arg z2,|.z2.|*sin Arg z2 *] by COMPLEX2:19 .= z3 by A12,A14,COMPLEX2:19; p2 = p2 + 0.REAL 2 by EUCLID:31 .= p2 +(pc+(-pc)) by EUCLID:40 .= p2 +(-pc) + pc by EUCLID:30 .= p3-pc + pc by A15,EUCLID_3:6 .= p3 +(pc+(-pc)) by EUCLID:30 .= p3 + 0.REAL 2 by EUCLID:40 .= p3 by EUCLID:31; hence contradiction by A10; end; A16: 2*angle(p2,p,p3) = angle(p2,pc,p3) or 2*(angle(p2,p,p3) - PI) = angle(p2,pc,p3) by Th31,A2,A9,A3,A4,A5; A17: angle(p2,p,p3)<>0 proof A18: -2*PI < -0; assume angle(p2,p,p3)=0; hence contradiction by A11,A18,COMPLEX2:84,A16; end; then A19: angle(p3,p,p2) = 2*PI-angle(p2,p,p3) by EUCLID_3:46; A20: 2*angle(p2,p,p3) = angle(p2,pc,p3) implies 2*(angle(p3,p,p2) -PI) = angle(p3,pc,p2) proof assume 2*angle(p2,p,p3) = angle(p2,pc,p3); hence 2*(angle(p3,p,p2)-PI) = 2*PI - angle(p2,pc,p3) by A19 .= angle(p3,pc,p2) by A11,EUCLID_3:46; end; A21: 2*(angle(p2,p,p3) - PI) = angle(p2,pc,p3) implies 2*angle(p3,p,p2) = angle(p3,pc,p2) proof assume A22: 2*(angle(p2,p,p3) - PI) = angle(p2,pc,p3); thus 2*angle(p3,p,p2) = 2*(2*PI-angle(p2,p,p3)) by A17,EUCLID_3:46 .= 2*PI -2*(angle(p2,p,p3)-PI) .= angle(p3,pc,p2) by A22,A11,EUCLID_3:46; end; A23: angle(p1,p,p2) = angle(p1,p,p3)+angle(p3,p,p2) or angle(p1,p,p2)+2*PI = angle(p1,p,p3)+angle(p3,p,p2) by Th4; per cases by Th4; suppose A24: angle(p1,pc,p2) = angle(p1,pc,p3)+angle(p3,pc,p2); per cases by Th31,A2,A9,A3,A4,A5,A20,A21,A1; suppose 2*angle(p1,p,p3) = angle(p1,pc,p3) & 2*(angle(p3,p,p2)-PI) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*angle(p1,p,p2) - 2*PI or angle(p1,pc,p2) = 2*angle(p1,p,p2)+2*PI by A24,A23; hence thesis by Lm3; end; suppose 2*angle(p1,p,p3) = angle(p1,pc,p3) & 2*angle(p3,p,p2) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*angle(p1,p,p2) or angle(p1,pc,p2) = 2*angle(p1,p,p2)+4*PI by A24,A23; hence thesis by Lm4; end; suppose 2*(angle(p1,p,p3) - PI) = angle(p1,pc,p3) & 2*(angle(p3,p,p2)-PI) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*(angle(p1,p,p3)+angle(p3,p,p2))-4*PI by A24; hence thesis by Lm5,A23; end; suppose 2*(angle(p1,p,p3) - PI) = angle(p1,pc,p3) & 2*angle(p3,p,p2) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*angle(p1,p,p2)-2*PI or angle(p1,pc,p2) = 2*angle(p1,p,p2)+2*PI by A24,A23; hence thesis by Lm3; end; end; suppose A25: angle(p1,pc,p2)+2*PI = angle(p1,pc,p3)+angle(p3,pc,p2); per cases by Th31,A2,A9,A3,A4,A5,A20,A21,A1; suppose 2*angle(p1,p,p3) = angle(p1,pc,p3) & 2*(angle(p3,p,p2)-PI) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*(angle(p1,p,p3)+angle(p3,p,p2))-4*PI by A25; hence thesis by Lm5,A23; end; suppose 2*angle(p1,p,p3) = angle(p1,pc,p3) & 2*angle(p3,p,p2) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*angle(p1,p,p2)-2*PI or angle(p1,pc,p2) = 2*angle(p1,p,p2)+2*PI by A25,A23; hence thesis by Lm3; end; suppose 2*(angle(p1,p,p3) - PI) = angle(p1,pc,p3) & 2*(angle(p3,p,p2)-PI) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*(angle(p1,p,p3)+angle(p3,p,p2))-6*PI by A25; hence thesis by Lm6,A23; end; suppose 2*(angle(p1,p,p3) - PI) = angle(p1,pc,p3) & 2*angle(p3,p,p2) = angle(p3,pc,p2); then angle(p1,pc,p2) = 2*(angle(p1,p,p3)+angle(p3,p,p2))-4*PI by A25; hence thesis by Lm5,A23; end; end; end; end; end; :: Angles subtended by the same chord theorem Th34: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r) & p1<>p3 & p1<>p4 & p2<>p3 & p2<>p4 implies angle(p1,p3,p2) = angle(p1,p4,p2) or angle(p1,p3,p2) = angle(p1,p4,p2) - PI or angle(p1,p3,p2) = angle(p1,p4,p2) + PI proof assume A1: p1 in circle(a,b,r); assume A2: p2 in circle(a,b,r); assume A3: p3 in circle(a,b,r); assume A4: p4 in circle(a,b,r); assume A5: p1<>p3 & p1<>p4 & p2<>p3 & p2<>p4; set pc=|[a,b]|; per cases by A5,A1,A2,A3,Th33; suppose 2*angle(p1,p3,p2) = angle(p1,pc,p2); then 2*angle(p1,p4,p2) = 2*angle(p1,p3,p2) or 2*(angle(p1,p4,p2) - PI) = 2*angle(p1,p3,p2) by A5,A1,A2,A4,Th33; hence thesis; end; suppose 2*(angle(p1,p3,p2) - PI) = angle(p1,pc,p2); then 2*angle(p1,p4,p2) = 2*(angle(p1,p3,p2) - PI) or 2*(angle(p1,p4,p2) - PI) = 2*(angle(p1,p3,p2) - PI) by A5,A1,A2,A4,Th33; hence thesis; end; end; theorem Th35: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p1<>p2 & p2<>p3 implies angle(p1,p2,p3)<>PI proof assume A1: p1 in circle(a,b,r); assume A2: p2 in circle(a,b,r); assume A3: p3 in circle(a,b,r); assume p1<>p2 & p2<>p3; then A4: not p2 in {p1,p3} by TARSKI:def 2; set pc = |[a,b]|; assume angle(p1,p2,p3)=PI; then p2 in LSeg(p1,p3) by Th11; then A5: p2 in LSeg(p1,p3) \ {p1,p3} by A4,XBOOLE_0:def 4; A6: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60; inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; then inside_of_circle(a,b,r) /\ circle(a,b,r) = {} by XBOOLE_0:def 7; hence contradiction by A2,A6,A5,XBOOLE_0:def 3; end; Lm22: p1 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p1,p4) implies |.p1-p.|*|.p-p3.| = |.p1-p.|*|.p-p4.| proof assume A1: p1 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r); assume A2: p in LSeg(p1,p3) & p in LSeg(p1,p4); per cases; suppose p3<>p4; then p=p1 by Th30,A2,A1; then |.p1-p.| = |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID_2:61; hence |.p1-p.|*|.p-p3.| = |.p1-p.|*|.p-p4.|; end; suppose p3=p4; hence thesis; end; end; Lm23: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p4 in circle(a,b,r) & p in LSeg(p1,p1) & p in LSeg(p2,p4) implies |.p1-p.|*|.p-p1.| = |.p2-p.|*|.p-p4.| proof assume A1: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p4 in circle(a,b,r); assume p in LSeg(p1,p1); then A2: p in {p1} by TOPREAL1:7; then A3: |.p1-p.| = |.p-p.| by TARSKI:def 1 .= |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID:10; assume p in LSeg(p2,p4); then A4: p1 in LSeg(p2,p4) by A2,TARSKI:def 1; A5: LSeg(p2,p4) \ {p2,p4} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A6: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; per cases; suppose p1<>p2 & p1<>p4; then not p1 in {p2,p4} by TARSKI:def 2; then p1 in LSeg(p2,p4) \ {p2,p4} by A4,XBOOLE_0:def 4; then p1 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A5,A1,XBOOLE_0:def 3; hence thesis by A6,XBOOLE_0:def 7; end; suppose A7: not(p1<>p2 & p1<>p4); per cases by A7; suppose p1=p2; then |.p2-p.|=|.p1-p1.| by A2,TARSKI:def 1 .= |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID:10; hence thesis by A3; end; suppose p1=p4; then |.p-p4.|=|.p1-p1.| by A2,TARSKI:def 1 .= |.0.REAL 2.| by EUCLID:46 .= 0 by EUCLID:10; hence thesis by A3; end; end; end; theorem Th36: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) & p1,p2,p3,p4 are_mutually_different implies angle(p1,p4,p2) = angle(p1,p3,p2) proof assume A1: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r); assume A2: p in LSeg(p1,p3) & p in LSeg(p2,p4); assume p1,p2,p3,p4 are_mutually_different; then A3: p1<>p2 & p1<>p3 & p1<>p4 & p2<>p3 & p2<>p4 & p3<>p4 by ZFMISC_1:def 6; A4: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; A5: LSeg(p2,p4) \ {p2,p4} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A6: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A7: p<>p1 & p<>p4 proof assume A8: p=p1 or p=p4; per cases by A8; suppose A9: p=p1; not p1 in {p2,p4} by A3,TARSKI:def 2; then p1 in LSeg(p2,p4) \ {p2,p4} by A2,A9,XBOOLE_0:def 4; then p1 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A5,A1,XBOOLE_0: def 3; hence contradiction by A4,XBOOLE_0:def 7; end; suppose A10: p=p4; not p4 in {p1,p3} by A3,TARSKI:def 2; then p4 in LSeg(p1,p3) \ {p1,p3} by A2,A10,XBOOLE_0:def 4; then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A6,A1,XBOOLE_0: def 3; hence contradiction by A4,XBOOLE_0:def 7; end; end; A11: p<>p2 & p<>p3 proof assume A12: p=p2 or p=p3; per cases by A12; suppose A13: p=p3; not p3 in {p2,p4} by A3,TARSKI:def 2; then p3 in LSeg(p2,p4) \ {p2,p4} by A2,A13,XBOOLE_0:def 4; then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A5,A1,XBOOLE_0: def 3; hence contradiction by A4,XBOOLE_0:def 7; end; suppose A14: p=p2; not p2 in {p1,p3} by A3,TARSKI:def 2; then p2 in LSeg(p1,p3) \ {p1,p3} by A2,A14,XBOOLE_0:def 4; then p2 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A6,A1,XBOOLE_0: def 3; hence contradiction by A4,XBOOLE_0:def 7; end; end; A15: angle(p1,p4,p) = angle(p1,p4,p2) by A2,A7,Th10; A16: angle(p,p3,p2) = angle(p1,p3,p2) by A2,A11,Th9; A17: angle(p4,p,p1) = angle(p2,p,p3) by A7,A11,A2,Th15; A18: p1,p4,p are_mutually_different by A7,A3,ZFMISC_1:def 5; A19: p2,p,p3 are_mutually_different by A11,A3,ZFMISC_1:def 5; A20: p,p3,p2 are_mutually_different by A11,A3,ZFMISC_1:def 5; A21: p4,p,p1 are_mutually_different by A7,A3,ZFMISC_1:def 5; per cases by A3,A1,Th34; suppose angle(p1,p4,p2) = angle(p1,p3,p2); hence thesis; end; suppose A22: angle(p1,p4,p2) = angle(p1,p3,p2) - PI; angle(p1,p3,p2)<2*PI by COMPLEX2:84; then angle(p1,p3,p2) - PI < 2*PI -PI by XREAL_1:11; then angle(p2,p,p3) <= PI by A15,A22,A17,A18,Th23; then A23: angle(p1,p3,p2) <= PI by A16,A19,Th23; angle(p1,p4,p2) >= 0 by COMPLEX2:84; then angle(p1,p3,p2) - PI + PI >= 0 + PI by A22,XREAL_1:8; then A24: p3 in LSeg(p1,p2) by Th11,A23,XXREAL_0:1; A25: LSeg(p1,p2) \ {p1,p2} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A26: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; not p3 in {p1,p2} by A3,TARSKI:def 2; then p3 in LSeg(p1,p2) \ {p1,p2} by A24,XBOOLE_0:def 4; then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A1,A25,XBOOLE_0:def 3; hence thesis by A26,XBOOLE_0:def 7; end; suppose A27: angle(p1,p4,p2) = angle(p1,p3,p2) + PI; angle(p1,p4,p2) < 2*PI by COMPLEX2:84; then angle(p1,p4,p2) - PI < 2*PI -PI by XREAL_1:11; then angle(p4,p,p1) <= PI by A16,A27,A17,A20,Th23; then A28: angle(p1,p4,p2) <= PI by A15,A21,Th23; angle(p1,p3,p2) >= 0 by COMPLEX2:84; then angle(p1,p4,p2) - PI + PI >= 0 + PI by A27,XREAL_1:8; then A29: p4 in LSeg(p1,p2) by Th11,A28,XXREAL_0:1; A30: LSeg(p1,p2) \ {p1,p2} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A31: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; not p4 in {p1,p2} by A3,TARSKI:def 2; then p4 in LSeg(p1,p2) \ {p1,p2} by A29,XBOOLE_0:def 4; then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A1,A30,XBOOLE_0:def 3; hence thesis by A31,XBOOLE_0:def 7; end; end; theorem Th37: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & angle(p1,p2,p3) = 0 & p1<>p2 & p2<>p3 implies p1=p3 proof assume A1: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r); assume A2: angle(p1,p2,p3) = 0; assume A3: p1<>p2 & p2<>p3; assume A4: p1<>p3; then euc2cpx(p1)<> euc2cpx(p2) & euc2cpx(p1)<> euc2cpx(p3) & euc2cpx(p2)<> euc2cpx(p3) by A3,EUCLID_3:6; then (angle(p2,p3,p1) = 0 & angle(p3,p1,p2) = PI) or (angle(p2,p3,p1) = PI & angle(p3,p1,p2) = 0) by A2,COMPLEX2:101; hence contradiction by Th35,A1,A3,A4; end; :: Intersecting Chords Theorem or :: Product of Segments of Chords theorem p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies |.p1-p.|*|.p-p3.| = |.p2-p.|*|.p-p4.| proof assume A1: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r); assume A2: p in LSeg(p1,p3) & p in LSeg(p2,p4); A3: |.p1-p.| = |.p-p1.| by Lm2; A4: |.p2-p.| = |.p-p2.| by Lm2; A5: |.p3-p.| = |.p-p3.| by Lm2; A6: |.p4-p.| = |.p-p4.| by Lm2; per cases; suppose A7: not p1,p2,p3,p4 are_mutually_different; per cases by A7,ZFMISC_1:def 6; suppose p1=p2; hence thesis by A1,A2,Lm22; end; suppose p1=p3; hence thesis by A1,A2,Lm23; end; suppose p1=p4; hence thesis by A1,A2,Lm22,A4,A6; end; suppose p2=p3; hence thesis by A1,A2,Lm22,A3,A5; end; suppose p2=p4; hence thesis by A1,A2,Lm23; end; suppose p3=p4; hence thesis by A1,A2,Lm22,A3,A4,A6; end; end; suppose A8: p1,p2,p3,p4 are_mutually_different; then A9: p1<>p2 & p1<>p3 & p1<>p4 & p2<>p3 & p2<>p4 & p3<>p4 by ZFMISC_1: def 6; A10: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; A11: LSeg(p2,p4) \ {p2,p4} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A12: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; A13: p<>p1 & p<>p4 proof assume A14: p=p1 or p=p4; per cases by A14; suppose A15: p=p1; not p1 in {p2,p4} by A9,TARSKI:def 2; then p1 in LSeg(p2,p4) \ {p2,p4} by A2,A15,XBOOLE_0:def 4; then p1 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A11,A1,XBOOLE_0:def 3; hence contradiction by A10,XBOOLE_0:def 7; end; suppose A16: p=p4; not p4 in {p1,p3} by A9,TARSKI:def 2; then p4 in LSeg(p1,p3) \ {p1,p3} by A2,A16,XBOOLE_0:def 4; then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A12,A1,XBOOLE_0:def 3; hence contradiction by A10,XBOOLE_0:def 7; end; end; A17: p<>p2 & p<>p3 proof assume A18: p=p2 or p=p3; per cases by A18; suppose A19: p=p3; not p3 in {p2,p4} by A9,TARSKI:def 2; then p3 in LSeg(p2,p4) \ {p2,p4} by A2,A19,XBOOLE_0:def 4; then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A11,A1,XBOOLE_0:def 3; hence contradiction by A10,XBOOLE_0:def 7; end; suppose A20: p=p2; not p2 in {p1,p3} by A9,TARSKI:def 2; then p2 in LSeg(p1,p3) \ {p1,p3} by A2,A20,XBOOLE_0:def 4; then p2 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A12,A1,XBOOLE_0:def 3; hence contradiction by A10,XBOOLE_0:def 7; end; end; A21: angle(p1,p4,p) = angle(p1,p4,p2) by A2,A13,Th10; A22: angle(p,p3,p2) = angle(p1,p3,p2) by A2,A17,Th9; A23: angle(p4,p,p1) = angle(p2,p,p3) by A13,A17,A2,Th15; A24: angle(p1,p4,p2) = angle(p1,p3,p2) by A1,A2,A8,Th36; A25: p4,p,p1 are_mutually_different by A13,A9,ZFMISC_1:def 5; A26: angle(p4,p,p1)<>PI proof assume angle(p4,p,p1)=PI; then p in LSeg(p1,p4) by Th11; hence contradiction by A13,A1,A2,A9,Th30; end; A27: angle(p,p1,p4)<>PI proof assume angle(p,p1,p4)=PI; then angle(p3,p1,p4)=PI by A2,A13,Th9; hence contradiction by A1,A9,Th35; end; angle(p1,p4,p)<>PI proof assume angle(p1,p4,p)=PI; then angle(p1,p4,p2)=PI by A2,A13,Th10; hence contradiction by A1,A9,Th35; end; then A28: p4,p,p1 is_a_triangle by A25,A26,A27,Th20; A29: p2,p,p3 are_mutually_different by A17,A9,ZFMISC_1:def 5; A30: angle(p2,p,p3)<>PI by A26,A13,A17,A2,Th15; A31: angle(p,p3,p2)<>PI proof assume angle(p,p3,p2)=PI; then angle(p1,p3,p2)=PI by A2,A17,Th9; hence contradiction by A1,A9,Th35; end; angle(p3,p2,p)<>PI proof assume angle(p3,p2,p)=PI; then angle(p3,p2,p4)=PI by A2,A17,Th10; hence contradiction by A1,A9,Th35; end; then p2,p,p3 is_a_triangle by A29,A30,A31,Th20; hence thesis by A24,A21,A22,A28,A23,A3,A4,A5,A6,Th22; end; end; begin :: Heron's Formula and Ptolemy's Theorem :: Heron's formula theorem a = |.p2-p1.| & b = |.p3-p2.| & c = |.p1-p3.| & s = (1/2)*the_perimeter_of_polygon3(p1,p2,p3) implies abs(the_area_of_polygon3(p1,p2,p3)) = sqrt(s*(s-a)*(s-b)*(s-c)) proof assume A1: a = |.p2-p1.| & b = |.p3-p2.| & c = |.p1-p3.|; assume A2: s = the_perimeter_of_polygon3(p1,p2,p3)/2; A3: a = |.p1-p2.| by A1,Lm2; A4: c = |.p3-p1.| by A1,Lm2; A5: (sin angle(p3,p2,p1))^2+(cos angle(p3,p2,p1))^2=1 by SIN_COS:32; A6: c^2 = a^2 + b^2 - 2*a*b* cos angle(p1,p2,p3) by A1,A3,A4,Th7; the_area_of_polygon3(p1,p2,p3)^2 = (a*b*sin angle(p3,p2,p1)/2)^2 by A1,A3,Th5 .= (a*b*sin angle(p3,p2,p1))^2*(1/2)^2 .= (a*b)^2*(1-(cos angle(p3,p2,p1))^2)*(1/2)^2 by A5,SQUARE_1:68 .= (((a*b)^2-(a*b)^2*(cos angle(p3,p2,p1))^2))*2^2/2^2*(1/2)^2 by XCMPLX_1:90 .= (2^2*(a*b)^2-(2*a*b*cos angle(p3,p2,p1))^2)/2^2*(1/2)^2 .= (2^2*(a*b)^2-(-c^2+a^2+b^2)^2)/2^2*(1/2)^2 by Th3,A6 .= 16*(s-a)*(s-b)*((s-c)*s)/(2*2)*(1/2)^2 by A1,A2 .= s*(s-a)*(s-b)*(s-c); hence thesis by COMPLEX1:158; end; :: Ptolemy's Theorem theorem p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies |.p3-p1.|*|.p4-p2.| = |.p2-p1.|*|.p4-p3.| + |.p3-p2.|*|.p4-p1.| proof assume A1: p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) & p4 in circle(a,b,r); assume A2: p in LSeg(p1,p3) & p in LSeg(p2,p4); A3: |.p3-p1.| = |.p1-p3.| by Lm2; per cases; suppose A4: not p1,p2,p3,p4 are_mutually_different; per cases by A4,ZFMISC_1:def 6; suppose A5: p1=p2; then |.p2-p1.| = 0 by Lm1; hence thesis by A5; end; suppose p1=p3; then A6: p in {p1} by A2,TOPREAL1:7; then p in circle(a,b,r) by A1,TARSKI:def 1; then p in LSeg(p2,p4) /\ circle(a,b,r) by A2,XBOOLE_0:def 3; then p in {p2,p4} by A1,TOPREAL9:61; then A7: p = p2 or p = p4 by TARSKI:def 2; per cases by A7,A6,TARSKI:def 1; suppose A8: p1 = p2; then |.p2-p1.| = 0 by Lm1; hence thesis by A8; end; suppose A9: p1 = p4; then |.p4-p1.| = 0 by Lm1; hence thesis by A9,Lm2,A3; end; end; suppose A10: p1=p4; then |.p4-p1.| = 0 by Lm1; hence thesis by A10,Lm2,A3; end; suppose A11: p2=p3; then |.p3-p2.| = 0 by Lm1; hence thesis by A11; end; suppose p2=p4; then A12: p in {p2} by A2,TOPREAL1:7; then p in circle(a,b,r) by A1,TARSKI:def 1; then p in LSeg(p1,p3) /\ circle(a,b,r) by A2,XBOOLE_0:def 3; then p in {p1,p3} by A1,TOPREAL9:61; then A13: p = p1 or p = p3 by TARSKI:def 2; per cases by A13,A12,TARSKI:def 1; suppose A14: p1 = p2; then |.p2-p1.| = 0 by Lm1; hence thesis by A14; end; suppose A15: p2 = p3; then |.p3-p2.| = 0 by Lm1; hence thesis by A15; end; end; suppose A16: p3=p4; then |.p4-p3.| = 0 by Lm1; hence thesis by A16; end; end; suppose A17: p1,p2,p3,p4 are_mutually_different; then A18: p1<>p2 & p1<>p3 & p1<>p4 & p2<>p3 & p2<>p4 & p3<>p4 by ZFMISC_1: def 6; A19: not p2 in LSeg(p1,p3) proof assume A20: p2 in LSeg(p1,p3); A21: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; A22: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; not p2 in {p1,p3} by A18,TARSKI:def 2; then p2 in LSeg(p1,p3) \ {p1,p3} by A20,XBOOLE_0:def 4; then p2 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A22,A1,XBOOLE_0: def 3; hence contradiction by A21,XBOOLE_0:def 7; end; then A23: angle(p,p2,p3) = angle(p4,p2,p3) by A2,Th9; consider p5 such that A24: p5 in LSeg(p1,p3) & angle(p1,p2,p5) = angle(p,p2,p3) by A19,A2,Th28; A25: angle(p4,p2,p3)<>PI & angle(p2,p3,p4)<>PI & angle(p3,p4,p2)<>PI by Th35,A1,A18; A26: euc2cpx(p2)<> euc2cpx(p3) & euc2cpx(p2)<> euc2cpx(p4) & euc2cpx(p3)<> euc2cpx(p4) by A18,EUCLID_3:6; A27: p5<>p1 proof assume p5=p1; then angle(p4,p2,p3) = angle(p1,p2,p1) by A24,A19,A2,Th9 .= 0 by COMPLEX2:93; hence contradiction by A25,A26,COMPLEX2:101; end; A28: p5<>p3 proof assume p5=p3; then A29: angle(p4,p2,p3) = angle(p1,p2,p3) by A24,A19,A2,Th9; angle(p4,p2,p3) + angle(p3,p2,p4) = angle(p4,p2,p4) or angle(p4,p2,p3) + angle(p3,p2,p4) = angle(p4,p2,p4) + 2*PI by Th4; then A30: angle(p4,p2,p3) + angle(p3,p2,p4) = 0 or angle(p4,p2,p3) + angle(p3,p2,p4) = 0 + 2*PI by COMPLEX2:93; per cases by A30,Th4; suppose (angle(p4,p2,p3) + angle(p3,p2,p4) = 0 & angle(p1,p2,p3) + angle(p3,p2,p4) = angle(p1,p2,p4)) or (angle(p4,p2,p3) + angle(p3,p2,p4) = 2*PI & angle(p1,p2,p3) + angle(p3,p2,p4) = angle(p1,p2,p4)+ 2*PI); hence contradiction by A29,A18,A1,Th37; end; suppose angle(p4,p2,p3) + angle(p3,p2,p4) = 2*PI & angle(p1,p2,p3) + angle(p3,p2,p4) = angle(p1,p2,p4); hence contradiction by A29,COMPLEX2:84; end; suppose angle(p4,p2,p3) + angle(p3,p2,p4) = 0 & angle(p1,p2,p3) + angle(p3,p2,p4) = angle(p1,p2,p4)+2*PI; then angle(p1,p2,p4) = -2*PI by A29; hence contradiction by COMPLEX2:84; end; end; A31: p5<>p2 proof assume A32: p5=p2; A33: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54; A34: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60; not p2 in {p1,p3} by A18,TARSKI:def 2; then p2 in LSeg(p1,p3) \ {p1,p3} by A32,A24,XBOOLE_0:def 4; then p2 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A34,A1,XBOOLE_0: def 3; hence contradiction by A33,XBOOLE_0:def 7; end; p2,p3,p4,p1 are_mutually_different by A18,ZFMISC_1:def 6; then A35: angle(p2,p1,p3) = angle(p2,p4,p3) by A1,A2,Th36; A36: angle(p3,p1,p2) = angle(p3,p4,p2) proof per cases; suppose A37: angle(p2,p1,p3)=0; then angle(p3,p1,p2)=0 by EUCLID_3:45; hence thesis by A35,A37,EUCLID_3:45; end; suppose A38: angle(p2,p1,p3)<>0; then angle(p3,p1,p2)=2*PI-angle(p2,p1,p3) by EUCLID_3:46; hence thesis by A35,A38,EUCLID_3:46; end; end; then A39: angle(p5,p1,p2) = angle(p3,p4,p2) by A24,A27,Th9; A40: angle(p1,p4,p2) = angle(p1,p3,p2) by A17,A1,A2,Th36; angle(p2,p4,p1) = angle(p2,p3,p1) proof per cases; suppose A41: angle(p1,p4,p2)=0; then angle(p2,p4,p1)=0 by EUCLID_3:45; hence thesis by A40,A41,EUCLID_3:45; end; suppose A42: angle(p1,p4,p2)<>0; then angle(p2,p4,p1)=2*PI-angle(p1,p4,p2) by EUCLID_3:46; hence thesis by A40,A42,EUCLID_3:46; end; end; then A43: angle(p2,p4,p1) = angle(p2,p3,p5) by A24,A28,Th10; A44: angle(p5,p2,p3) = angle(p1,p2,p4) proof per cases by Th4,A24,A23; suppose (angle(p5,p2,p3) = angle(p5,p2,p4) + angle(p4,p2,p3) & angle(p1,p2,p4) = angle(p4,p2,p3) + angle(p5,p2,p4)) or (angle(p5,p2,p3)+2*PI = angle(p5,p2,p4) + angle(p4,p2,p3) & angle(p1,p2,p4)+2*PI = angle(p4,p2,p3) + angle(p5,p2,p4)); hence thesis; end; suppose A45: angle(p5,p2,p3)+2*PI = angle(p5,p2,p4) + angle(p4,p2,p3) & angle(p1,p2,p4) = angle(p4,p2,p3) + angle(p5,p2,p4); angle(p5,p2,p3)>=0 & angle(p1,p2,p4)<2*PI by COMPLEX2:84; then angle(p5,p2,p3)+2*PI>=0+2*PI by XREAL_1:8; hence thesis by A45,COMPLEX2:84; end; suppose A46: angle(p5,p2,p3) = angle(p5,p2,p4) + angle(p4,p2,p3) & angle(p1,p2,p4)+2*PI = angle(p4,p2,p3) + angle(p5,p2,p4); angle(p5,p2,p3)<2*PI & angle(p1,p2,p4)>=0 by COMPLEX2:84; then angle(p1,p2,p4)+2*PI>=0+2*PI by XREAL_1:8; hence thesis by A46,COMPLEX2:84; end; end; angle(p2,p3,p4) = angle(p2,p5,p1) proof A47: euc2cpx(p2)<> euc2cpx(p5) & euc2cpx(p2)<> euc2cpx(p1) & euc2cpx(p5)<> euc2cpx(p1) by A18,A27,A31,EUCLID_3:6; per cases by A26,A47,COMPLEX2:102; suppose (angle(p2,p3,p4)+angle(p3,p4,p2)+angle(p4,p2,p3) = PI & angle(p2,p5,p1)+angle(p5,p1,p2)+angle(p1,p2,p5) = PI) or (angle(p2,p3,p4)+angle(p3,p4,p2)+angle(p4,p2,p3) = 5*PI & angle(p2,p5,p1)+angle(p5,p1,p2)+angle(p1,p2,p5) = 5*PI); hence thesis by A39,A24,A23; end; suppose angle(p2,p3,p4)+angle(p3,p4,p2)+angle(p4,p2,p3) = 5*PI & angle(p2,p5,p1)+angle(p5,p1,p2)+angle(p1,p2,p5) = PI; then A48: angle(p2,p3,p4)-angle(p2,p5,p1) = 4*PI by A39,A24,A23; angle(p2,p3,p4)<2*PI & angle(p2,p5,p1)>=0 by COMPLEX2:84; then angle(p2,p3,p4)-angle(p2,p5,p1) < 2*PI-0 by XREAL_1:16; hence thesis by A48,XREAL_1:66; end; suppose angle(p2,p3,p4)+angle(p3,p4,p2)+angle(p4,p2,p3) = PI & angle(p2,p5,p1)+angle(p5,p1,p2)+angle(p1,p2,p5) = 5*PI; then A49: angle(p2,p5,p1)-angle(p2,p3,p4) = 4*PI by A39,A24,A23; angle(p2,p5,p1)<2*PI & angle(p2,p3,p4)>=0 by COMPLEX2:84; then angle(p2,p5,p1)-angle(p2,p3,p4) < 2*PI-0 by XREAL_1:16; hence thesis by A49,XREAL_1:66; end; end; then A50: angle(p1,p2,p5)<>PI & angle(p2,p5,p1)<>PI & angle(p5,p1,p2)<>PI by A24,A25,A36,A19,A2,Th9,A27; p1,p2,p5 are_mutually_different & p4,p2,p3 are_mutually_different by A18,A27,A31,ZFMISC_1:def 5; then A51: p1,p2,p5 is_a_triangle & p4,p2,p3 is_a_triangle by A50,A25,Th20; A52: angle(p4,p1,p2) = angle(p3,p5,p2) proof A53: euc2cpx(p2)<> euc2cpx(p4) & euc2cpx(p2)<> euc2cpx(p1) & euc2cpx(p4)<> euc2cpx(p1) by A18,EUCLID_3:6; A54: euc2cpx(p2)<> euc2cpx(p3) & euc2cpx(p2)<> euc2cpx(p5) & euc2cpx(p3)<> euc2cpx(p5) by A18,A28,A31,EUCLID_3:6; per cases by A53,A54,COMPLEX2:102; suppose (angle(p2,p4,p1)+angle(p4,p1,p2)+angle(p1,p2,p4) = PI & angle(p2,p3,p5)+angle(p3,p5,p2)+angle(p5,p2,p3) = PI) or (angle(p2,p4,p1)+angle(p4,p1,p2)+angle(p1,p2,p4) = 5*PI & angle(p2,p3,p5)+angle(p3,p5,p2)+angle(p5,p2,p3) = 5*PI); hence thesis by A43,A44; end; suppose angle(p2,p4,p1)+angle(p4,p1,p2)+angle(p1,p2,p4) = 5*PI & angle(p2,p3,p5)+angle(p3,p5,p2)+angle(p5,p2,p3) = PI; then A55: angle(p4,p1,p2)-angle(p3,p5,p2) = 4*PI by A43,A44; angle(p4,p1,p2)<2*PI & angle(p3,p5,p2)>=0 by COMPLEX2:84; then angle(p4,p1,p2)-angle(p3,p5,p2) < 2*PI-0 by XREAL_1:16; hence thesis by A55,XREAL_1:66; end; suppose angle(p2,p4,p1)+angle(p4,p1,p2)+angle(p1,p2,p4) = PI & angle(p2,p3,p5)+angle(p3,p5,p2)+angle(p5,p2,p3) = 5*PI; then A56: angle(p3,p5,p2)-angle(p4,p1,p2) = 4*PI by A43,A44; angle(p3,p5,p2)<2*PI & angle(p4,p1,p2)>=0 by COMPLEX2:84; then angle(p3,p5,p2)-angle(p4,p1,p2) < 2*PI-0 by XREAL_1:16; hence thesis by A56,XREAL_1:66; end; end; A57: angle(p2,p4,p1)<>PI & angle(p4,p1,p2)<>PI & angle(p1,p2,p4)<>PI by Th35,A1,A18; p2,p3,p5 are_mutually_different & p2,p4,p1 are_mutually_different by A18,A28,A31,ZFMISC_1:def 5; then A58: p2,p3,p5 is_a_triangle & p2,p4,p1 is_a_triangle by A52,A43,A44, A57,Th20; |.p1-p5.|*|.p2-p4.| = |.p2-p1.|*|.p4-p3.| by A39,A24,A23,A51,Th21; then A59: |.p1-p5.|*|.p4-p2.| = |.p2-p1.|*|.p4-p3.| by Lm2; |.p5-p3.|*|.p4-p2.| = |.p3-p2.|*|.p1-p4.| by A43,A44,A58,Th21; then |.p5-p3.|*|.p4-p2.| = |.p3-p2.|*|.p4-p1.| by Lm2; then A60: |.p3-p5.|*|.p4-p2.| = |.p3-p2.|*|.p4-p1.| by Lm2; A61: |.p3-p1.| = sqrt |.p3-p1.|^2 by SQUARE_1:89 .= sqrt (|.p1-p5.|^2 + |.p3-p5.|^2 - 2*|.p1-p5.|*|.p3-p5.|*cos angle(p1,p5,p3)) by Th7 .= sqrt (|.p1-p5.|^2 + |.p3-p5.|^2 - 2*|.p1-p5.|*|.p3-p5.|*cos PI) by A24,A27,A28,Th8 .= sqrt (|.p1-p5.| + |.p3-p5.|)^2 by SIN_COS:82 .= |.p1-p5.| + |.p3-p5.| by SQUARE_1:89; thus |.p2-p1.|*|.p4-p3.| + |.p3-p2.|*|.p4-p1.| = |.p5-p1.|*|.p4-p2.| + |.p3-p5.|*|.p4-p2.| by A59,Lm2,A60 .= (|.p5-p1.| + |.p3-p5.|)*|.p4-p2.| .= |.p3-p1.|*|.p4-p2.| by A61,Lm2; end; end; begin :: Appendix reserve c1,c2,c3 for Element of COMPLEX; theorem (p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2 by Lm15; theorem |.p1-p2.| = 0 iff p1=p2 by Lm1; theorem |.p1-p2.| = |.p2-p1.| by Lm2; theorem not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+2*PI by Lm3; theorem not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+4*PI by Lm4; theorem not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-4*PI by Lm5; theorem not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-6*PI by Lm6; theorem c1=euc2cpx(p1-p2) & c2=euc2cpx(p3-p2) implies angle(p1,p2,p3) = angle(c1,c2) by Lm7; theorem angle(c1,c2) + angle(c2,c3) = angle(c1,c3) or angle(c1,c2) + angle(c2,c3) = angle(c1,c3) + 2*PI by Lm14; theorem c1 = euc2cpx(p1-p2) & c2 = euc2cpx(p3-p2) implies Re (c1.|.c2) = (p1`1 - p2`1)*(p3`1 - p2`1)+(p1`2 - p2`2)*(p3`2 - p2`2) & Im (c1.|.c2) = -(p1`1 - p2`1)*(p3`2 - p2`2)+(p1`2 - p2`2)*(p3`1 - p2`1) & |.c1.| = sqrt((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) & |.p1-p2.|=|.c1.| by Lm16; theorem for n being Element of NAT, q1 being Point of TOP-REAL n for f being Function of TOP-REAL n,R^1 st (for q being Point of TOP-REAL n holds f.q=|.q-q1.|) holds f is continuous by Lm20; theorem for n being Element of NAT, q1 being Point of TOP-REAL n ex f being Function of TOP-REAL n, R^1 st (for q being Point of TOP-REAL n holds f.q=|.q-q1.|) & f is continuous by Lm21;