:: Heron's Formula and Ptolemy's Theorem
:: by Marco Riccardi
::
:: Received January 10, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, EUCLID, COMPLEX1, ARYTM_1, CARD_1, SUPINF_2,
SUBSET_1, VALUED_0, FINSEQ_1, SIN_COS, COMPLEX2, RELAT_1, XXREAL_0,
ARYTM_3, REAL_1, EUCLID_3, COMPTRIG, FINSEQ_6, XCMPLX_0, MCART_1,
FUNCT_1, PROB_2, SQUARE_1, RVSUM_1, RLTOPSP1, JGRAPH_6, XBOOLE_0,
BORSUK_1, XXREAL_1, TOPS_2, STRUCT_0, PARTFUN1, ORDINAL2, TARSKI,
ZFMISC_1, PROJPL_1, TOPMETR, PCOMPS_1, METRIC_1, SIN_COS6, EUCLID_6,
PENCIL_1, RLVECT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
NUMBERS, XREAL_0, XXREAL_0, PARTFUN1, BINOP_1, STRUCT_0, PRE_TOPC,
SQUARE_1, VALUED_0, FINSEQ_1, FINSEQ_2, RVSUM_1, RLVECT_1, RLTOPSP1,
EUCLID, SIN_COS, JGRAPH_6, COMPTRIG, COMPLEX2, TOPMETR, RCOMP_1,
EUCLID_3, TOPS_2, XCMPLX_0, COMPLEX1, REAL_1, METRIC_1, PCOMPS_1,
SIN_COS6;
constructors REAL_1, SQUARE_1, BINOP_2, MONOID_0, RCOMP_1, SIN_COS, JGRAPH_6,
COMPTRIG, COMPLEX2, EUCLID_3, TOPS_2, SIN_COS6, FUNCSDOM, CONVEX1,
PCOMPS_1, COMPLEX1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, MONOID_0,
STRUCT_0, EUCLID, XCMPLX_0, TOPMETR, SQUARE_1, FUNCT_2, PRE_TOPC,
METRIC_1, BORSUK_1, SIN_COS6, VALUED_0, RVSUM_1, RLTOPSP1, SIN_COS,
ORDINAL1;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
definitions TARSKI;
equalities EUCLID, COMPLEX1, EUCLID_3, SQUARE_1, VALUED_1, ALGSTR_0, RLTOPSP1;
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, 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, RELAT_1,
RLVECT_1, RLTOPSP1, RLVECT_4;
schemes CLASSES1;
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;
Lm1: |.p1-p2.| = 0 iff p1=p2
proof
hereby
assume |.p1-p2.| = 0;
then p1-p2=0.TOP-REAL 2 by EUCLID_2:42;
hence p1=p2 by RLVECT_1:21;
end;
assume p1=p2;
then p1-p2=0.TOP-REAL 2 by RLVECT_1:5;
hence thesis by EUCLID_2:39;
end;
Lm2: |.p1-p2.| = |.p2-p1.|
proof
reconsider q = p1-p2 as Element of REAL 2 by EUCLID:22;
thus |.p1-p2.| = |. q qua real-valued FinSequence .| .= |.-q.| by EUCLID:10
.= |.-(p1 - p2).|
.= |.p2 - p1.| by RLVECT_1:33;
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
A1: 2*PI*0<=angle(p1,p2,p3) & angle(p1,p2,p3)<2*PI+2*PI*0 by COMPLEX2:70;
A2: 2*PI*0<=angle(p4,p5,p6) & angle(p4,p5,p6)<2*PI+2*PI*0 by COMPLEX2:70;
assume sin angle(p1,p2,p3) = sin angle(p4,p5,p6) & cos angle(p1,p2,p3) =
cos angle( p4,p5,p6);
hence thesis by A1,A2,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:36;
hence thesis by A1,SIN_COS:31;
end;
suppose
angle(p1,p2,p3)<>0;
then angle(p3,p2,p1)=2*PI-angle(p1,p2,p3) by EUCLID_3:37;
then sin angle(p1,p2,p3) = sin(-angle(p3,p2,p1)+2*PI)
.= sin(-angle(p3,p2,p1)) by SIN_COS:79
.= -sin(angle(p3,p2,p1)) by SIN_COS:31;
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:36;
end;
suppose
angle(p1,p2,p3)<>0;
then angle(p3,p2,p1)=2*PI-angle(p1,p2,p3) by EUCLID_3:37;
then cos angle(p1,p2,p3) = cos(-angle(p3,p2,p1)+2*PI)
.= cos(-angle(p3,p2,p1)) by SIN_COS:79
.= cos(angle(p3,p2,p1)) by SIN_COS:31;
hence thesis;
end;
end;
Lm3: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+2*PI
proof
angle(p4,p5,p6)>=0 by COMPLEX2:70;
then
A1: angle(p4,p5,p6)*2+2*PI>=0+2*PI by XREAL_1:7;
assume angle(p1,p2,p3) = 2*angle(p4,p5,p6)+2*PI;
hence contradiction by A1,COMPLEX2:70;
end;
Lm4: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)+4*PI
proof
angle(p4,p5,p6)>=0 by COMPLEX2:70;
then 4*PI>=2*PI & angle(p4,p5,p6)*2+4*PI>=0+4*PI by XREAL_1:7,64;
then
A1: angle(p4,p5,p6)*2+4*PI>=2*PI by XXREAL_0:2;
assume angle(p1,p2,p3) = 2*angle(p4,p5,p6)+4*PI;
hence contradiction by A1,COMPLEX2:70;
end;
Lm5: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-4*PI
proof
angle(p4,p5,p6)*2 < 2*PI*2 by COMPLEX2:70,XREAL_1:68;
then
A1: angle(p4,p5,p6)*2-4*PI<4*PI-4*PI by XREAL_1:9;
assume angle(p1,p2,p3) = 2*angle(p4,p5,p6)-4*PI;
hence contradiction by A1,COMPLEX2:70;
end;
Lm6: not angle(p1,p2,p3) = 2*angle(p4,p5,p6)-6*PI
proof
angle(p4,p5,p6)*2 < 2*PI*2 by COMPLEX2:70,XREAL_1:68;
then
A1: PI*(-2)<=(0 qua Real)*(-2) & angle(p4,p5,p6)*2-6*PI<4*PI-6*PI by XREAL_1:9;
assume angle(p1,p2,p3) = 2*angle(p4,p5,p6)-6*PI;
hence contradiction by A1,COMPLEX2:70;
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.TOP-REAL 2,p3-p2) by EUCLID_3:35
.= angle(c1,c2) by A1,COMPLEX2:73,EUCLID_3:17;
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:52;
hence thesis 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 that
A1: c2=0 and
A2: Arg c1 = 0;
thus angle(c1,c2) = Arg(Rotate(c2, -Arg c1)) by A2,COMPLEX2:def 3
.= 0 by A1,Lm8;
end;
Lm10: for c1,c2 being Complex st c2<>0 & Arg c2 - Arg c1 >= 0 holds
Arg(Rotate(c2, -Arg c1)) = Arg c2 - Arg c1
proof
let c1,c2 be Complex;
assume that
A1: c2<>0 and
A2: Arg c2 - Arg c1 >= 0;
set a = -Arg c1 + Arg c2;
set z = Rotate(c2, -Arg c1);
Arg c2<2*PI & 0<=Arg c1 by COMPTRIG:34;
then Arg c2+0<2*PI+Arg c1 by XREAL_1:8;
then
A3: z = |.c2.|*cos a + |.c2.|*sin a * <i> & Arg c2-Arg c1<2*PI+Arg c1-Arg c1
by COMPLEX2:def 2,XREAL_1:9;
A4: |.z.| = |.c2.| by COMPLEX2:53;
then z<>0 by A1,COMPLEX1:44,45;
hence thesis by A2,A3,A4,COMPTRIG:def 1;
end;
Lm11: for c1,c2 being Complex st c2<>0 & Arg c2 - Arg c1 >= 0 holds
angle(c1,c2) = Arg c2 - Arg c1
proof
let c1,c2 be Complex;
assume that
A1: c2<>0 and
A2: Arg c2 - Arg c1 >= 0;
thus angle(c1,c2) = Arg(Rotate(c2, -Arg c1)) by A1,COMPLEX2:def 3
.= Arg c2 - Arg c1 by A1,A2,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 that
A1: c2<>0 and
A2: Arg c2 - Arg c1 < 0;
set a = -Arg c1 + Arg c2;
A3: a+2*PI<0+2*PI by A2,XREAL_1:6;
set z = Rotate(c2, -Arg c1);
z = |.c2.|*cos a + |.c2.|*sin a * <i> by COMPLEX2:def 2;
then
A4: z = |.c2.|*cos(2*PI*1+a) + |.c2.|*sin a * <i> by COMPLEX2:9
.= |.c2.|*cos(2*PI+a) + |.c2.|*sin(2*PI*1+a) * <i> by COMPLEX2:8;
0<=Arg c2 & Arg c1<=2*PI by COMPTRIG:34;
then Arg c1+0<=2*PI+Arg c2 by XREAL_1:7;
then
A5: Arg c1-Arg c1<=2*PI+Arg c2-Arg c1 by XREAL_1:9;
A6: |.z.| = |.c2.| by COMPLEX2:53;
then z<>0 by A1,COMPLEX1:44,45;
hence thesis by A4,A5,A3,A6,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 that
A1: c2<>0 and
A2: Arg c2 - Arg c1 < 0;
thus angle(c1,c2) = Arg(Rotate(c2, -Arg c1)) by A1,COMPLEX2:def 3
.= 2*PI - Arg c1 + Arg c2 by A1,A2,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 3
.= 2*PI - Arg c1 + 0 by A1,A2,Lm9;
hence thesis by A1,A3,COMPLEX2:def 3;
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 A4,A5,Lm9;
hence thesis by A4,A5,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 A4,A6,Lm9;
hence thesis by A4,A6,COMPLEX2:def 3;
end;
suppose
Arg c2 - Arg c1 >= 0;
then --Arg c1 <= -0 by A6;
hence thesis by A6,COMPTRIG:34;
end;
end;
suppose
A7: Arg c1=0 & Arg c2<>0;
per cases;
suppose
Arg c2 - Arg c1 < 0;
hence thesis by A7,COMPTRIG:34;
end;
suppose
A8: Arg c2 - Arg c1 >= 0;
A9: angle(c1,c3) = 0 by A4,A7,Lm9;
angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1 + angle(c2,c3) by A4,A8
,Lm11
.= Arg c2 + (2*PI - Arg c2) by A4,A7,COMPLEX2:def 3;
hence thesis by A9;
end;
end;
suppose
A10: Arg c1<>0 & Arg c2<>0;
per cases;
suppose
A11: Arg c2 - Arg c1 < 0;
A12: angle(c1,c3) = 2*PI -Arg c1 by A4,A10,COMPLEX2:def 3;
angle(c1,c2) + angle(c2,c3) = 2*PI -Arg c1 +Arg c2 + angle(c2,c3)
by A4,A11,Lm13
.= 2*PI -Arg c1 + Arg c2 + (2*PI - Arg c2) by A4,A10,COMPLEX2:def 3
.= 2*PI + 2*PI -Arg c1;
hence thesis by A12;
end;
suppose
A13: Arg c2 - Arg c1 >= 0;
A14: angle(c1,c3) = 2*PI -Arg c1 by A4,A10,COMPLEX2:def 3;
angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1 + angle(c2,c3) by A4,A13
,Lm11
.= Arg c2 - Arg c1 + (2*PI - Arg c2) by A4,A10,COMPLEX2:def 3;
hence thesis by A14;
end;
end;
end;
suppose
A15: c2=0 & c3<>0;
per cases;
suppose
Arg c3 - Arg c2<0 & Arg c3 - Arg c1<0;
then Arg c3 - 0 < 0 by A15,COMPTRIG:def 1;
hence thesis by COMPTRIG:34;
end;
suppose
A16: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1<0;
per cases;
suppose
Arg c1=0;
hence thesis by A16,COMPTRIG:34;
end;
suppose
Arg c1<>0;
then
angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + angle(c2,c3) by A15,
COMPLEX2:def 3
.= 2*PI - Arg c1 + (Arg c3 - Arg c2) by A15,A16,Lm11
.= 2*PI - Arg c1 + (Arg c3 - 0) by A15,COMPTRIG:def 1
.= 2*PI - Arg c1 + Arg c3;
hence thesis by A15,A16,Lm13;
end;
end;
suppose
Arg c3 - Arg c2<0 & Arg c3 - Arg c1>=0;
then Arg c3 - 0 < 0 by A15,COMPTRIG:def 1;
hence thesis by COMPTRIG:34;
end;
suppose
A17: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1>=0;
per cases;
suppose
A18: Arg c1=0;
then angle(c1,c2) + angle(c2,c3) = 0 + angle(c2,c3) by A15,Lm9
.= 0 + (Arg c3 - Arg c2) by A15,A17,Lm11
.= 0 + (Arg c3 - 0) by A15,COMPTRIG:def 1;
hence thesis by A15,A17,A18,Lm11;
end;
suppose
A19: Arg c1<>0;
A20: angle(c1,c3) = Arg c3 - Arg c1 by A15,A17,Lm11;
angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + angle(c2,c3) by A15,A19,
COMPLEX2:def 3
.= 2*PI - Arg c1 + (Arg c3 - Arg c2) by A15,A17,Lm11
.= 2*PI - Arg c1 + (Arg c3 - 0) by A15,COMPTRIG:def 1;
hence thesis by A20;
end;
end;
end;
suppose
A21: c2<>0 & c3<>0;
per cases;
suppose
A22: Arg c3 - Arg c2<0 & Arg c3 - Arg c1<0;
per cases;
suppose
A23: Arg c2 - Arg c1 < 0;
A24: angle(c1,c3) = 2*PI - Arg c1 + Arg c3 by A21,A22,Lm13;
angle(c1,c2) + angle(c2,c3) = 2*PI - Arg c1 + Arg c2+ angle(c2,c3
) by A21,A23,Lm13
.= 2*PI - Arg c1 + Arg c2 + (2*PI - Arg c2 + Arg c3) by A21,A22,Lm13
.= 2*PI +2*PI - Arg c1 + Arg c3;
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 A21
,Lm11
.= Arg c2 - Arg c1 + (2*PI - Arg c2 + Arg c3) by A21,A22,Lm13
.= 2*PI - Arg c1 + Arg c3;
hence thesis by A21,A22,Lm13;
end;
end;
suppose
A25: 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 A21,Lm13
.= 2*PI - Arg c1 + Arg c2 + (Arg c3 - Arg c2) by A21,A25,Lm11
.= 2*PI - Arg c1 + Arg c3;
hence thesis by A21,A25,Lm13;
end;
suppose
Arg c2 - Arg c1 >= 0;
then Arg c2 - Arg c1 +(Arg c3 - Arg c2) >= 0+0 by A25;
hence thesis by A25;
end;
end;
suppose
A26: 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 A26;
hence thesis by A26;
end;
suppose
A27: Arg c2 - Arg c1 >= 0;
A28: angle(c1,c3) = Arg c3 - Arg c1 by A21,A26,Lm11;
angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1+ angle(c2,c3 ) by A21,A27
,Lm11
.= Arg c2 - Arg c1 + (2*PI -Arg c2 +Arg c3) by A21,A26,Lm13
.= 2*PI - Arg c1 + Arg c3;
hence thesis by A28;
end;
end;
suppose
A29: Arg c3 - Arg c2>=0 & Arg c3 - Arg c1>=0;
per cases;
suppose
A30: Arg c2 - Arg c1 < 0;
A31: angle(c1,c3) = Arg c3 - Arg c1 by A21,A29,Lm11;
angle(c1,c2) + angle(c2,c3) = 2*PI -Arg c1 + Arg c2+ angle (c2,c3
) by A21,A30,Lm13
.= 2*PI +Arg c2 - Arg c1 + (Arg c3 - Arg c2) by A21,A29,Lm11
.= 2*PI - Arg c1 + Arg c3;
hence thesis by A31;
end;
suppose
Arg c2 - Arg c1 >= 0;
then angle(c1,c2) + angle(c2,c3) = Arg c2 - Arg c1+ angle(c2,c3) by A21
,Lm11
.= Arg c2 - Arg c1 + (Arg c3 -Arg c2) by A21,A29,Lm11
.= - Arg c1 + Arg c3;
hence thesis by A21,A29,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(c1,c2) + angle(c2,c3) = angle(c1,c3) or angle(c1,c2) + angle(c2,c3
) = angle(c1,c3) + 2*PI by Lm14;
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;
hence thesis by A1,Lm7;
end;
Lm15: (p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2
proof
reconsider pp=p2 as Element of REAL 2 by EUCLID:22;
A1: (-p2)`1 = (-pp).1
.= -pp.1 by VALUED_1:8
.= -p2`1;
A2: euc2cpx(p1-p2) = euc2cpx(p1)-euc2cpx(p2) by EUCLID_3:15
.= euc2cpx(p1)+(-euc2cpx(p2))
.= euc2cpx(p1)+euc2cpx(-p2) by EUCLID_3:13;
hence (p1-p2)`1 = Re (euc2cpx(p1)+euc2cpx(-p2)) by COMPLEX1:12
.= Re euc2cpx(p1) + Re euc2cpx(-p2) by COMPLEX1:8
.= p1`1 + Re euc2cpx(-p2) by COMPLEX1:12
.= p1`1 + (-p2)`1 by COMPLEX1:12
.= p1`1 - p2`1 by A1;
A3: (-p2)`2 = (-pp).2
.= -pp.2 by VALUED_1:8
.= -p2`2;
thus (p1-p2)`2 = Im (euc2cpx(p1)+euc2cpx(-p2)) by A2,COMPLEX1:12
.= Im euc2cpx(p1) + Im euc2cpx(-p2) by COMPLEX1:8
.= p1`2 + Im euc2cpx(-p2) by COMPLEX1:12
.= p1`2 + (-p2)`2 by COMPLEX1:12
.= 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 that
A1: c1 = euc2cpx(p1-p2) and
A2: c2 = euc2cpx(p3-p2);
A3: Re c2 = (p3-p2)`1 by A2,COMPLEX1:12
.= p3`1 - p2`1 by Lm15;
A4: Im c2 = (p3-p2)`2 by A2,COMPLEX1:12
.= p3`2 - p2`2 by Lm15;
A5: Im c1 = (p1-p2)`2 by A1,COMPLEX1:12
.= p1`2 - p2`2 by Lm15;
A6: Re c1 = (p1-p2)`1 by A1,COMPLEX1:12
.= p1`1 - p2`1 by Lm15;
hence Re (c1.|.c2) = (p1`1 - p2`1)*(p3`1 - p2`1)+(p1`2 - p2`2)*(p3`2 - p2`2)
by A3,A5,A4,EUCLID_3:39;
thus Im (c1.|.c2) = -(p1`1 - p2`1)*(p3`2 - p2`2)+(p1`2 - p2`2)*(p3`1 - p2`1)
by A6,A3,A5,A4,EUCLID_3:40;
thus |.c1.| = sqrt((p1-p2)`1^2 + (Im c1)^2) by A1,COMPLEX1:12
.= sqrt((p1-p2)`1^2 + (p1-p2)`2^2) by A1,COMPLEX1:12
.= 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 thesis by A1,EUCLID_3:25;
end;
:: Meister-Gauss formula
definition
let p1,p2,p3;
::$N Meister-Gauss formula (for triangles
func the_area_of_polygon3(p1,p2,p3) -> Real equals
((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;
correctness;
end;
definition
let p1,p2,p3;
func the_perimeter_of_polygon3(p1,p2,p3) -> Real 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.TOP-REAL 2.| by RLVECT_1:5
.= 0 by EUCLID_2:39;
hence thesis by A1;
end;
suppose
A2: p1<>p2;
per cases;
suppose
A3: p2=p3;
then |.p3-p2.| = |.0.TOP-REAL 2.| by RLVECT_1:5
.= 0 by EUCLID_2:39;
hence thesis by A3;
end;
suppose
A4: p2<>p3;
set b = euc2cpx(p3-p2);
set a = euc2cpx(p1-p2);
A5: now
assume
A6: a=0 or b=0;
per cases by A6;
suppose
a=0;
hence contradiction by A2,EUCLID_3:18,RLVECT_1:21;
end;
suppose
b=0;
hence contradiction by A4,EUCLID_3:18,RLVECT_1:21;
end;
end;
A7: now
assume
A8: |.a.|*|.b.|=0;
per cases by A8;
suppose
|.a.|=0;
hence contradiction by A5,COMPLEX1:45;
end;
suppose
|.b.|=0;
hence contradiction by A5,COMPLEX1:45;
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:69
.= |.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:81
.= (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
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
A1: |.p3-p2.|*sin angle(p3,p2,p1)*|.p1-p2.| = |.p3-p1.|*sin angle(p2,p1,p3)*
|.p1-p2.|;
assume p2<>p1;
then |.p1-p2.|<>0 by Lm1;
hence thesis by A1,XCMPLX_1:5;
end;
:: Law of Cosines
::$N Law of Cosines
::$L https://en.wikipedia.org/wiki/Law_of_cosines 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 that
A1: a = |.p1-p2.| & b = |.p3-p2.| and
A2: c = |.p3-p1.|;
per cases;
suppose
A3: p1=p2;
then |.p1-p2.| = |.0.TOP-REAL 2.| by RLVECT_1:5
.= 0 by EUCLID_2:39;
hence thesis by A1,A2,A3;
end;
suppose
A4: p1<>p2;
per cases;
suppose
A5: p2=p3;
then |.p3-p2.| = |.0.TOP-REAL 2.| by RLVECT_1:5
.= 0 by EUCLID_2:39;
then |.p1-p2.|^2 + |.p3-p2.|^2 - 2*|.p1-p2.|*|.p3-p2.|*cos angle(p1,p2,
p3) = |.-(p1 - p2).|^2 by EUCLID:71
.= |.p2 - p1.|^2 by RLVECT_1:33;
hence thesis by A1,A2,A5;
end;
suppose
A6: p2<>p3;
set c2 = euc2cpx(p3-p2);
set c1 = euc2cpx(p1-p2);
A7: now
assume
A8: c1=0 or c2=0;
per cases by A8;
suppose
c1=0;
hence contradiction by A4,EUCLID_3:18,RLVECT_1:21;
end;
suppose
c2=0;
hence contradiction by A6,EUCLID_3:18,RLVECT_1:21;
end;
end;
A9: now
assume
A10: |.c1.|*|.c2.|=0;
per cases by A10;
suppose
|.c1.|=0;
hence contradiction by A7,COMPLEX1:45;
end;
suppose
|.c2.|=0;
hence contradiction by A7,COMPLEX1:45;
end;
end;
A11: a^2+b^2-c^2 = |.p1.|^2-2*|(p2, p1)|+|.p2.|^2+|.p3-p2.|^2- |.p3-p1.|
^2 by A1,A2,EUCLID_2:46
.= |.p1.|^2-2*|(p2, p1)|+|.p2.|^2 + |.p3-p2.|^2 -(|.p3.|^2-2*|(p1,
p3)|+|.p1.|^2) by EUCLID_2:46
.= -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:46
.= 2*(- |(p2,p1)|+|.p2.|^2 - |(p2, p3)|+ |(p1, p3)|);
|.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 A7,COMPLEX2:69
.= (Re (c1.|.c2)/((|.c1.|*|.c2.|)/(|.c1.|*|.c2.|))) by XCMPLX_1:81
.= Re (c1.|.c2)/1 by A9,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:41
.= |(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:41
.= |(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:41
.= |(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:41
.= |(p1,p3)|- |(p1,p2)|- |(p2,p3)|+|.p2.|^2 by EUCLID_2:36;
hence thesis by A1,A11;
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
set c1=euc2cpx(p1-p);
set c2=euc2cpx(p2-p);
assume p in LSeg(p1,p2);
then consider l be Real such that
A1: p=(1-l)*p1+l*p2 and
A2: 0<=l and
A3: l<=1;
reconsider l as Real;
A4: p2-p = p2-((1+(-l))*p1 +l*p2) by A1
.= p2-((1)*p1+(-l)*p1 +l*p2) by RLVECT_1:def 6
.= p2+(-1)*((1)*p1+(-l)*p1 +l*p2)
.= p2+((-1)*((1)*p1+(-l)*p1)+(-1)*(l*p2)) by RLVECT_1:def 5
.= p2+((-1)*(p1+(-l)*p1)+(-1)*(l*p2)) by RLVECT_1:def 8
.= p2+((-1)*(p1+(-l)*p1)+((-1)*l)*p2) by RLVECT_1:def 7
.= p2+((-1)*p1+(-1)*((-l)*p1)+(-l)*p2) by RLVECT_1:def 5
.= p2+((-1)*p1+((-1)*(-l))*p1+(-l)*p2) by RLVECT_1:def 7
.= p2+((-1)*p1+(l*p1+(-l)*p2)) by RLVECT_1:def 3
.= p2+(-p1+(l*p1+(-l)*p2))
.= (-p1+p2)+(l*(p1)+(-l)*p2) by RLVECT_1:def 3
.= (-p1+p2)+(l*(--p1)+(-l)*p2)
.= (-p1+p2)+(l*((-1)*(-p1))+(-l)*p2)
.= (-p1+p2)+(l*(-1)*(-p1)+(-l)*p2) by RLVECT_1:def 7
.= (-p1+p2)+(-l)*(-p1+p2) by RLVECT_1:def 5
.= (1)*(-p1+p2)+(-l)*(-p1+p2) by RLVECT_1:def 8
.= (1+(-l))*(-p1+p2) by RLVECT_1:def 6
.= (1-l)*(-p1+p2);
assume
A5: p<>p1;
A6: l<>0
proof
assume l=0;
then p =1*p1+0.TOP-REAL 2 by A1,RLVECT_1:10
.=1*p1 by RLVECT_1:4
.=p1 by RLVECT_1:def 8;
hence contradiction by A5;
end;
assume
A7: p<>p2;
l<>1
proof
assume l=1;
then p = 0.TOP-REAL 2+1*p2 by A1,RLVECT_1:10
.= 1*p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8;
hence contradiction by A7;
end;
then l<1 by A3,XXREAL_0:1;
then -1 < -l by XREAL_1:24;
then
A8: -1+1 < -l+1 by XREAL_1:6;
A9: -c2<>0
proof
assume -c2 = 0;
then |.p2-p.| = 0 by COMPLEX1:44,EUCLID_3:25;
then p2-p = 0.TOP-REAL 2 by EUCLID_2:42;
hence contradiction by A7,RLVECT_1:21;
end;
set r = -l/(1-l);
A10: p1-p = p1-((1+(-l))*p1 +l*p2) by A1
.= p1-((1)*p1+(-l)*p1 +l*p2) by RLVECT_1:def 6
.= p1+(-1)*((1)*p1+(-l)*p1 +l*p2)
.= p1+((-1)*((1)*p1+(-l)*p1)+(-1)*(l*p2)) by RLVECT_1:def 5
.= p1+((-1)*(p1+(-l)*p1)+(-1)*(l*p2)) by RLVECT_1:def 8
.= p1+((-1)*(p1+(-l)*p1)+((-1)*l)*p2) by RLVECT_1:def 7
.= p1+((-1)*p1+(-1)*((-l)*p1)+(-l)*p2) by RLVECT_1:def 5
.= p1+((-1)*p1+((-1)*(-l))*p1+(-l)*p2) by RLVECT_1:def 7
.= p1+((-1)*p1+(l*p1+(-l)*p2)) by RLVECT_1:def 3
.= p1+(-p1+(l*p1+(-l)*p2))
.= (p1+(-p1))+(l*p1+(-l)*p2) by RLVECT_1:def 3
.= 0.TOP-REAL 2 +(l*p1+(-l)*p2) by RLVECT_1:5
.= l*p1+(l*(-1))*p2 by RLVECT_1:4
.= l*p1+l*((-1)*p2) by RLVECT_1:def 7
.= l*p1+l*(-p2)
.= l*(p1-p2) by RLVECT_1:def 5;
cpx2euc(c2 * r) = r*cpx2euc(c2) by EUCLID_3:19
.= (-l/(1-l))*((1-l)*(-p1+p2)) by A4,EUCLID_3:2
.= ((-l/(1-l))*(1-l))*(-p1+p2) by RLVECT_1:def 7
.= (((-l)/(1-l))*(1-l))*(-p1+p2) by XCMPLX_1:187
.= (((1-l)/(1-l))*(-l))*(-p1+p2) by XCMPLX_1:75
.= ((1)*(-l))*(-p1+p2) by A8,XCMPLX_1:60
.= (l*(-1))*(-p1+p2)
.= l*((-1)*(-p1+p2)) by RLVECT_1:def 7
.= l*((-1)*(-p1)+(-1)*p2) by RLVECT_1:def 5
.= l*(--p1+(-1)*p2)
.= l*(--p1+-p2)
.= l*(--p1+(-p2))
.= l*(p1+(-p2))
.= cpx2euc(c1) by A10,EUCLID_3:2;
then c1 = c2*r by EUCLID_3:3;
then
A11: Arg(-c2) = Arg c1 by A2,A6,A8,COMPLEX2:28;
angle(c1,-c2) = 0
proof
per cases;
suppose
Arg(-c2) - Arg c1 < 0;
hence thesis by A11;
end;
suppose
Arg(-c2) - Arg c1 >= 0;
hence thesis by A11,A9,Lm11;
end;
end;
then angle(c1,-(-c2)) = PI by A9,COMPLEX2:68;
hence thesis by Lm7;
end;
theorem Th9:
p in LSeg(p2,p3) & p<>p2 implies angle(p3,p2,p1)=angle(p,p2,p1)
proof
set c = euc2cpx(p-p2);
set c1 = euc2cpx(p1-p2);
set c3 = euc2cpx(p3-p2);
assume p in LSeg(p2,p3);
then consider l be Real such that
A1: p=(1-l)*p2+l*p3 and
A2: 0<=l and
l<=1;
reconsider l as Real;
A3: p - p2 = (1+(-l))*p2 +l*p3 -p2 by A1
.= (1)*p2+(-l)*p2 +l*p3 -p2 by RLVECT_1:def 6
.= p2 +(-l)*p2 +l*p3 -p2 by RLVECT_1:def 8
.= (p2 +(-l)*p2)+ (l*p3 + -p2) by RLVECT_1:def 3
.= p2 +((-l)*p2 +(l*p3 + -p2)) by RLVECT_1:def 3
.= p2 +(-p2 + ((-l)*p2 + l*p3)) by RLVECT_1:def 3
.= (p2 + -p2) + ((-l)*p2 + l*p3) by RLVECT_1:def 3
.= 0.TOP-REAL 2 + ((-l)*p2 + l*p3) by RLVECT_1:5
.= (l*(-1))*p2 + l*p3 by RLVECT_1:4
.= l*((-1)*p2) + l*p3 by RLVECT_1:def 7
.= l*(-p2) + l*p3
.= l*(p3-p2) by RLVECT_1:def 5;
assume
A4: p<>p2;
A5: l <> 0
proof
assume l=0;
then p = 1*p2+0.TOP-REAL 2 by A1,RLVECT_1:10
.= 1*p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8;
hence contradiction by A4;
end;
cpx2euc(c3 * l) = l*cpx2euc(c3) by EUCLID_3:19
.= l*(p3-p2) by EUCLID_3:2
.= cpx2euc(c) by A3,EUCLID_3:2;
then c = c3 * l by EUCLID_3:3;
then
A6: Arg c = Arg c3 by A2,A5,COMPLEX2:27;
angle(c3,c1) = angle(c,c1)
proof
per cases;
suppose
A7: Arg c3 = 0 or c1 <> 0;
then angle(c3,c1)=Arg(Rotate(c1, -Arg c3)) by COMPLEX2:def 3
.= angle(c,c1) by A6,A7,COMPLEX2:def 3;
hence thesis;
end;
suppose
A8: not (Arg c3 = 0 or c1 <> 0);
then angle(c3,c1)=2*PI - Arg c3 by COMPLEX2:def 3
.= angle(c,c1) by A6,A8,COMPLEX2:def 3;
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 A1,Th9;
per cases;
suppose
A4: angle(p1,p2,p3) = 0;
then angle(p3,p2,p1) = 0 by EUCLID_3:36;
then
A5: angle(p,p2,p1) = 0 by A1,A2,Th9;
thus angle(p1,p2,p3) = angle(p3,p2,p1) by A4,EUCLID_3:36
.= angle(p,p2,p1) by A1,A2,Th9
.= angle(p1,p2,p) by A5,EUCLID_3:36;
end;
suppose
A6: angle(p1,p2,p3) <> 0;
then
A7: angle(p,p2,p1) <> 0 by A3,EUCLID_3:36;
thus angle(p1,p2,p3) = 2*PI - angle(p3,p2,p1) by A6,EUCLID_3:38
.= 2*PI - angle(p,p2,p1) by A1,A2,Th9
.= angle(p1,p2,p) by A7,EUCLID_3:37;
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
set pc1 = p1 - |[a,b]|;
set pc2 = p2 - |[a,b]|;
reconsider r9=r as Real;
assume p1 in inside_of_circle(a,b,r);
then p1 in {p:|.p - |[a,b]|.| < r} by JGRAPH_6:def 6;
then
A1: ex p19 be Point of TOP-REAL 2 st p1=p19 & |.p19 - |[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
A2: ex p29 be Point of TOP-REAL 2 st p2=p29 & |.p29 - |[a,b ]|.| > r;
then 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 being_homeomorphism and
A5: f.0 = pc1 and
A6: f.1 = pc2 by A1,JORDAN5A:3;
reconsider g=f as Function of I[01], TOP-REAL 2 by JORDAN6:3;
0 in the carrier of I[01] by BORSUK_1:40,XXREAL_1:1;
then 0 in dom g by FUNCT_2:def 1;
then
A7: g/.0 = pc1 by A5,PARTFUN1:def 6;
1 in the carrier of I[01] by BORSUK_1:40,XXREAL_1:1;
then 1 in dom g by FUNCT_2:def 1;
then
A8: g/.1 = pc2 by A6,PARTFUN1:def 6;
f is continuous by A4,TOPS_2:def 5;
then consider s be Point of I[01] such that
A9: |.g/.s.| = r9 by A1,A2,A7,A8,JORDAN2C:86,JORDAN6:3;
A10: s in the carrier of I[01];
s in [.0,1.] by BORSUK_1:40;
then s in {s9 where s9 is Element of ExtREAL:0 <= s9 & s9 <= 1} by
XXREAL_1:def 1;
then
A11: ex s9 be Element of ExtREAL st s=s9 & 0 <= s9 & s9 <= 1;
reconsider s as Real;
set p9 = f.s;
s in dom g by A10,FUNCT_2:def 1;
then rng g c= the carrier of TOP-REAL 2 & g.s in rng g by FUNCT_1:3
,RELAT_1:def 19;
then reconsider p9 as Point of TOP-REAL 2;
set p = p9 + |[a,b]|;
take p;
f.s = (1-s)*pc1 + s*pc2 by A3,BORSUK_1:40
.= (1-s)*p1 - (1-s)*|[a,b]| + s*(p2 - |[a,b]|) by RLVECT_1:34
.= (1-s)*p1 - (1-s)*|[a,b]| + (s*p2 - s*|[a,b]|) by RLVECT_1:34
.= (1-s)*p1 + (-(1-s))*|[a,b]| + (s*p2 - s*|[a,b]|) by RLVECT_1:79
.= (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
RLVECT_1:def 6
.= ((1-s)*p1 + (-1)*|[a,b]|) +s*|[a,b]| + (s*p2 + -s*|[a,b]|) by
RLVECT_1:def 3
.= ((1-s)*p1 + (-1)*|[a,b]|) + (s*|[a,b]|+(s*p2 + -s*|[a,b]|)) by
RLVECT_1:def 3
.= ((1-s)*p1 + (-1)*|[a,b]|) + (s*|[a,b]| +(-s*|[a,b]|) +s*p2) by
RLVECT_1:def 3
.= ((1-s)*p1 + (-1)*|[a,b]|) + (s*|[a,b]|+(-s)*|[a,b]|+s*p2) by RLVECT_1:79
.= ((1-s)*p1 + (-1)*|[a,b]|) + ((s+(-s))*|[a,b]|+s*p2) by RLVECT_1:def 6
.= ((1-s)*p1 + (-1)*|[a,b]|) + ((0.TOP-REAL 2)+s*p2) by RLVECT_1:10
.= ((1-s)*p1 + (-1)*|[a,b]|) + s*p2 by RLVECT_1:4
.= (1-s)*p1 + s*p2 + (-1)*|[a,b]| by RLVECT_1:def 3;
then
A12: p = (1-s)*p1 + s*p2 + (-1)*|[a,b]| + |[a,b]|
.= (1-s)*p1 + s*p2 + - |[a,b]| + |[a,b]|
.= ((1-s)*p1 + s*p2) + (- |[a,b]| +|[a,b]|) by RLVECT_1:def 3
.= ((1-s)*p1 + s*p2) + 0.TOP-REAL 2 by RLVECT_1:5
.= (1-s)*p1 + s*p2 by RLVECT_1:4;
r = |. p9 + 0.TOP-REAL 2 .| by A9,RLVECT_1:4
.= |. p9 +(|[a,b]| - |[a,b]|) .| by RLVECT_1:5
.= |. p9 + |[a,b]| + - |[a,b]| .| by RLVECT_1:def 3
.= |. p - |[a,b]| .|;
then p in {p99 where p99 is Point of (TOP-REAL 2):|. p99 - |[a,b]|.| = r};
then
A13: p in circle(a,b,r) by JGRAPH_6:def 5;
(1-s)*p1 + s*p2 in LSeg(p1,p2) by A11;
hence thesis by A12,A13,XBOOLE_0:def 4;
end;
theorem Th11:
angle(p1,p,p2) = PI implies p in LSeg(p1,p2)
proof
assume
A1: angle(p1,p,p2) = PI;
set r = |.p-p1.|;
set b = p1`2;
set a = p1`1;
A2: p1 = |[a,b]| by EUCLID:53;
per cases;
suppose
p=p1 or p=p2;
hence thesis by RLTOPSP1:68;
end;
suppose
A3: p<>p1 & p<>p2;
A4: |.p2-p1.|^2 = |.p1-p.|^2 + |.p2-p.|^2 - 2*|.p1-p.|*|.p2-p.|* (-1) by A1,Th7
,SIN_COS:77
.= (|.p1-p.|+|.p2-p.|)^2;
|.p2-p1.|>r
proof
assume |.p2-p1.|<=r;
then |.p2-p1.|^2<=r^2 by SQUARE_1:15;
then (r+|.p2-p.|)^2 <= r^2 by A4,Lm2;
then r^2+2*r*|.p2-p.|+|.p2-p.|^2-r^2<=r^2-r^2 by XREAL_1:9;
then
A5: (2*r+|.p2-p.|)*|.p2-p.|<=0;
|.p2-p.|<>0 by A3,Lm1;
hence contradiction by A5;
end;
then p2 in {p4 : |.p4- |[a,b]| .|>r} by A2;
then
A6: p2 in outside_of_circle(a,b,r) by JGRAPH_6:def 8;
A7: |.p1 - |[a,b]|.|=0 by A2,Lm1;
r<>0 by A3,Lm1;
then p1 in {p4 : |.p4- |[a,b]| .|<r} by A7;
then p1 in inside_of_circle(a,b,r) by JGRAPH_6:def 6;
then consider p3 such that
A8: p3 in LSeg(p1,p2) /\ circle(a,b,r) by A6,Lm17;
A9: euc2cpx(p1)<> euc2cpx(p2) by A1,COMPLEX2:79;
A10: euc2cpx(p)<> euc2cpx(p1) & euc2cpx(p)<> euc2cpx(p2) by A3,EUCLID_3:4;
A11: angle(p,p1,p2) = 0
proof
assume angle(p,p1,p2) <> 0;
then
A12: angle(p,p1,p2) > 0 by COMPLEX2:70;
A13: angle(p,p1,p2)<2*PI by COMPLEX2:70;
per cases by A10,A9,COMPLEX2:88;
suppose
A14: angle(p,p1,p2)+angle(p1,p2,p)+angle(p2,p,p1) = PI;
A15: angle(p1,p2,p)>=0 by COMPLEX2:70;
angle(p,p1,p2)+angle(p1,p2,p)+PI = PI by A1,A14,COMPLEX2:82;
hence contradiction by A12,A15;
end;
suppose
A16: angle(p,p1,p2)+angle(p1,p2,p)+angle(p2,p,p1) = 5*PI;
angle(p1,p2,p)<2*PI by COMPLEX2:70;
then
A17: angle(p,p1,p2)+angle(p1,p2,p) < 2*PI+2*PI by A13,XREAL_1:8;
angle(p,p1,p2)+angle(p1,p2,p)+PI = 5*PI by A1,A16,COMPLEX2:82;
hence contradiction by A17;
end;
end;
p3 in circle(a,b,r) by A8,XBOOLE_0:def 4;
then p3 in {p4: |.p4- |[a,b]| .|=r} by JGRAPH_6:def 5;
then
A18: ex p4 st p3=p4 & |.p4 - |[a,b]|.| = r;
then
A19: |.p3-p1.|=r by EUCLID:53;
r<>0 by A3,Lm1;
then
A20: p3<>p1 by A2,A18,Lm1;
A21: p3 in LSeg(p1,p2) by A8,XBOOLE_0:def 4;
|.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 A21,A19,A20,A11,Th10
.= 0 by SIN_COS:31;
then |.p3-p.|=0;
hence thesis by A21,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 consider l1 be Real such that
A1: p=(1-l1)*p1+l1*p3 and
A2: 0<=l1 and
l1<=1;
assume p in LSeg(p1,p4);
then consider l2 be Real such that
A3: p=(1-l2)*p1+l2*p4 and
A4: 0<=l2 and
l2<=1;
(1+(-l1))*p1+l1*p3 = (1+(-l2))*p1+l2*p4 by A1,A3;
then 1*p1+(-l1)*p1+l1*p3 = (1+(-l2))*p1+l2*p4 by RLVECT_1:def 6;
then 1*p1+(-l1)*p1+l1*p3 = 1*p1+(-l2)*p1+l2*p4 by RLVECT_1:def 6;
then p1+(-l1)*p1+l1*p3 = 1*p1+(-l2)*p1+l2*p4 by RLVECT_1:def 8;
then p1+(-l1)*p1+l1*p3 = p1+(-l2)*p1+l2*p4 by RLVECT_1:def 8;
then -p1+(p1+((-l1)*p1+l1*p3)) = -p1+(p1+(-l2)*p1+l2*p4) by RLVECT_1:def 3;
then (-p1+p1)+((-l1)*p1+l1*p3) = -p1+(p1+(-l2)*p1+l2*p4) by RLVECT_1:def 3;
then 0.TOP-REAL 2+((-l1)*p1+l1*p3) = -p1+(p1+(-l2)*p1+l2*p4) by RLVECT_1:5;
then (-l1)*p1+l1*p3 = -p1+(p1+(-l2)*p1+l2*p4) by RLVECT_1:4;
then (-l1)*p1+l1*p3 = -p1+(p1+((-l2)*p1+l2*p4)) by RLVECT_1:def 3;
then (-l1)*p1+l1*p3 = (-p1+p1)+((-l2)*p1+l2*p4) by RLVECT_1:def 3;
then (-l1)*p1+l1*p3 = 0.TOP-REAL 2+((-l2)*p1+l2*p4) by RLVECT_1:5;
then
A5: (-l1)*p1+l1*p3 = (-l2)*p1+l2*p4 by RLVECT_1:4;
assume that
A6: p3<>p4 and
A7: p<>p1;
per cases;
suppose
A8: l1<=l2;
per cases by A8,XXREAL_0:1;
suppose
A9: l1<l2;
(1/l2)*((-l1)*p1)+(1/l2)*(l1*p3)=(1/l2)*((-l2)*p1+l2*p4) by A5,
RLVECT_1:def 5;
then (1/l2)*(-l1)*p1+(1/l2)*(l1*p3) = (1/l2)*((-l2)*p1+l2*p4) by
RLVECT_1:def 7;
then (-1)*((1/l2)*l1)*p1+(1/l2)*l1*p3 = (1/l2)*((-l2)*p1+l2*p4) by
RLVECT_1:def 7;
then (-1)*(l1/l2*1)*p1+(1/l2)*l1*p3 = (1/l2)*((-l2)*p1+l2*p4) by
XCMPLX_1:75;
then (-l1/l2)*p1+(l1/l2)*1*p3 = (1/l2)*((-l2)*p1+l2*p4) by XCMPLX_1:75;
then (-l1/l2)*p1+(l1/l2)*p3 = (1/l2)*((-l2)*p1)+(1/l2)*(l2*p4) by
RLVECT_1:def 5;
then (-l1/l2)*p1+(l1/l2)*p3 = (1/l2)*(-l2)*p1+(1/l2)*(l2*p4) by
RLVECT_1:def 7;
then (-l1/l2)*p1+(l1/l2)*p3 = (-1)*((1/l2)*l2)*p1+(1/l2)*l2*p4 by
RLVECT_1:def 7;
then (-l1/l2)*p1+(l1/l2)*p3 = (-1)*((l2/l2)*1)*p1+(1/l2)*l2*p4 by
XCMPLX_1:75;
then (-l1/l2)*p1+(l1/l2)*p3 = (-1)*(l2/l2)*p1+(l2/l2)*1*p4 by XCMPLX_1:75
;
then (-l1/l2)*p1+(l1/l2)*p3 = (-1)*1*p1+(l2/l2)*p4 by A2,A9,XCMPLX_1:60;
then (-l1/l2)*p1+(l1/l2)*p3 = (-1)*p1+1*p4 by A2,A9,XCMPLX_1:60;
then (-l1/l2)*p1+(l1/l2)*p3 = -p1+1*p4;
then
A10: (-l1/l2)*p1+(l1/l2)*p3 = p4+(-p1) by RLVECT_1:def 8;
l1/l2<l2/l2 by A2,A9,XREAL_1:74;
then
A11: l1/l2<1 by A2,A9,XCMPLX_1:60;
p4 = p4 - p1 + p1 by RLVECT_4:1
.= p1+(-l1/l2)*p1+(l1/l2)*p3 by A10,RLVECT_1:def 3
.= 1*p1+(-l1/l2)*p1+(l1/l2)*p3 by RLVECT_1:def 8
.= (1+(-l1/l2))*p1+(l1/l2)*p3 by RLVECT_1:def 6
.= (1-l1/l2)*p1+(l1/l2)*p3;
hence thesis by A2,A4,A11;
end;
suppose
l1=l2;
then l1*p1+(-l1)*p1+l1*p3 = l1*p1+((-l1)*p1+l1*p4) by A5,RLVECT_1:def 3;
then (l1+(-l1))*p1+l1*p3 = l1*p1+((-l1)*p1+l1*p4) by RLVECT_1:def 6;
then 0.TOP-REAL 2+l1*p3 = l1*p1+((-l1)*p1+l1*p4) by RLVECT_1:10;
then l1*p3 = l1*p1+((-l1)*p1+l1*p4) by RLVECT_1:4;
then l1*p3 = l1*p1+(-l1)*p1+l1*p4 by RLVECT_1:def 3;
then l1*p3 = (l1+(-l1))*p1+l1*p4 by RLVECT_1:def 6;
then l1*p3 = 0.TOP-REAL 2+l1*p4 by RLVECT_1:10;
then
A12: l1*p3 = l1*p4 by RLVECT_1:4;
per cases by A12,RLVECT_1:36;
suppose
l1=0;
then p = p1+(0 qua Real)*p3 by A1,RLVECT_1:def 8
.= p1+0.TOP-REAL 2 by RLVECT_1:10
.= p1 by RLVECT_1:4;
hence thesis by A7;
end;
suppose
p3=p4;
hence thesis by A6;
end;
end;
end;
suppose
A13: l1>l2;
(1/l1)*((-l1)*p1)+(1/l1)*(l1*p3) = (1/l1)*((-l2)*p1+l2*p4) by A5,
RLVECT_1:def 5;
then (1/l1)*(-l1)*p1+(1/l1)*(l1*p3) = (1/l1)*((-l2)*p1+l2*p4) by
RLVECT_1:def 7;
then (-1)*((1/l1)*l1)*p1+(1/l1)*l1*p3 = (1/l1)*((-l2)*p1+l2*p4) by
RLVECT_1:def 7;
then (-1)*(l1/l1*1)*p1+(1/l1)*l1*p3 = (1/l1)*((-l2)*p1+l2*p4) by
XCMPLX_1:75;
then (-l1/l1)*p1+(l1/l1)*1*p3 = (1/l1)*((-l2)*p1+l2*p4) by XCMPLX_1:75;
then (-1)*p1+(l1/l1)*1*p3 = (1/l1)*((-l2)*p1+l2*p4) by A4,A13,XCMPLX_1:60;
then (1)*p3+(-1)*p1 = (1/l1)*((-l2)*p1+l2*p4) by A4,A13,XCMPLX_1:60;
then (1)*p3+-p1 = (1/l1)*((-l2)*p1+l2*p4);
then p3+ -p1 = (1/l1)*((-l2)*p1+l2*p4) by RLVECT_1:def 8;
then p3-p1 = (1/l1)*((-l2)*p1)+(1/l1)*(l2*p4) by RLVECT_1:def 5;
then p3-p1 = (1/l1)*(-l2)*p1+(1/l1)*(l2*p4) by RLVECT_1:def 7;
then p3-p1 = (-1)*((1/l1)*l2)*p1+(1/l1)*l2*p4 by RLVECT_1:def 7;
then
A14: p3-p1 = (-1)*((l2/l1)*1)*p1+(1/l1)*l2*p4 by XCMPLX_1:75;
l2/l1<l1/l1 by A4,A13,XREAL_1:74;
then
A15: l2/l1<1 by A4,A13,XCMPLX_1:60;
p3 = p3 - p1 + p1 by RLVECT_4:1
.= (-l2/l1)*p1+(l2/l1)*p4 + p1 by A14,XCMPLX_1:75
.= p1+(-l2/l1)*p1+(l2/l1)*p4 by RLVECT_1:def 3
.= 1*p1+(-l2/l1)*p1+(l2/l1)*p4 by RLVECT_1:def 8
.= (1+(-l2/l1))*p1+(l2/l1)*p4 by RLVECT_1:def 6
.= (1-l2/l1)*p1+(l2/l1)*p4;
hence thesis by A2,A4,A15;
end;
end;
theorem Th13:
p in LSeg(p1,p3) & p<>p1 & 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 p in LSeg(p1,p3) & p<>p1 & p<>p3;
then
A1: angle(p1,p,p3) = PI by Th8;
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;
hence thesis by A1;
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 thesis;
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:70;
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:6;
hence thesis by A5,COMPLEX2:70;
end;
end;
per cases;
suppose
A6: angle(p3,p,p1)=0;
then angle(p1,p,p3) = 0 by EUCLID_3:36;
hence thesis by A3,A6,EUCLID_3:36;
end;
suppose
A7: angle(p3,p,p1)<>0;
then angle(p1,p,p3)=2*PI-angle(p3,p,p1) by EUCLID_3:37;
hence thesis by A3,A7,EUCLID_3:37;
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,A2,A3,A4,A5,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:70;
then angle(p3,p,p4)+2*PI>=0+2*PI by XREAL_1:6;
hence thesis by A7,COMPLEX2:70;
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:70;
then angle(p3,p,p4)-2*PI<2*PI-2*PI by XREAL_1:9;
hence thesis by A8,COMPLEX2:70;
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
A3: p1,p2,p3 are_mutually_distinct;
|.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
A4: |.p3-p2.| * cos angle(p1,p2,p3)* |.p1-p2.| = |.p2-p3.| * cos angle(p3
,p1,p2)* |.p1-p2.|;
p1<>p2 by A3,ZFMISC_1:def 5;
then |.p1-p2.|<>0 by Lm1;
then |.p3-p2.| * cos angle(p1,p2,p3) = |.p2-p3.| * cos angle(p3,p1,p2) by
A4,XCMPLX_1:5;
then
A5: |.p2-p3.| * cos angle(p1,p2,p3) = |.p2-p3.| * cos angle(p3,p1,p2) by Lm2;
p1<>p3 by A3,ZFMISC_1:def 5;
then
A6: |.p3-p1.|<>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
A7: sin angle(p3,p1,p2) = sin angle(p1,p2,p3) by A6,XCMPLX_1:5;
p2<>p3 by A3,ZFMISC_1:def 5;
then |.p2-p3.|<>0 by Lm1;
then cos angle(p1,p2,p3) = cos angle(p3,p1,p2) by A5,XCMPLX_1:5;
hence thesis by A7,Th1;
end;
suppose
A8: not p1,p2,p3 are_mutually_distinct;
per cases by A8,ZFMISC_1:def 5;
suppose
p1=p2;
hence thesis by A2;
end;
suppose
A9: p1=p3;
then |.p2-p3.| = 0 by A1,Lm1;
then p2=p3 by Lm1;
hence thesis by A9;
end;
suppose
A10: p2=p3;
then |.p3-p1.| = 0 by A1,Lm1;
then p3=p1 by Lm1;
hence thesis by A10;
end;
end;
end;
::$L https://en.wikipedia.org/wiki/Isosceles_triangle Isosceles triangle
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 p in LSeg(p2,p1);
then consider l be Real such that
A1: p=(1-l)*p2+l*p1 and
0<=l and
l<=1;
assume
A2: p<>p2;
A3: p2-p = p2-((1-l)*p2)-l*p1 by A1,RLVECT_1:27
.= p2-(1*p2-l*p2)-l*p1 by RLVECT_1:35
.= p2-(p2-l*p2)-l*p1 by RLVECT_1:def 8
.= p2-p2+l*p2-l*p1 by RLVECT_1:29
.= 0.TOP-REAL 2+l*p2-l*p1 by RLVECT_1:5
.= l*p2-l*p1 by RLVECT_1:4
.= l*(p2-p1) by RLVECT_1:34;
hereby
assume
A4: |(p3-p,p2-p1)| = 0;
thus |(p3-p,p2-p)| = l*|(p3-p,p2-p1)| by A3,EUCLID_2:20
.= 0 by A4;
end;
assume |(p3-p,p2-p)| = 0;
then
A5: l*|(p3-p,p2-p1)| = 0 by A3,EUCLID_2:20;
per cases by A5;
suppose
l=0;
then p = 1*p2+0.TOP-REAL 2 by A1,RLVECT_1:10
.= 1*p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8;
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 that
A4: p<>p3 and
A5: p<>p1;
assume
A6: angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI;
per cases;
suppose
A7: p1=p2;
then LSeg(p1,p2) = {p1} by RLTOPSP1:70;
then p=p1 by A3,TARSKI:def 1;
hence thesis by A7;
end;
suppose
A8: p1<>p2;
per cases;
suppose
A9: p<>p2;
p2<>p3
proof
assume
A10: p2=p3;
then |.p3-p1.|=0 by A2,Lm1;
hence contradiction by A8,A10,Lm1;
end;
then
A11: euc2cpx(p2)<> euc2cpx(p3) by EUCLID_3:4;
p1<>p3
proof
assume
A12: p1=p3;
then |.p2-p3.|=0 by A1,Lm1;
hence contradiction by A8,A12,Lm1;
end;
then
A13: euc2cpx(p1)<> euc2cpx(p3) by EUCLID_3:4;
A14: euc2cpx(p)<> euc2cpx(p1) & euc2cpx(p)<> euc2cpx(p3) by A4,A5,EUCLID_3:4;
A15: angle(p1,p,p3) = angle(p3,p,p2) & euc2cpx(p)<> euc2cpx(p2) by A3,A5,A6,A9
,Th14,EUCLID_3:4;
A16: angle(p3,p1,p) = angle(p3,p1,p2) by A3,A5,Th10
.= angle(p1,p2,p3) by A2,A8,Th16
.= angle(p,p2,p3) by A3,A9,Th9;
A17: angle(p,p3,p1)=angle(p2,p3,p)
proof
per cases by A16,A14,A13,A11,A15,COMPLEX2:88;
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
A18: 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;
angle(p2,p3,p)<2*PI & angle(p,p3,p1)>=0 by COMPLEX2:70;
then
A19: angle(p2,p3,p)-angle(p,p3,p1) < 2*PI-0 by XREAL_1:14;
angle(p2,p3,p)-angle(p,p3,p1) = 4*PI by A18;
hence thesis by A19,XREAL_1:64;
end;
suppose
A20: 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;
angle(p,p3,p1)<2*PI & angle(p2,p3,p)>=0 by COMPLEX2:70;
then
A21: angle(p,p3,p1)-angle(p2,p3,p) < 2*PI-0 by XREAL_1:14;
angle(p,p3,p1)-angle(p2,p3,p) = 4*PI by A20;
hence thesis by A21,XREAL_1:64;
end;
end;
per cases;
suppose
A22: angle(p,p3,p1)=0;
then angle(p1,p3,p)=0 by EUCLID_3:36;
hence thesis by A17,A22,EUCLID_3:36;
end;
suppose
A23: angle(p,p3,p1)<>0;
then angle(p1,p3,p)=2*PI-angle(p,p3,p1) by EUCLID_3:37;
hence thesis by A17,A23,EUCLID_3:37;
end;
end;
suppose
A24: 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 A4,A5,A6,EUCLID_3:46;
then |.p1-p.|=0;
hence thesis by A24,Lm1;
end;
end;
end;
:: The Isosceles Triangle Theorem B
::$N Isosceles Triangle Theorem
::$L https://en.wikipedia.org/wiki/Isosceles_triangle Isosceles triangle
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;
thus angle(p1,p3,p)=angle(p,p3,p2) implies |.p1-p.| = |.p-p2.|
proof
assume
A4: angle(p1,p3,p)=angle(p,p3,p2);
A5: |.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 A1,A4
.= |.p2-p.|^2 by Th7;
thus |.p1-p.| = |.p-p1.| by Lm2
.= sqrt |.p2-p.|^2 by A5,SQUARE_1:22
.= |.p2-p.| by SQUARE_1:22
.= |.p-p2.| by Lm2;
end;
thus |.p1-p.| = |.p-p2.| implies |(p3-p,p2-p1)| = 0
proof
assume
A6: |.p1-p.| = |.p-p2.|;
per cases;
suppose
A7: p=p2;
then |.p1-p.| = 0 by A6,Lm1;
hence |(p3-p,p2-p1)| = |(p3-p,p-p)| by A7,Lm1
.= |(p3-p,0.TOP-REAL 2)| by RLVECT_1:5
.= 0 by EUCLID_2:32;
end;
suppose
A8: p<>p2;
then |.p1-p.|<>0 by A6,Lm1;
then
A9: p<>p1 by Lm1;
A10: cos angle(p1,p,p3) = - cos angle(p3,p,p2)
proof
per cases by A2,A8,A9,Th13;
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:79
.= - cos angle(p3,p,p2) by SIN_COS:31;
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:79
.= - cos(-angle(p3,p,p2)) by SIN_COS:79
.= - cos angle(p3,p,p2) by SIN_COS:31;
end;
end;
A11: |.p3-p1.|^2 = |.p1-p.|^2 + |.p3-p.|^2 - 2*|.p1-p.|*|.p3-p.| * cos
angle(p1,p, p3) & |.p2-p3.|^2 = |.p3-p.|^2 + |.p2-p.|^2 - 2*|.p3-p.|*|.p2-p.| *
cos angle( p3,p,p2) by Th7;
A12: |.p1-p.| = |.p2-p.| by A6,Lm2;
A13: |.p2-p.|<>0 by A8,Lm1;
A14: |.p3-p.|<>0 by A3,Lm1;
|.p3-p1.| = |.p2-p3.| by A1,Lm2;
then
2*|.p1-p.|*cos angle(p1,p,p3)*|.p3-p.| = 2*|.p2-p.|*cos angle(p3,
p,p2)*|.p3-p.| by A11,A12;
then 2*cos angle(p1,p,p3)*|.p2-p.|=2*cos angle(p3,p,p2)*|.p2-p.| by A14
,A12,XCMPLX_1:5;
then
A15: 2*cos angle(p1,p,p3)=2*cos angle(p3,p,p2) by A13,XCMPLX_1:5;
0<=angle(p3,p,p2) & angle(p3,p,p2)<2*PI by COMPLEX2:70;
then angle(p3,p,p2)=PI/2 or angle(p3,p,p2)=3/2*PI by A15,A10,
COMPTRIG:18;
then |(p3-p,p2-p)| = 0 by A3,A8,EUCLID_3:45;
hence thesis by A2,A8,Th17;
end;
end;
thus |(p3-p,p2-p1)| = 0 implies angle(p1,p3,p)=angle(p,p3,p2)
proof
assume
A16: |(p3-p,p2-p1)| = 0;
then
A17: 0 = - |(p3-p,p2-p1)| .= |(p3-p,-(p2-p1))| by EUCLID_2:22
.= |(p3-p,p1-p2)| by RLVECT_1:33;
per cases;
suppose
p2=p & p1=p;
hence thesis;
end;
suppose
A18: p1<>p;
then |(p3-p,p1-p)| = 0 by A2,A17,Th17;
then angle(p3,p,p1)=PI/2 or angle(p3,p,p1)=3/2*PI by A3,A18,EUCLID_3:45
;
hence thesis by A1,A2,A3,A18,Th18;
end;
suppose
A19: p2<>p;
then |(p3-p,p2-p)| = 0 by A2,A16,Th17;
then angle(p3,p,p2)=PI/2 or angle(p3,p,p2)=3/2*PI by A3,A19,EUCLID_3:45
;
then
A20: angle(p2,p3,p)=angle(p,p3,p1) by A1,A2,A3,A19,Th18;
per cases;
suppose
A21: angle(p2,p3,p)=0;
then angle(p,p3,p2) = 0 by EUCLID_3:36;
hence thesis by A20,A21,EUCLID_3:36;
end;
suppose
A22: angle(p2,p3,p)<>0;
then angle(p,p3,p2)=2*PI-angle(p2,p3,p) by EUCLID_3:37;
hence thesis by A20,A22,EUCLID_3:37;
end;
end;
end;
end;
definition let V be RealLinearSpace;
::$CD
:: let p1,p2,p3 be Point of V;
:: redefine pred p1,p2,p3 are_collinear means
:: :Def3:
:: p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2);
:: compatibility by TOPREAL9:67;
end;
notation let V be RealLinearSpace;
let p1,p2,p3 be Element of V;
antonym p1,p2,p3 is_a_triangle for p1,p2,p3 are_collinear;
end;
theorem Th20:
p1,p2,p3 is_a_triangle iff p1,p2,p3 are_mutually_distinct &
angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI
proof
hereby
assume
A1: p1,p2,p3 is_a_triangle;
then
A2: not p2 in LSeg(p3,p1) by TOPREAL9:67;
then
A3: p2<>p3 by RLTOPSP1:68;
A4: not p1 in LSeg(p2,p3) by A1,TOPREAL9:67;
then p1<>p2 & p1<>p3 by RLTOPSP1:68;
hence p1,p2,p3 are_mutually_distinct by A3,ZFMISC_1:def 5;
not p3 in LSeg(p1,p2) by A1,TOPREAL9:67;
hence
angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI by A4,A2
,Th11;
end;
assume
A5: p1,p2,p3 are_mutually_distinct;
then
A6: p1<>p2 by ZFMISC_1:def 5;
assume
A7: angle(p1,p2,p3)<>PI;
A8: p1<>p3 by A5,ZFMISC_1:def 5;
A9: p2<>p3 by A5,ZFMISC_1:def 5;
assume angle(p2,p3,p1)<>PI;
then
A10: not p3 in LSeg(p2,p1) by A8,A9,Th8;
assume angle(p3,p1,p2)<>PI;
then
A11: not p1 in LSeg(p3,p2) by A6,A8,Th8;
not p2 in LSeg(p1,p3) by A6,A9,A7,Th8;
hence thesis by A10,A11,TOPREAL9:67;
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 that
A1: p3<>p2 & p3<>p1 and
A2: p2<>p1;
A3: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) by A1,EUCLID_3:4;
A4: euc2cpx(p2)<> euc2cpx(p1) by A2,EUCLID_3:4;
assume that
A5: p5<>p6 and
A6: p5<>p4 and
A7: p6<>p4;
A8: euc2cpx(p5)<> euc2cpx(p6) & euc2cpx(p5)<> euc2cpx(p4) by A5,A6,EUCLID_3:4;
A9: euc2cpx(p6)<> euc2cpx(p4) by A7,EUCLID_3:4;
assume
A10: angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI;
assume
A11: angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI & angle(p6,p4,p5)<>PI;
assume that
A12: angle(p1,p2,p3) = angle(p4,p5,p6) and
A13: angle(p3,p1,p2) = angle(p6,p4,p5);
A14: sin angle(p2,p1,p3)*sin angle(p6,p5,p4) = sin angle(p2,p1,p3)*(-sin
angle(p1,p2,p3)) by A12,Th2
.= (-sin angle(p6,p4,p5))*(-sin angle(p1,p2,p3)) by A13,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
A15: sin angle(p3,p2,p1)*sin angle(p5,p4,p6)<>0;
A16: |.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 A2
,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 A6
,Th6
.= |.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 A15,XCMPLX_1:89
.= ((|.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 A16
.= |.p3-p1.|*|.p6-p5.| by A14,A15,XCMPLX_1:89
.= |.p1-p3.|*|.p6-p5.| by Lm2;
end;
suppose
A17: sin angle(p3,p2,p1)*sin angle(p5,p4,p6)=0;
per cases by A17;
suppose
A18: sin angle(p3,p2,p1) = 0;
A19: 2*PI*0 <= angle(p1,p2,p3) & angle(p1,p2,p3) < 2*PI+2*PI*0 by COMPLEX2:70;
- sin angle(p1,p2,p3) = 0 by A18,Th2;
then angle(p1,p2,p3)=2*PI*0 or angle(p1,p2,p3)=PI+2*PI*0 by A19,
SIN_COS6:21;
hence thesis by A3,A4,A10,COMPLEX2:87;
end;
suppose
A20: sin angle(p5,p4,p6) = 0;
A21: 2*PI*0 <= angle(p6,p4,p5) & angle(p6,p4,p5) < 2*PI+2*PI*0 by COMPLEX2:70;
- sin angle(p6,p4,p5) = 0 by A20,Th2;
then angle(p6,p4,p5)=2*PI*0 or angle(p6,p4,p5)=PI+2*PI*0 by A21,
SIN_COS6:21;
hence thesis by A8,A9,A11,COMPLEX2:87;
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
A1: p1,p2,p3 are_mutually_distinct by Th20;
then
A2: p3<>p2 by ZFMISC_1:def 5;
A3: p2<>p1 by A1,ZFMISC_1:def 5;
then
A4: euc2cpx(p2)<> euc2cpx(p1) by EUCLID_3:4;
A5: p3<>p1 by A1,ZFMISC_1:def 5;
then
A6: euc2cpx(p3)<> euc2cpx(p1) by EUCLID_3:4;
assume
A7: p4,p5,p6 is_a_triangle;
then
A8: angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI by Th20;
A9: p4,p5,p6 are_mutually_distinct by A7,Th20;
then
A10: p5<>p6 by ZFMISC_1:def 5;
then
A11: euc2cpx(p5)<> euc2cpx(p6) by EUCLID_3:4;
A12: p6<>p4 by A9,ZFMISC_1:def 5;
then
A13: euc2cpx(p6)<> euc2cpx(p4) by EUCLID_3:4;
A14: p5<>p4 by A9,ZFMISC_1:def 5;
then
A15: euc2cpx(p5)<> euc2cpx(p4) by EUCLID_3:4;
assume
A16: angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p6,p4, p5);
A17: euc2cpx(p3)<> euc2cpx(p2) by A2,EUCLID_3:4;
A18: angle(p2,p3,p1) = angle(p5,p6,p4)
proof
per cases by A17,A6,A4,A11,A15,A13,COMPLEX2:88;
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 A16;
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 A16;
end;
suppose
A19: 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;
angle(p2,p3,p1)>=0 & -angle(p5,p6,p4) > -2*PI by COMPLEX2:70,XREAL_1:24;
then
A20: angle(p2,p3,p1)+(-angle(p5,p6,p4)) > 0+(-2*PI) by XREAL_1:8;
angle(p2,p3,p1)-angle(p5,p6,p4) = -4*PI by A16,A19;
then 4*PI < 2*PI by A20,XREAL_1:24;
then 4*PI/PI < 2*PI/PI by XREAL_1:74;
then 4 < 2*PI/PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence thesis;
end;
suppose
A21: 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;
angle(p2,p3,p1)<2*PI & angle(p5,p6,p4)>=0 by COMPLEX2:70;
then angle(p2,p3,p1)+(-angle(p5,p6,p4)) < 2*PI+(-0) by XREAL_1:8;
then 4*PI/PI < 2*PI/PI by A16,A21,XREAL_1:74;
then 4 < 2*PI/PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence thesis;
end;
end;
A22: angle(p6,p4,p5)<>PI by A7,Th20;
hence |.p3-p2.|*|.p4-p6.| = |.p1-p3.|*|.p6-p5.| by A2,A5,A3,A8,A10,A14,A12
,A16,A18,Lm18;
thus |.p3-p2.|*|.p5-p4.| = |.p2-p1.|*|.p6-p5.| by A2,A5,A3,A8,A22,A10,A14,A12
,A16,A18,Lm18;
thus thesis by A2,A5,A3,A8,A22,A10,A14,A12,A16,A18,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 that
A1: p3<>p2 & p3<>p1 and
A2: p2<>p1;
A3: euc2cpx(p3)<> euc2cpx(p2) & euc2cpx(p3)<> euc2cpx(p1) by A1,EUCLID_3:4;
A4: euc2cpx(p2)<> euc2cpx(p1) by A2,EUCLID_3:4;
assume that
A5: p4<>p5 & p4<>p6 and
A6: p5<>p6;
A7: euc2cpx(p4)<> euc2cpx(p5) & euc2cpx(p4)<> euc2cpx(p6) by A5,EUCLID_3:4;
A8: euc2cpx(p5)<> euc2cpx(p6) by A6,EUCLID_3:4;
assume
A9: angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI & angle(p3,p1,p2)<>PI;
assume that
A10: angle(p4,p5,p6)<>PI and
A11: angle(p5,p6,p4)<>PI and
A12: angle(p6,p4,p5)<>PI;
assume that
A13: angle(p1,p2,p3) = angle(p4,p5,p6) and
A14: angle(p3,p1,p2) = angle(p5,p6,p4);
A15: sin angle(p1,p2,p3)*sin angle(p4,p6,p5) = sin angle(p4,p5,p6)*(-sin
angle(p5,p6,p4)) by A13,Th2
.= (-sin angle(p6,p5,p4))*(-sin angle(p3,p1,p2)) by A14,Th2
.= sin angle(p6,p5,p4)*sin angle(p3,p1,p2);
per cases;
suppose
A16: sin angle(p1,p2,p3)*sin angle(p4,p6,p5)<>0;
A17: |.p4-p5.|*sin angle(p6,p5,p4)=|.p4-p6.|*sin angle(p4,p6,p5) by A6,Th6;
A18: |.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 A2
,A17,Th6
.= |.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 A16,XCMPLX_1:89
.= ((|.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 A15,A18
.= |.p3-p1.|*|.p4-p5.| by A15,A16,XCMPLX_1:89
.= |.p3-p1.|*|.p5-p4.| by Lm2;
end;
suppose
A19: sin angle(p1,p2,p3)*sin angle(p4,p6,p5)=0;
per cases by A19;
suppose
A20: sin angle(p1,p2,p3) = 0;
2*PI*0 <= angle(p1,p2,p3) & angle(p1,p2,p3) < 2*PI+2*PI*0 by COMPLEX2:70;
then angle(p1,p2,p3)=2*PI*0 or angle(p1,p2,p3)=PI+2*PI*0 by A20,
SIN_COS6:21;
hence thesis by A3,A4,A9,COMPLEX2:87;
end;
suppose
A21: sin angle(p4,p6,p5) = 0;
2*PI*0 <= angle(p4,p6,p5) & angle(p4,p6,p5) < 2*PI+2*PI*0 by COMPLEX2:70;
then angle(p4,p6,p5)=2*PI*0 or angle(p4,p6,p5)=PI+2*PI*0 by A21,
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 A7,A8,A11,COMPLEX2:82,87;
hence thesis by A10,A12,COMPLEX2:82;
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
A1: p1,p2,p3 is_a_triangle;
then
A2: p1,p2,p3 are_mutually_distinct by Th20;
then
A3: p3<>p2 by ZFMISC_1:def 5;
A4: angle(p3,p1,p2)<>PI by A1,Th20;
A5: p3<>p1 by A2,ZFMISC_1:def 5;
then
A6: euc2cpx(p3)<> euc2cpx(p1) by EUCLID_3:4;
A7: p2<>p1 by A2,ZFMISC_1:def 5;
then
A8: euc2cpx(p2)<> euc2cpx(p1) by EUCLID_3:4;
assume
A9: p4,p5,p6 is_a_triangle;
then
A10: p4,p5,p6 are_mutually_distinct by Th20;
then
A11: p4<>p5 by ZFMISC_1:def 5;
then
A12: euc2cpx(p4)<> euc2cpx(p5) by EUCLID_3:4;
A13: p5<>p6 by A10,ZFMISC_1:def 5;
then
A14: euc2cpx(p5)<> euc2cpx(p6) by EUCLID_3:4;
A15: angle(p6,p4,p5)<>PI by A9,Th20;
A16: p4<>p6 by A10,ZFMISC_1:def 5;
then
A17: euc2cpx(p4)<> euc2cpx(p6) by EUCLID_3:4;
assume
A18: angle(p1,p2,p3) = angle(p4,p5,p6) & angle(p3,p1,p2) = angle(p5,p6, p4);
A19: euc2cpx(p3)<> euc2cpx(p2) by A3,EUCLID_3:4;
A20: angle(p2,p3,p1) = angle(p6,p4,p5)
proof
per cases by A19,A6,A8,A12,A17,A14,COMPLEX2:88;
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 A18;
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 A18;
end;
suppose
A21: 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;
angle(p2,p3,p1)>=0 & -angle(p6,p4,p5) > -2*PI by COMPLEX2:70,XREAL_1:24;
then
A22: angle(p2,p3,p1)+(-angle(p6,p4,p5)) > 0+(-2*PI) by XREAL_1:8;
angle(p2,p3,p1)-angle(p6,p4,p5) = -4*PI by A18,A21;
then 4*PI < 2*PI by A22,XREAL_1:24;
then 4*PI/PI < 2*PI/PI by XREAL_1:74;
then 4 < 2*PI/PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence thesis;
end;
suppose
A23: 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;
angle(p2,p3,p1)<2*PI & angle(p6,p4,p5)>=0 by COMPLEX2:70;
then angle(p2,p3,p1)+(-angle(p6,p4,p5)) < 2*PI+(-0) by XREAL_1:8;
then 4*PI/PI < 2*PI/PI by A18,A23,XREAL_1:74;
then 4 < 2*PI/PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence thesis;
end;
end;
angle(p1,p2,p3)<>PI & angle(p2,p3,p1)<>PI by A1,Th20;
hence |.p2-p3.|*|.p4-p6.| = |.p3-p1.|*|.p5-p4.| by A4,A3,A5,A7,A15,A11,A16
,A13,A18,Lm19;
A24: angle(p4,p5,p6)<>PI & angle(p5,p6,p4)<>PI by A9,Th20;
hence |.p2-p3.|*|.p6-p5.| = |.p1-p2.|*|.p5-p4.| by A3,A5,A7,A15,A11,A16,A13
,A18,A20,Lm19;
thus thesis by A3,A5,A7,A24,A15,A11,A16,A13,A18,A20,Lm19;
end;
theorem Th23:
p1,p2,p3 are_mutually_distinct & angle(p1,p2,p3)<=PI implies
angle(p2,p3,p1)<=PI & angle(p3,p1,p2)<=PI
proof
A1: angle(p1,p2,p3)>=0 by COMPLEX2:70;
assume
A2: p1,p2,p3 are_mutually_distinct;
then p1<>p3 by ZFMISC_1:def 5;
then
A3: euc2cpx(p1)<> euc2cpx(p3) by EUCLID_3:4;
p2<>p3 by A2,ZFMISC_1:def 5;
then
A4: euc2cpx(p2)<> euc2cpx(p3) by EUCLID_3:4;
p1<>p2 by A2,ZFMISC_1:def 5;
then euc2cpx(p1)<> euc2cpx(p2) by EUCLID_3:4;
then
A5: 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 A3,A4,COMPLEX2:88;
angle(p2,p3,p1)< 2*PI & angle(p3,p1,p2)<2*PI by COMPLEX2:70;
then
A6: angle(p2,p3,p1)+angle(p3,p1,p2)<2*PI+2*PI by XREAL_1:8;
assume angle(p1,p2,p3)<=PI;
then
A7: angle(p1,p2,p3)+(angle(p2,p3,p1)+angle(p3,p1,p2))<PI+4*PI by A6,XREAL_1:8;
A8: angle(p3,p1,p2)>=0 by COMPLEX2:70;
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 A1,XREAL_1:8;
hence contradiction by A5,A7,A8,XREAL_1:8;
end;
A9: angle(p2,p3,p1)>= 0 by COMPLEX2:70;
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 A9,XREAL_1:8;
hence contradiction by A5,A7,A1,XREAL_1:8;
end;
end;
theorem Th24:
p1,p2,p3 are_mutually_distinct & angle(p1,p2,p3)>PI implies
angle(p2,p3,p1)>PI & angle(p3,p1,p2)>PI
proof
assume
A1: p1,p2,p3 are_mutually_distinct;
then
A2: p1<>p2 & p1<>p3 by ZFMISC_1:def 5;
assume
A3: angle(p1,p2,p3)>PI;
A4: p2<>p3 by A1,ZFMISC_1:def 5;
then p2,p3,p1 are_mutually_distinct by A2,ZFMISC_1:def 5;
hence angle(p2,p3,p1)>PI by A3,Th23;
p3,p1,p2 are_mutually_distinct by A2,A4,ZFMISC_1:def 5;
hence thesis by A3,Th23;
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;
A1: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider
f1=f as Function of TopSpaceMetr(Euclid n),TopSpaceMetr(RealSpace
) by TOPMETR:def 6;
assume
A2: for q being Point of TOP-REAL n holds f.q=|.q-q1.|;
now
let r be Real,u be Element of Euclid n,u1 be Element
of RealSpace;
assume that
A3: r>0 and
A4: 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)<s1 holds dist(u1,w1)<r
proof
let w be Element of Euclid n, w1 be Element of RealSpace;
assume that
A5: w1=f1.w and
A6: dist(u,w)<s1;
reconsider tu=u1,tw=w1 as Real;
reconsider qw=w,qu=u as Point of TOP-REAL n by TOPREAL3:8;
A7: dist(u1,w1)=(the distance of RealSpace).(u1,w1) by METRIC_1:def 1
.= |.tu-tw.| by METRIC_1:def 12,def 13;
A8: tu=|.qu-q1.| by A2,A4;
A9: |.(qu-q1)-(qw-q1).| = |.(qu-q1)-(-q1 + qw).|
.= |.(qu-q1)-(-q1)-qw.| by RLVECT_1:27
.= |.(qu+-q1)+q1-qw.|
.= |.(qu+(q1-q1))-qw.| by RLVECT_1:def 3
.= |.(qu+0.TOP-REAL n)-qw.| by RLVECT_1:5
.= |.qu-qw.| by RLVECT_1:4;
w1=|.qw-q1.| by A2,A5;
then dist(u,w)=|.qu-qw.| & dist(u1,w1)<=|.(qu-q1)-(qw-q1).| by A7,A8,
JGRAPH_1:28,JORDAN2C:9;
hence thesis by A6,A9,XXREAL_0:2;
end;
hence ex s being Real st s>0 & for w being Element of Euclid n, w1
being Element of RealSpace st w1=f1.w & dist(u,w)<s holds dist(u1,w1)<r by A3;
end;
then f1 is continuous by UNIFORM1:3;
hence f is continuous by A1,PRE_TOPC:32,TOPMETR:def 6;
end;
::LIKE JORDAN2C:92
Lm21: 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
proof
let n be Element of NAT;
let q1 be Point of TOP-REAL n;
defpred P[object,object] means
ex q being Point of TOP-REAL n st q=$1 & $2=|.q-q1.|;
A1: for x being object st x in the carrier of TOP-REAL n
ex y being object st P[x,y]
proof
let x be object;
assume x in the carrier of TOP-REAL n;
then reconsider q3=x as Point of TOP-REAL n;
take |.q3-q1.|;
thus thesis;
end;
consider f1 being Function such that
A2: dom f1 = (the carrier of TOP-REAL n) &
for x being object st x in (the
carrier of TOP-REAL n) holds P[x,f1.x] from CLASSES1:sch 1(A1);
rng f1 c= the carrier of R^1
proof
let z be object;
assume z in rng f1;
then consider xz being object such that
A3: xz in dom f1 and
A4: z=f1.xz by FUNCT_1:def 3;
consider q4 being Point of TOP-REAL n such that
A5: q4=xz & f1.xz=|.q4-q1 .| by A2,A3;
f1.xz in REAL by A5,XREAL_0:def 1;
hence thesis by A4,TOPMETR:17;
end;
then reconsider f2=f1 as Function of TOP-REAL n,R^1 by A2,FUNCT_2:def 1
,RELSET_1:4;
A6: for q being Point of TOP-REAL n holds f1.q=|.q-q1.|
proof
let q be Point of TOP-REAL n;
ex q2 be Point of TOP-REAL n st q2=q & f1.q=|.q2-q1.| by A2;
hence thesis;
end;
then f2 is continuous by Lm20;
hence thesis by A6;
end;
theorem Th25:
p in LSeg(p1,p2) & p1,p2,p3 is_a_triangle & angle(p1,p3,p2) =
angle(p,p3,p2) implies p=p1
proof
assume
A1: p in LSeg(p1,p2);
assume
A2: p1,p2,p3 is_a_triangle;
then
A3: angle(p3,p1,p2)<>PI by Th20;
A4: p1,p2,p3 are_mutually_distinct by A2,Th20;
then p1<>p2 by ZFMISC_1:def 5;
then
A5: euc2cpx(p2)<> euc2cpx(p1) by EUCLID_3:4;
A6: not p3 in LSeg(p1,p2) by A2,TOPREAL9:67;
( not p1 in LSeg(p2,p3))& not p2 in LSeg(p3,p1) by A2,TOPREAL9:67;
then
A7: p1,p3,p2 is_a_triangle by A6,TOPREAL9:67;
p2<>p3 by A4,ZFMISC_1:def 5;
then
A8: |.p2-p3.|<>0 by Lm1;
A9: p2<>p3 by A4,ZFMISC_1:def 5;
then
A10: euc2cpx(p3)<> euc2cpx(p2) by EUCLID_3:4;
assume
A11: angle(p1,p3,p2) = angle(p,p3,p2);
angle(p2,p3,p1)<>PI by A2,Th20;
then
A12: angle(p,p3,p2)<>PI by A11,COMPLEX2:82;
A13: p<>p3 by A1,A2,TOPREAL9:67;
then
A14: euc2cpx(p)<> euc2cpx(p3) by EUCLID_3:4;
p1<>p3 by A4,ZFMISC_1:def 5;
then
A15: euc2cpx(p3)<> euc2cpx(p1) by EUCLID_3:4;
A16: angle(p1,p2,p3)<>PI by A2,Th20;
A17: p<>p2
proof
assume p=p2;
then angle(p1,p3,p2)=0 by A11,COMPLEX2:79;
then angle(p3,p2,p1) = 0 & angle(p2,p1,p3) = PI or angle(p3,p2,p1) = PI &
angle(p2,p1,p3) = 0 by A10,A15,A5,COMPLEX2:87;
hence contradiction by A16,A3,COMPLEX2:82;
end;
then
A18: angle(p3,p2,p1) = angle(p3,p2,p) by A1,Th10;
then
A19: angle(p3,p2,p)<>PI by A16,COMPLEX2:82;
A20: p,p3,p2 are_mutually_distinct by A9,A17,A13,ZFMISC_1:def 5;
A21: euc2cpx(p)<> euc2cpx(p2) by A17,EUCLID_3:4;
A22: angle(p2,p1,p3) = angle(p2,p,p3)
proof
per cases by A10,A15,A5,A14,A21,COMPLEX2:88;
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,A18;
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,A18;
end;
suppose
A23: 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;
angle(p2,p1,p3)>=0 & -angle(p2,p,p3) > -2*PI by COMPLEX2:70,XREAL_1:24;
then
A24: angle(p2,p1,p3)+(-angle(p2,p,p3)) > 0+(-2*PI) by XREAL_1:8;
angle(p2,p1,p3)-angle(p2,p,p3) = -4*PI by A11,A18,A23;
then 4*PI < 2*PI by A24,XREAL_1:24;
then 4*PI/PI < 2*PI/PI by XREAL_1:74;
then 4 < 2*PI/PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence thesis;
end;
suppose
A25: 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;
angle(p2,p1,p3)<2*PI & angle(p2,p,p3)>=0 by COMPLEX2:70;
then angle(p2,p1,p3)+(-angle(p2,p,p3)) < 2*PI+(-0) by XREAL_1:8;
then 4*PI/PI < 2*PI/PI by A11,A18,A25,XREAL_1:74;
then 4 < 2*PI/PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence thesis;
end;
end;
then angle(p2,p,p3)<>PI by A3,COMPLEX2:82;
then p,p3,p2 is_a_triangle by A20,A12,A19,Th20;
then |.p2-p3.|*|.p-p2.| = |.p1-p2.|*|.p2-p3.| by A7,A11,A22,Th21;
then |.p-p2.| = |.p1-p2.| by A8,XCMPLX_1:5;
then
A26: |.p2-p.| = |.p1-p2.| by Lm2
.= |.p2-p1.| by Lm2;
assume
A27: p1<>p;
A28: |.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,A27,A17,Th8,
SIN_COS:77;
per cases by A26,A28;
suppose
|.p1-p.|=0;
hence contradiction by A27,Lm1;
end;
suppose
|.p1-p.| + 2*|.p2-p.|=0;
then |.p1-p.|=0;
hence contradiction by A27,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:79;
hence contradiction by A4,COMPLEX2:70;
end;
suppose
A5: p1=p2;
then p in {p2} by A1,RLTOPSP1:70;
hence contradiction by A4,A5,TARSKI:def 1;
end;
suppose
A6: p<>p2 & p1<>p2 & p<>p1;
then
A7: euc2cpx(p)<> euc2cpx(p1) by EUCLID_3:4;
A8: p3<>p1 by A2,RLTOPSP1:68;
then
A9: euc2cpx(p3)<> euc2cpx(p1) by EUCLID_3:4;
A10: euc2cpx(p2)<> euc2cpx(p1) & euc2cpx(p)<> euc2cpx(p2) by A6,EUCLID_3:4;
A11: euc2cpx(p)<> euc2cpx(p3) by A1,A2,EUCLID_3:4;
A12: angle(p3,p2,p1) = angle(p3,p2,p) by A1,A6,Th10;
A13: p3<>p2 by A2,RLTOPSP1:68;
then
A14: euc2cpx(p3)<> euc2cpx(p2) by EUCLID_3:4;
angle(p1,p3,p2)+angle(p2,p1,p3) = angle(p,p3,p2)+angle(p2,p,p3)
proof
per cases by A14,A9,A11,A10,COMPLEX2:88;
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 A12;
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 A12;
end;
suppose
A15: 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;
A16: angle(p1,p3,p2)>=0 & angle(p2,p1,p3)>=0 by COMPLEX2:70;
angle(p2,p,p3)<2*PI by COMPLEX2:70;
then
A17: -angle(p2,p,p3) > -2*PI by XREAL_1:24;
angle(p,p3,p2)<2*PI by COMPLEX2:70;
then -angle(p,p3,p2) > -2*PI by XREAL_1:24;
then -angle(p,p3,p2)+(-angle(p2,p,p3)) > -2*PI+(-2*PI) by A17,XREAL_1:8
;
then angle(p1,p3,p2)+angle(p2,p1,p3)+(-angle(p,p3,p2)-angle(p2,p,p3))
> 0+0+(-2*PI-2*PI) by A16,XREAL_1:8;
hence thesis by A12,A15;
end;
suppose
A18: 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;
angle(p2,p1,p3)<2*PI & angle(p1,p3,p2)<2*PI by COMPLEX2:70;
then
A19: angle(p2,p1,p3)+angle(p1,p3,p2) <2*PI+2*PI by XREAL_1:8;
angle(p,p3,p2)>=0 & angle(p2,p,p3)>=0 by COMPLEX2:70;
then angle(p2,p1,p3)+angle(p1,p3,p2)+(-angle(p,p3,p2)-angle(p2,p,p3))
< 2*PI+2*PI+(0+0) by A19,XREAL_1:8;
hence thesis by A12,A18;
end;
end;
then
A20: angle(p2,p1,p3) > angle(p2,p,p3) by A4,XREAL_1:8;
per cases by A1,A6,A9,A11,A7,Th13,COMPLEX2:88;
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,A20,Th9;
then angle(p1,p3,p) < 0 by XREAL_1:6;
hence contradiction by COMPLEX2:70;
end;
suppose
A21: angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)+angle(p,p1,
p3)+angle(p1,p3,p) = PI;
A22: angle(p,p1,p3)>=0 & angle(p1,p3,p)>=0 by COMPLEX2:70;
angle(p2,p,p3) = angle(p,p1,p3)+angle(p1,p3,p)+2*PI by A21;
then angle(p2,p,p3) >= 0+2*PI by A22,XREAL_1:6;
hence contradiction by COMPLEX2:70;
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:70;
then angle(p,p1,p3)+angle(p1,p3,p) < 2*PI+2*PI by XREAL_1:8;
then angle(p2,p,p3)+4*PI < 0+4*PI by A23;
then angle(p2,p,p3) < 0 by XREAL_1:6;
hence contradiction by COMPLEX2:70;
end;
suppose
A24: 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_distinct by A6,A8,A13,ZFMISC_1:def 5;
then angle(p2,p1,p3) <= PI by A3,Th23;
then
A25: angle(p,p1,p3) <= PI by A1,A6,Th9;
p,p1,p3 are_mutually_distinct by A1,A2,A6,A8,ZFMISC_1:def 5;
then angle(p1,p3,p)<=PI & angle(p3,p,p1)<=PI by A25,Th23;
then angle(p3,p,p1)+angle(p1,p3,p) <= PI+PI by XREAL_1:7;
then angle(p3,p,p1)+angle(p1,p3,p)+angle(p,p1,p3) <= 2*PI+PI by A25,
XREAL_1:7;
hence contradiction by A24,XREAL_1:68;
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,RLTOPSP1:70;
hence contradiction by A5,A6,TARSKI:def 1;
end;
suppose
A7: p1<>p2 & p<>p1;
then
A8: euc2cpx(p2)<> euc2cpx(p1) by EUCLID_3:4;
A9: euc2cpx(p)<> euc2cpx(p2) by A4,EUCLID_3:4;
A10: angle(p3,p2,p1) = angle(p3,p2,p) by A1,A4,Th10;
A11: euc2cpx(p)<> euc2cpx(p1) by A7,EUCLID_3:4;
A12: euc2cpx(p)<> euc2cpx(p3) by A1,A2,EUCLID_3:4;
A13: p3<>p1 by A2,RLTOPSP1:68;
then
A14: euc2cpx(p3)<> euc2cpx(p1) by EUCLID_3:4;
A15: p3<>p2 by A2,RLTOPSP1:68;
then
A16: euc2cpx(p3)<> euc2cpx(p2) by EUCLID_3:4;
angle(p1,p3,p2)+angle(p2,p1,p3) = angle(p,p3,p2)+angle(p2,p,p3)
proof
per cases by A16,A14,A8,A12,A9,COMPLEX2:88;
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
A17: 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;
A18: angle(p1,p3,p2)>=0 & angle(p2,p1,p3)>=0 by COMPLEX2:70;
angle(p2,p,p3)<2*PI by COMPLEX2:70;
then
A19: -angle(p2,p,p3) > -2*PI by XREAL_1:24;
angle(p,p3,p2)<2*PI by COMPLEX2:70;
then -angle(p,p3,p2) > -2*PI by XREAL_1:24;
then -angle(p,p3,p2)+(-angle(p2,p,p3)) > -2*PI+(-2*PI) by A19,XREAL_1:8
;
then angle(p1,p3,p2)+angle(p2,p1,p3)+(-angle(p,p3,p2)-angle(p2,p,p3))
> 0+0+(-2*PI-2*PI) by A18,XREAL_1:8;
hence thesis by A10,A17;
end;
suppose
A20: 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;
angle(p2,p1,p3)<2*PI & angle(p1,p3,p2)<2*PI by COMPLEX2:70;
then
A21: angle(p2,p1,p3)+angle(p1,p3,p2) <2*PI+2*PI by XREAL_1:8;
angle(p,p3,p2)>=0 & angle(p2,p,p3)>=0 by COMPLEX2:70;
then angle(p2,p1,p3)+angle(p1,p3,p2)+(-angle(p,p3,p2)-angle(p2,p,p3))
< 2*PI+2*PI+(0+0) by A21,XREAL_1:8;
hence thesis by A10,A20;
end;
end;
then angle(p2,p1,p3) < angle(p2,p,p3) by A5,XREAL_1:8;
then
A22: angle(p,p1,p3) < angle(p2,p,p3) by A1,Th9;
per cases by A1,A4,A14,A12,A11,Th13,COMPLEX2:88;
suppose
A23: 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_distinct by A7,A13,A15,ZFMISC_1:def 5;
then angle(p2,p1,p3) > PI by A3,Th24;
then
A24: angle(p,p1,p3) > PI by A1,A7,Th9;
p,p1,p3 are_mutually_distinct by A1,A2,A7,A13,ZFMISC_1:def 5;
then angle(p1,p3,p)>PI & angle(p3,p,p1)>PI by A24,Th24;
then angle(p3,p,p1)+angle(p1,p3,p) > PI+PI by XREAL_1:8;
then
A25: angle(p3,p,p1)+angle(p1,p3,p)+angle(p,p1,p3) > 2*PI+PI by A24,XREAL_1:8;
1*PI<3*PI by XREAL_1:68;
hence contradiction by A23,A25;
end;
suppose
A26: angle(p2,p,p3)+angle(p3,p,p1)=3*PI & angle(p3,p,p1)+angle(p,p1,
p3)+angle(p1,p3,p) = PI;
A27: angle(p,p1,p3)>=0 & angle(p1,p3,p)>=0 by COMPLEX2:70;
angle(p2,p,p3) = angle(p,p1,p3)+angle(p1,p3,p)+2*PI by A26;
then angle(p2,p,p3) >= 0+2*PI by A27,XREAL_1:6;
hence contradiction by COMPLEX2:70;
end;
suppose
A28: 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:70;
then angle(p,p1,p3)+angle(p1,p3,p) < 2*PI+2*PI by XREAL_1:8;
then angle(p2,p,p3)+4*PI < 0+4*PI by A28;
then angle(p2,p,p3) < 0 by XREAL_1:6;
hence contradiction by COMPLEX2:70;
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 A22,XREAL_1:6
;
then 2*PI < angle(p1,p3,p) by XREAL_1:6;
hence contradiction by COMPLEX2:70;
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;
set p4=p;
take p4;
thus p4 in LSeg(p1,p2) by A1;
LSeg(p1,p2) = {p1} by A3,RLTOPSP1:70;
then p=p1 by A1,TARSKI:def 1;
hence thesis by A3;
end;
suppose
A4: p=p2 or p1 in LSeg(p2,p3);
set p4=p1;
take p4;
thus p4 in LSeg(p1,p2) by RLTOPSP1:68;
per cases by A4;
suppose
A5: p=p2;
thus angle(p1,p3,p4) = 0 by COMPLEX2:79
.= angle(p,p3,p2) by A5,COMPLEX2:79;
end;
suppose
A6: p1 in LSeg(p2,p3);
p2 in LSeg(p3,p2) by RLTOPSP1:68;
then
A7: LSeg(p1,p2) c= LSeg(p3,p2) by A6,TOPREAL1:6;
thus angle(p1,p3,p4) = 0 by COMPLEX2:79
.= angle(p2,p3,p2) by COMPLEX2:79
.= angle(p,p3,p2) by A1,A2,A7,Th9;
end;
end;
suppose
A8: p=p1 or p2 in LSeg(p1,p3);
set p4=p2;
take p4;
thus p4 in LSeg(p1,p2) by RLTOPSP1:68;
per cases by A8;
suppose
p=p1;
hence thesis;
end;
suppose
A9: p2 in LSeg(p1,p3);
p1 in LSeg(p1,p3) by RLTOPSP1:68;
then LSeg(p1,p2) c= LSeg(p1,p3) by A9,TOPREAL1:6;
hence thesis by A1,A2,Th9;
end;
end;
suppose
A10: p1<>p2 & p<>p1 & p<>p2 & not p1 in LSeg(p2,p3) & not p2 in LSeg( p1,p3);
p1 in LSeg(p1,p2) by RLTOPSP1:68;
then reconsider q1=p1 as Point of (TOP-REAL 2) | LSeg(p1,p2) by PRE_TOPC:8;
A11: 1*(-2) <= cos angle(p,p3,p2)*(-2) by SIN_COS6:6,XREAL_1:65;
consider f1 be Function of TOP-REAL 2, R^1 such that
A12: for q being Point of TOP-REAL 2 holds f1.q=|.q-p1.| and
A13: f1 is continuous by Lm21;
consider f12 be Function of TOP-REAL 2, R^1 such that
A14: for q being Point of TOP-REAL 2,r1,r2 being Real st f1.q=
r1 & f1.q=r2 holds f12.q=r1*r2 and
A15: f12 is continuous by A13,JGRAPH_2:25;
consider f3 be Function of TOP-REAL 2, R^1 such that
A16: for q being Point of TOP-REAL 2 holds f3.q=|.q-p3.| and
A17: f3 is continuous by Lm21;
consider f32 be Function of TOP-REAL 2, R^1 such that
A18: for q being Point of TOP-REAL 2,r1,r2 being Real st f3.q=
r1 & f3.q=r2 holds f32.q=r1*r2 and
A19: f32 is continuous by A17,JGRAPH_2:25;
A20: |.p2-p1.|^2 = |.p1-p3.|^2 + |.p2-p3.|^2 - 2*|.p1-p3.|*|.p2-p3.|* cos
angle(p1,p3,p2) by Th7;
A21: p2<>p3 by A2,RLTOPSP1:68;
then
A22: |.p2-p3.|<>0 by Lm1;
p2 in LSeg(p1,p2) by RLTOPSP1:68;
then reconsider q2=p2 as Point of (TOP-REAL 2) | LSeg(p1,p2) by PRE_TOPC:8;
consider f0 be Function of (TOP-REAL 2) | LSeg(p1,p2),TOP-REAL 2 such that
A23: for q being Point of (TOP-REAL 2) | LSeg(p1,p2) holds f0.q=q and
A24: f0 is continuous by JGRAPH_6:6;
set d = (|.p2-p.|^2 - |.p-p3.|^2 - |.p2-p3.|^2)/(|.p-p3.|*|.p2-p3.|);
consider f2 be Function of TOP-REAL 2, R^1 such that
A25: for q being Point of TOP-REAL 2 holds f2.q=|.p1-p3.| and
A26: f2 is continuous by JGRAPH_2:20;
A27: p1<>p3 by A2,RLTOPSP1:68;
then
A28: |.p1-p3.|<>0 by Lm1;
A29: cos angle(p,p3,p2) <> 1
proof
A30: 0 <= angle(p,p3,p2) & angle(p,p3,p2) < 2*PI by COMPLEX2:70;
assume cos angle(p,p3,p2) = 1;
then
A31: angle(p,p3,p2) = 0 by A30,COMPTRIG:61;
A32: euc2cpx(p)<> euc2cpx(p3) & euc2cpx(p)<> euc2cpx(p2) by A1,A2,A10,
EUCLID_3:4;
A33: euc2cpx(p3)<> euc2cpx(p2) by A21,EUCLID_3:4;
per cases by A31,A32,A33,COMPLEX2:87;
suppose
angle(p3,p2,p) = 0 & angle(p2,p,p3) = PI;
then p in LSeg(p2,p3) by Th11;
hence contradiction by A1,A2,A10,A27,Th12;
end;
suppose
angle(p3,p2,p) = PI & angle(p2,p,p3) = 0;
then angle(p3,p2,p1) = PI by A1,A10,Th10;
hence contradiction by A10,Th11;
end;
end;
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:8;
hence q is Point of TOP-REAL 2;
thus thesis by A35,PRE_TOPC:8;
end;
consider f6 be Function of TOP-REAL 2, R^1 such that
A36: for q being Point of TOP-REAL 2,r1,r2 being Real st f2.q=
r1 & f3.q=r2 holds f6.q=r1*r2 and
A37: f6 is continuous by A26,A17,JGRAPH_2:25;
reconsider f8=f6*f0 as continuous Function of (TOP-REAL 2) | LSeg(p1,p2),
R^1 by A24,A37;
consider f22 be Function of TOP-REAL 2, R^1 such that
A38: for q being Point of TOP-REAL 2,r1,r2 being Real st f2.q=
r1 & f2.q=r2 holds f22.q=r1*r2 and
A39: f22 is continuous by A26,JGRAPH_2:25;
consider f4 be Function of TOP-REAL 2, R^1 such that
A40: for q being Point of TOP-REAL 2,r1,r2 being Real st f12.q=
r1 & f22.q=r2 holds f4.q=r1-r2 and
A41: f4 is continuous by A15,A39,JGRAPH_2:21;
consider f5 be Function of TOP-REAL 2, R^1 such that
A42: for q being Point of TOP-REAL 2,r1,r2 being Real st f4.q=
r1 & f32.q=r2 holds f5.q=r1-r2 and
A43: f5 is continuous by A19,A41,JGRAPH_2:21;
A44: |.p-p3.|<>0 by A1,A2,Lm1;
reconsider f7=f5*f0 as continuous Function of (TOP-REAL 2) | LSeg(p1,p2),
R^1 by A24,A43;
A45: 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;
dom f8 = the carrier of (TOP-REAL 2) | LSeg(p1,p2) by FUNCT_2:def 1;
then
A46: f8.q = f6.(f0.q) by FUNCT_1:12
.= f6.q by A23;
assume
A47: q=q1;
then f6.q = f2.q*f3.q & f2.q = |.p1-p3.| by A25,A36;
hence thesis by A16,A47,A46;
end;
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;
A48: f8.q = |.p1-p3.|*|.q1-p3.| by A45;
assume
A49: f8.q=0;
per cases by A48,A49;
suppose
|.p1-p3.|=0;
hence contradiction by A27,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
A50: for q being Point of (TOP-REAL 2) | LSeg(p1,p2), r1,r2 being Real
st f7.q=r1 & f8.q=r2 holds f9.q=r1/r2 and
A51: f9 is continuous by JGRAPH_2:27;
consider f be Function of I[01], (TOP-REAL 2) | LSeg(p1,p2) such that
A52: for x being Real st x in [.0,1.] holds f.x = (1-x)*p1 + x*p2 and
A53: f is being_homeomorphism and
A54: f.0 = p1 and
A55: f.1 = p2 by A10,JORDAN5A:3;
f is continuous by A53,TOPS_2:def 5;
then reconsider
g=f9*f as continuous Function of Closed-Interval-TSpace(0,1),
R^1 by A51,TOPMETR:20;
A56: dom g = [.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
set b=g.1;
1 in {r where r is Real:0 <= r & r <= 1};
then 1 in dom g by A56,RCOMP_1:def 1;
then
A57: g.1 = f9.p2 by A55,FUNCT_1:12;
|.p2-p.|^2 = |.p-p3.|^2 + |.p2-p3.|^2 - 2*|.p-p3.|*|.p2-p3.|* cos
angle(p,p3,p2) by Th7;
then
A58: 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:74
.= (-2)*cos angle(p,p3,p2) by A22,A44,XCMPLX_1:89;
A59: 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;
A60: q is Point of TOP-REAL 2 by A34;
dom f7 = the carrier of (TOP-REAL 2) | LSeg(p1,p2) by FUNCT_2:def 1;
then
A61: f7.q = f5.(f0.q) by FUNCT_1:12
.= f5.q by A23
.= f4.q-f32.q by A42,A60
.= (f12.q-f22.q)-f32.q by A40,A60
.= f12.q-f22.q-f3.q*f3.q by A18,A60
.= f1.q*f1.q-f22.q-f3.q*f3.q by A14,A60
.= f1.q*f1.q-f2.q*f2.q-f3.q*f3.q by A38,A60;
A62: f9.q = f7.q/f8.q by A50;
assume
A63: q=q1;
then
A64: f3.q=|.q1-p3.| by A16;
f1.q=|.q1-p1.| & f2.q=|.p1-p3.| by A12,A25,A63;
hence thesis by A45,A63,A62,A61,A64;
end;
then f9.q2 = (|.p2-p1.|^2- |.p1-p3.|^2- |.p2-p3.|^2)/(|.p1-p3.|*|.p2-p3.|);
then
A65: f9.q2 = (-2)*(|.p1-p3.|*|.p2-p3.|* cos angle(p1,p3,p2))/(|.p1-p3.|*|.
p2-p3.|) by A20
.= (-2)*((|.p1-p3.|*|.p2-p3.|* cos angle(p1,p3,p2))/(|.p1-p3.|*|.p2-p3
.|)) by XCMPLX_1:74
.= (-2)*cos angle(p1,p3,p2) by A28,A22,XCMPLX_1:89;
A66: d<b
proof
per cases;
suppose
A67: angle(p1,p3,p2) <= PI;
A68: [.0,PI.] /\ (dom cos) = [.0,PI.] by SIN_COS:24,XBOOLE_1:28;
0 <= angle(p1,p3,p2) by COMPLEX2:70;
then
A69: angle(p1,p3,p2) in [.0,PI.] /\ (dom cos) by A67,A68,XXREAL_1:1;
A70: cos.angle(p1,p3,p2) = cos angle(p1,p3,p2) & cos.angle(p,p3,p2) =
cos angle(p,p3,p2) by SIN_COS:def 19;
A71: angle(p,p3,p2) <= angle(p1,p3,p2) by A1,A2,A67,Th26;
then 0 <= angle(p,p3,p2) & angle(p,p3,p2) <= PI by A67,COMPLEX2:70
,XXREAL_0:2;
then
A72: angle(p,p3,p2) in [.0,PI.] /\ (dom cos) by A68,XXREAL_1:1;
p1,p2,p3 is_a_triangle by A2,A10,TOPREAL9:67;
then
A73: angle(p,p3,p2) < angle(p1,p3,p2) by A1,A10,A71,Th25,XXREAL_0:1;
cos| [.2*PI*0,PI+2*PI*0 .] is decreasing by SIN_COS6:55;
then cos.angle(p1,p3,p2) < cos.angle(p,p3,p2) by A73,A72,A69,
RFUNCT_2:21;
hence thesis by A57,A65,A58,A70,XREAL_1:69;
end;
suppose
A74: angle(p1,p3,p2) > PI;
A75: [.PI,2*PI.] /\ (dom cos) = [.PI,2*PI.] by SIN_COS:24,XBOOLE_1:28;
A76: angle(p,p3,p2) <= 2*PI by COMPLEX2:70;
A77: angle(p,p3,p2) >= angle(p1,p3,p2) by A1,A2,A10,A74,Th27;
then PI <= angle(p,p3,p2) by A74,XXREAL_0:2;
then
A78: angle(p,p3,p2) in [.PI,2*PI.] /\ (dom cos) by A75,A76,XXREAL_1:1;
angle(p1,p3,p2) <= 2*PI by COMPLEX2:70;
then
A79: angle(p1,p3,p2) in [.PI,2*PI.] /\ (dom cos) by A74,A75,XXREAL_1:1;
A80: cos.angle(p1,p3,p2) = cos angle(p1,p3,p2) & cos.angle(p,p3,p2) =
cos angle(p,p3,p2) by SIN_COS:def 19;
p1,p2,p3 is_a_triangle by A2,A10,TOPREAL9:67;
then
A81: angle(p,p3,p2) > angle(p1,p3,p2) by A1,A10,A77,Th25,XXREAL_0:1;
cos| [.PI+2*PI*0,2*PI+2*PI*0 .] is increasing by SIN_COS6:56;
then cos.angle(p1,p3,p2) < cos.angle(p,p3,p2) by A81,A78,A79,
RFUNCT_2:20;
hence thesis by A57,A65,A58,A80,XREAL_1:69;
end;
end;
set a=g.0;
0 in {r where r is Real:0 <= r & r <= 1};
then 0 in dom g by A56,RCOMP_1:def 1;
then
A82: g.0 = f9.p1 by A54,FUNCT_1:12;
A83: f9.q1 = (|.p1-p1.|^2- |.p1-p3.|^2- |.p1-p3.|^2)/(|.p1-p3.|*|.p1-p3.|)
by A59
.= (0^2- |.p1-p3.|^2- |.p1-p3.|^2)/(|.p1-p3.|*|.p1-p3.|) by Lm1
.= (-2)*|.p1-p3.|^2/(|.p1-p3.|*|.p1-p3.|)
.= -2 by A28,XCMPLX_1:89;
then a<>d by A82,A58,A29;
then a<d by A82,A83,A58,A11,XXREAL_0:1;
then consider rc be Real such that
A84: g.rc = d and
A85: 0<rc & rc<1 by A66,TOPREAL5:6;
rc in {r where r is Real:0 <= r & r <= 1} by A85;
then
A86: rc in dom g by A56,RCOMP_1:def 1;
then
A87: f.rc = (1-rc)*p1 + rc*p2 by A52,A56;
set p4=(1-rc)*p1 + rc*p2;
take p4;
thus
A88: p4 in LSeg(p1,p2) by A85;
then reconsider q=p4 as Point of (TOP-REAL 2) | LSeg(p1,p2) by PRE_TOPC:8;
A89: |.p4-p3.|<>0 by A2,A88,Lm1;
set r2=|.p1-p3.|*|.p4-p3.|;
A90: |.p4-p1.|^2 = |.p1-p3.|^2 + |.p4-p3.|^2 - 2*|.p1-p3.|*|.p4-p3.|* cos
angle(p1,p3,p4) by Th7;
f9.q = (|.p4-p1.|^2- |.p1-p3.|^2- |.p4-p3.|^2)/ (|.p1-p3.|*|.p4-p3.|)
by A59;
then
A91: d = (-2)*(r2* cos angle(p1,p3,p4))/r2 by A84,A86,A87,A90,FUNCT_1:12
.= (-2)*((r2* cos angle(p1,p3,p4))/r2) by XCMPLX_1:74
.= (-2)*cos angle(p1,p3,p4) by A28,A89,XCMPLX_1:89;
A92: p1<>p4
proof
A93: |.p1-p3.|<>0 by A27,Lm1;
assume
A94: p1=p4;
0 = 0 * |.p1-p1.|
.= 2*|.p1-p3.|*|.p1-p3.| - 2*|.p1-p3.|*|.p1-p3.|*cos angle(p1,p3,p4)
by A90,A94,Lm1;
hence contradiction by A58,A29,A91,A93,XCMPLX_1:7;
end;
A95: p3<>p4 by A2,A85;
per cases;
suppose
A96: angle(p,p3,p2) <= PI;
p,p3,p2 are_mutually_distinct by A1,A2,A10,A21,ZFMISC_1:def 5;
then angle(p3,p2,p) <= PI by A96,Th23;
then
A97: angle(p3,p2,p1) <= PI by A1,A10,Th10;
p3,p2,p1 are_mutually_distinct by A10,A27,A21,ZFMISC_1:def 5;
then angle(p2,p1,p3) <= PI by A97,Th23;
then
A98: angle(p4,p1,p3) <= PI by A88,A92,Th9;
p4,p1,p3 are_mutually_distinct by A27,A92,A95,ZFMISC_1:def 5;
then angle(p1,p3,p4) <= PI by A98,Th23;
hence angle(p1,p3,p4) = arccos cos angle(p1,p3,p4) by COMPLEX2:70
,SIN_COS6:92
.= angle(p,p3,p2) by A58,A91,A96,COMPLEX2:70,SIN_COS6:92;
end;
suppose
A99: angle(p,p3,p2) > PI;
p,p3,p2 are_mutually_distinct by A1,A2,A10,A21,ZFMISC_1:def 5;
then angle(p3,p2,p) > PI by A99,Th24;
then
A100: angle(p3,p2,p1) > PI by A1,A10,Th10;
p3,p2,p1 are_mutually_distinct by A10,A27,A21,ZFMISC_1:def 5;
then angle(p2,p1,p3) > PI by A100,Th24;
then
A101: angle(p4,p1,p3) > PI by A88,A92,Th9;
p4,p1,p3 are_mutually_distinct by A27,A92,A95,ZFMISC_1:def 5;
then angle(p1,p3,p4) > PI by A101,Th24;
then - angle(p1,p3,p4)< -PI by XREAL_1:24;
then
A102: -angle(p1,p3,p4)+2*PI < -PI+2*PI by XREAL_1:6;
A103: cos(2*PI - angle(p1,p3,p4)) = cos.(-angle(p1,p3,p4)+2*PI*1) by
SIN_COS:def 19
.= cos.(-angle(p1,p3,p4)) by SIN_COS6:10
.= cos.(angle(p1,p3,p4)) by SIN_COS:30
.= cos angle(p,p3,p2) by A58,A91,SIN_COS:def 19
.= cos.(angle(p,p3,p2)) by SIN_COS:def 19
.= cos.(-angle(p,p3,p2)) by SIN_COS:30
.= cos.(-angle(p,p3,p2)+2*PI*1) by SIN_COS6:10
.= cos(2*PI-angle(p,p3,p2)) by SIN_COS:def 19;
- angle(p,p3,p2)< -PI by A99,XREAL_1:24;
then
A104: -angle(p,p3,p2)+2*PI < -PI+2*PI by XREAL_1:6;
angle(p,p3,p2) < 2*PI by COMPLEX2:70;
then -angle(p,p3,p2) > -2*PI by XREAL_1:24;
then
A105: -angle(p,p3,p2)+2*PI > -2*PI+2*PI by XREAL_1:6;
angle(p1,p3,p4) < 2*PI by COMPLEX2:70;
then -angle(p1,p3,p4) > -2*PI by XREAL_1:24;
then -angle(p1,p3,p4)+2*PI > -2*PI+2*PI by XREAL_1:6;
then 2*PI - angle(p1,p3,p4) = arccos cos(2*PI-angle(p1,p3,p4)) by A102,
SIN_COS6:92
.= 2*PI - angle(p,p3,p2) by A104,A103,A105,SIN_COS6:92;
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,RLTOPSP1:70;
hence thesis by TARSKI:def 1;
end;
suppose
p1=p4;
then p in {p1} by A5,RLTOPSP1:70;
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 A4,A5,A6,A9,Th12;
suppose
A11: p3 in LSeg(p1,p4);
not p3 in {p1,p4} by A6,A8,TARSKI:def 2;
then
A12: p3 in LSeg(p1,p4) \ {p1,p4} by A11,XBOOLE_0:def 5;
LSeg(p1,p4) \ {p1,p4} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60;
then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A2,A12,
XBOOLE_0:def 4;
hence thesis by A10,XBOOLE_0:def 7;
end;
suppose
A13: p4 in LSeg(p1,p3);
not p4 in {p1,p3} by A6,A8,TARSKI:def 2;
then
A14: p4 in LSeg(p1,p3) \ {p1,p3} by A13,XBOOLE_0:def 5;
LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A2,TOPREAL9:60;
then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A3,A14,
XBOOLE_0:def 4;
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 that
A4: pc = |[a,b]| and
A5: pc in LSeg(p,p2);
assume
A6: p1<>p;
per cases;
suppose
A7: r=0;
then |.p1-pc.|=0 by A1,A4,TOPREAL9:43;
then
A8: p1=pc by Lm1;
A9: |.p2-pc.|=0 by A2,A4,A7,TOPREAL9:43;
then p2=pc by Lm1;
then 2*angle(p1,p,p2) = 2*0 by A8,COMPLEX2:79
.= angle(pc,pc,pc) by COMPLEX2:79;
hence thesis by A9,A8,Lm1;
end;
suppose
A10: r<>0;
|.p2-pc.|=r by A2,A4,TOPREAL9:43;
then
A11: pc<>p2 by A10,Lm1;
A12: euc2cpx(p1)<> euc2cpx(p) by A6,EUCLID_3:4;
A13: |.p1-pc.|=r by A1,A4,TOPREAL9:43;
then pc<>p1 by A10,Lm1;
then
A14: euc2cpx(pc)<> euc2cpx(p1) by EUCLID_3:4;
A15: |.p-pc.|=r by A3,A4,TOPREAL9:43;
then
A16: pc<>p by A10,Lm1;
then
A17: angle(p1,p,p2)=angle(p1,p,pc) by A5,Th10;
|.pc-p1.|=|.p-pc.| by A13,A15,Lm2;
then
A18: angle(pc,p1,p)=angle(p1,p,pc) by A6,Th16;
euc2cpx(pc)<> euc2cpx(p) by A16,EUCLID_3:4;
then
A19: 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 A14,A12,COMPLEX2:88;
per cases by A5,A16,A11,A19,A18,A17,Th13;
suppose
angle(p,pc,p1)+angle(p1,pc,p2)=PI & 2*angle(p1,p,p2)+angle(p,pc ,p1)=PI;
hence thesis;
end;
suppose
A20: angle(p,pc,p1)+angle(p1,pc,p2)=3*PI & 2*angle(p1,p,p2)+angle(p,
pc,p1)=PI;
angle(p1,pc,p2)<2*PI & angle(p1,p,p2)>=0 by COMPLEX2:70;
then -2*angle(p1,p,p2)+angle(p1,pc,p2)<0+2*PI by XREAL_1:8;
hence thesis by A20;
end;
suppose
A21: angle(p,pc,p1)+angle(p1,pc,p2)=PI & 2*angle(p1,p,p2)+angle(p,pc
,p1)=5*PI;
angle(p1,pc,p2)>=0 & angle(p1,p,p2)*2 < (2*PI)*2 by COMPLEX2:70
,XREAL_1:68;
then 2*angle(p1,p,p2)+(-angle(p1,pc,p2))<(2*PI)*2+0 by XREAL_1:8;
hence thesis by A21;
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 RLVECT_1:def 8;
then 1*p1 + 1*p1 = 2*pc -p1 + p1 by RLVECT_1:def 8;
then (1+1)*p1 = 2*pc -p1 +p1 by RLVECT_1:def 6;
then 2*p1 = 2*pc -(p1-p1) by RLVECT_1:29;
then 2*p1 = 2*pc -0.TOP-REAL 2 by RLVECT_1:5;
then 2*p1 = 2*pc + 0.TOP-REAL 2 by RLVECT_1:12;
then 2*p1 = 2*pc by RLVECT_1:4;
then p1 = pc by RLVECT_1:36;
then |. pc - pc .| = r by A1,TOPREAL9:43;
hence contradiction by A3,Lm1;
end;
|. p2 - pc .| = |. 2*pc - p1 - pc .| .= |. 2*pc + -p1 - pc .|
.= |. 2*pc +(-pc) +(-p1) .| by RLVECT_1:def 3
.= |. 2*pc +((-1)*pc) +(-p1) .|
.= |. (2+(-1))*pc +(-p1) .| by RLVECT_1:def 6
.= |. pc - p1 .| by RLVECT_1:def 8
.= 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 RLVECT_1:def 5
.= (1/2)*(p1+(-p1)+2*pc) by RLVECT_1:def 3
.= (1/2)*(0.TOP-REAL 2+2*pc) by RLVECT_1:5
.= (1/2)*(2*pc) by RLVECT_1:4
.= ((1/2)*2)*pc by RLVECT_1:def 7
.= pc by RLVECT_1:def 8;
hence thesis;
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 that
A5: p1<>p and
A6: p2<>p;
per cases;
suppose
A7: r=0;
then |.p1-pc.|=0 by A1,A4,TOPREAL9:43;
then
A8: p1=pc by Lm1;
A9: |.p2-pc.|=0 by A2,A4,A7,TOPREAL9:43;
then p2=pc by Lm1;
then 2*angle(p1,p,p2) = 2*0 by A8,COMPLEX2:79
.= angle(pc,pc,pc) by COMPLEX2:79;
hence thesis by A9,A8,Lm1;
end;
suppose
A10: r<>0;
A11: |.p2-pc.|=r by A2,A4,TOPREAL9:43;
|.p1 - pc.| >= 0;
then r > 0 by A1,A4,A10,TOPREAL9:43;
then consider p3 such that
p<>p3 and
A12: p3 in circle(a,b,r) and
A13: |[a,b]| in LSeg(p,p3) by A3,Th32;
per cases;
suppose
p2=p3;
hence thesis by A1,A3,A4,A5,A12,A13,Th31;
end;
suppose
A14: p2<>p3;
A15: angle(p2,pc,p3)<>0
proof
set z3=euc2cpx(p3-pc);
set z2=euc2cpx(p2-pc);
assume angle(p2,pc,p3)=0;
then
A16: Arg(p2-pc)=Arg(p3-pc) by EUCLID_3:36;
A17: |.p2-pc.|=|.p3-pc.| by A4,A11,A12,TOPREAL9:43;
A18: |.z2.| = |.p2-pc.| by EUCLID_3:25
.= |.z3.| by A17,EUCLID_3:25;
A19: z2 = |.z2.|*cos Arg z2+|.z2.|*sin Arg z2 *<i> by COMPTRIG:62
.= z3 by A16,A18,COMPTRIG:62;
p2 = p2 + 0.TOP-REAL 2 by RLVECT_1:4
.= p2 +(pc+(-pc)) by RLVECT_1:5
.= p2 +(-pc) + pc by RLVECT_1:def 3
.= p3-pc + pc by A19,EUCLID_3:4
.= p3 +(pc+(-pc)) by RLVECT_1:def 3
.= p3 + 0.TOP-REAL 2 by RLVECT_1:5
.= p3 by RLVECT_1:4;
hence contradiction by A14;
end;
2*angle(p2,p,p3) = angle(p2,pc,p3) or 2*(angle(p2,p,p3) - PI) =
angle(p2,pc,p3) by A2,A3,A4,A6,A12,A13,Th31;
then
A20: angle(p2,p,p3)<>0 by A15,COMPLEX2:70;
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 A20,EUCLID_3:37
.= 2*PI -2*(angle(p2,p,p3)-PI)
.= angle(p3,pc,p2) by A15,A22,EUCLID_3:37;
end;
A23: angle(p3,p,p2) = 2*PI-angle(p2,p,p3) by A20,EUCLID_3:37;
A24: 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 A23
.= angle(p3,pc,p2) by A15,EUCLID_3:37;
end;
A25: 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
A26: angle(p1,pc,p2) = angle(p1,pc,p3)+angle(p3,pc,p2);
per cases by A1,A2,A3,A4,A5,A6,A12,A13,A24,A21,Th31;
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 A25,A26;
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 A25,A26;
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 A26;
hence thesis by A25,Lm5;
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 A25,A26;
hence thesis by Lm3;
end;
end;
suppose
A27: angle(p1,pc,p2)+2*PI = angle(p1,pc,p3)+angle(p3,pc,p2);
per cases by A1,A2,A3,A4,A5,A6,A12,A13,A24,A21,Th31;
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 A27;
hence thesis by A25,Lm5;
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,A27;
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 A27;
hence thesis by A25,Lm6;
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 A27;
hence thesis by A25,Lm5;
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);
set pc=|[a,b]|;
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 that
A5: p1<>p3 and
A6: p1<>p4 and
A7: p2<>p3 and
A8: p2<>p4;
per cases by A1,A2,A3,A5,A7,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 A1,A2,A4,A6,A8,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 A1,A2,A4,A6,A8,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 p3 in circle(a,b,r);
then
A3: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,TOPREAL9:60;
assume p1<>p2 & p2<>p3;
then
A4: not p2 in {p1,p3} by TARSKI:def 2;
inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54;
then
A5: inside_of_circle(a,b,r) /\ circle(a,b,r) = {} by XBOOLE_0:def 7;
assume angle(p1,p2,p3)=PI;
then p2 in LSeg(p1,p3) by Th11;
then p2 in LSeg(p1,p3) \ {p1,p3} by A4,XBOOLE_0:def 5;
hence contradiction by A2,A3,A5,XBOOLE_0:def 4;
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 A1,A2,Th30;
then |.p1-p.| = |.0.TOP-REAL 2.| by RLVECT_1:5
.= 0 by EUCLID_2:39;
hence thesis;
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 that
A1: p1 in circle(a,b,r) and
A2: p2 in circle(a,b,r) & p4 in circle(a,b,r);
A3: LSeg(p2,p4) \ {p2,p4} c= inside_of_circle(a,b,r) by A2,TOPREAL9:60;
A4: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54;
assume p in LSeg(p1,p1);
then
A5: p in {p1} by RLTOPSP1:70;
then
A6: |.p1-p.| = |.p-p.| by TARSKI:def 1
.= |.0.TOP-REAL 2.| by RLVECT_1:5
.= |.0*2.| by EUCLID:70
.= 0 by EUCLID:7;
assume p in LSeg(p2,p4);
then
A7: p1 in LSeg(p2,p4) by A5,TARSKI:def 1;
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 A7,XBOOLE_0:def 5;
then p1 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A1,A3,XBOOLE_0:def 4
;
hence thesis by A4,XBOOLE_0:def 7;
end;
suppose
A8: not(p1<>p2 & p1<>p4);
per cases by A8;
suppose
p1=p2;
then |.p2-p.|=|.p1-p1.| by A5,TARSKI:def 1
.= |.0.TOP-REAL 2.| by RLVECT_1:5
.= |.0*2.| by EUCLID:70
.= 0 by EUCLID:7;
hence thesis by A6;
end;
suppose
p1=p4;
then |.p-p4.|=|.p1-p1.| by A5,TARSKI:def 1
.= |.0.TOP-REAL 2.| by RLVECT_1:5
.= |.0*2.| by EUCLID:70
.= 0 by EUCLID:7;
hence thesis by A6;
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_distinct implies angle(p1,p4,p2) = angle(p1,p3,p2)
proof
assume that
A1: p1 in circle(a,b,r) and
A2: p2 in circle(a,b,r) and
A3: p3 in circle(a,b,r) and
A4: p4 in circle(a,b,r);
A5: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60;
assume that
A6: p in LSeg(p1,p3) and
A7: p in LSeg(p2,p4);
assume
A8: p1,p2,p3,p4 are_mutually_distinct;
then
A9: p1<>p2 by ZFMISC_1:def 6;
A10: p3<>p4 by A8,ZFMISC_1:def 6;
A11: p1<>p4 by A8,ZFMISC_1:def 6;
A12: p2<>p4 by A8,ZFMISC_1:def 6;
A13: p1<>p3 by A8,ZFMISC_1:def 6;
A14: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54;
A15: LSeg(p2,p4) \ {p2,p4} c= inside_of_circle(a,b,r) by A2,A4,TOPREAL9:60;
A16: p<>p1 & p<>p4
proof
assume
A17: p=p1 or p=p4;
per cases by A17;
suppose
A18: p=p1;
not p1 in {p2,p4} by A9,A11,TARSKI:def 2;
then p1 in LSeg(p2,p4) \ {p2,p4} by A7,A18,XBOOLE_0:def 5;
then p1 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A1,A15,
XBOOLE_0:def 4;
hence contradiction by A14,XBOOLE_0:def 7;
end;
suppose
A19: p=p4;
not p4 in {p1,p3} by A11,A10,TARSKI:def 2;
then p4 in LSeg(p1,p3) \ {p1,p3} by A6,A19,XBOOLE_0:def 5;
then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A4,A5,
XBOOLE_0:def 4;
hence contradiction by A14,XBOOLE_0:def 7;
end;
end;
then
A20: p1,p4,p are_mutually_distinct by A11,ZFMISC_1:def 5;
A21: p4,p,p1 are_mutually_distinct by A11,A16,ZFMISC_1:def 5;
A22: angle(p1,p4,p) = angle(p1,p4,p2) by A7,A16,Th10;
A23: p2<>p3 by A8,ZFMISC_1:def 6;
A24: p<>p2 & p<>p3
proof
assume
A25: p=p2 or p=p3;
per cases by A25;
suppose
A26: p=p3;
not p3 in {p2,p4} by A23,A10,TARSKI:def 2;
then p3 in LSeg(p2,p4) \ {p2,p4} by A7,A26,XBOOLE_0:def 5;
then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A3,A15,
XBOOLE_0:def 4;
hence contradiction by A14,XBOOLE_0:def 7;
end;
suppose
A27: p=p2;
not p2 in {p1,p3} by A9,A23,TARSKI:def 2;
then p2 in LSeg(p1,p3) \ {p1,p3} by A6,A27,XBOOLE_0:def 5;
then p2 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A2,A5,
XBOOLE_0:def 4;
hence contradiction by A14,XBOOLE_0:def 7;
end;
end;
then
A28: angle(p4,p,p1) = angle(p2,p,p3) by A6,A7,A16,Th15;
A29: p,p3,p2 are_mutually_distinct by A23,A24,ZFMISC_1:def 5;
A30: p2,p,p3 are_mutually_distinct by A23,A24,ZFMISC_1:def 5;
A31: angle(p,p3,p2) = angle(p1,p3,p2) by A6,A24,Th9;
per cases by A1,A2,A3,A4,A13,A11,A23,A12,Th34;
suppose
angle(p1,p4,p2) = angle(p1,p3,p2);
hence thesis;
end;
suppose
A32: angle(p1,p4,p2) = angle(p1,p3,p2) - PI;
angle(p1,p3,p2)<2*PI by COMPLEX2:70;
then angle(p1,p3,p2) - PI < 2*PI -PI by XREAL_1:9;
then angle(p2,p,p3) <= PI by A22,A28,A20,A32,Th23;
then
A33: angle(p1,p3,p2) <= PI by A31,A30,Th23;
A34: not p3 in {p1,p2} by A13,A23,TARSKI:def 2;
angle(p1,p4,p2) >= 0 by COMPLEX2:70;
then angle(p1,p3,p2) - PI + PI >= 0 + PI by A32,XREAL_1:6;
then p3 in LSeg(p1,p2) by A33,Th11,XXREAL_0:1;
then
A35: p3 in LSeg(p1,p2) \ {p1,p2} by A34,XBOOLE_0:def 5;
LSeg(p1,p2) \ {p1,p2} c= inside_of_circle(a,b,r) by A1,A2,TOPREAL9:60;
then
inside_of_circle(a,b,r) misses circle(a,b,r) & p3 in inside_of_circle
(a,b,r) /\ circle(a,b,r) by A3,A35,TOPREAL9:54,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 7;
end;
suppose
A36: angle(p1,p4,p2) = angle(p1,p3,p2) + PI;
angle(p1,p4,p2) < 2*PI by COMPLEX2:70;
then angle(p1,p4,p2) - PI < 2*PI -PI by XREAL_1:9;
then angle(p4,p,p1) <= PI by A31,A28,A29,A36,Th23;
then
A37: angle(p1,p4,p2) <= PI by A22,A21,Th23;
A38: not p4 in {p1,p2} by A11,A12,TARSKI:def 2;
angle(p1,p3,p2) >= 0 by COMPLEX2:70;
then angle(p1,p4,p2) - PI + PI >= 0 + PI by A36,XREAL_1:6;
then p4 in LSeg(p1,p2) by A37,Th11,XXREAL_0:1;
then
A39: p4 in LSeg(p1,p2) \ {p1,p2} by A38,XBOOLE_0:def 5;
LSeg(p1,p2) \ {p1,p2} c= inside_of_circle(a,b,r) by A1,A2,TOPREAL9:60;
then
inside_of_circle(a,b,r) misses circle(a,b,r) & p4 in inside_of_circle
(a,b,r) /\ circle(a,b,r) by A4,A39,TOPREAL9:54,XBOOLE_0:def 4;
hence thesis by 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;
then
A4: euc2cpx(p1)<> euc2cpx(p2) & euc2cpx(p2)<> euc2cpx(p3) by EUCLID_3:4;
assume
A5: p1<>p3;
then euc2cpx(p1)<> euc2cpx(p3) by EUCLID_3:4;
then angle(p2,p3,p1) = 0 & angle(p3,p1,p2) = PI or angle(p2,p3,p1) = PI &
angle(p3,p1,p2) = 0 by A2,A4,COMPLEX2:87;
hence contradiction by A1,A3,A5,Th35;
end;
:: Intersecting Chords Theorem or
:: Product of Segments of Chords
::$N Intersecting chords theorem
::$L https://en.wikipedia.org/wiki/Intersecting_chords_theorem Intersecting chords 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
|.p1-p.|*|.p-p3.| = |.p2-p.|*|.p-p4.|
proof
assume that
A1: p1 in circle(a,b,r) and
A2: p2 in circle(a,b,r) and
A3: p3 in circle(a,b,r) and
A4: p4 in circle(a,b,r);
A5: |.p1-p.| = |.p-p1.| by Lm2;
A6: |.p3-p.| = |.p-p3.| by Lm2;
A7: |.p2-p.| = |.p-p2.| & |.p4-p.| = |.p-p4.| by Lm2;
assume that
A8: p in LSeg(p1,p3) and
A9: p in LSeg(p2,p4);
per cases;
suppose
A10: not p1,p2,p3,p4 are_mutually_distinct;
per cases by A10,ZFMISC_1:def 6;
suppose
p1=p2;
hence thesis by A1,A3,A4,A8,A9,Lm22;
end;
suppose
p1=p3;
hence thesis by A1,A2,A4,A8,A9,Lm23;
end;
suppose
p1=p4;
hence thesis by A1,A2,A3,A8,A9,A7,Lm22;
end;
suppose
p2=p3;
hence thesis by A1,A2,A4,A8,A9,A5,A6,Lm22;
end;
suppose
p2=p4;
hence thesis by A1,A2,A3,A8,A9,Lm23;
end;
suppose
p3=p4;
hence thesis by A1,A2,A3,A8,A9,A5,A7,Lm22;
end;
end;
suppose
A11: p1,p2,p3,p4 are_mutually_distinct;
then
A12: p3<>p4 by ZFMISC_1:def 6;
A13: p1<>p2 by A11,ZFMISC_1:def 6;
A14: p2<>p3 by A11,ZFMISC_1:def 6;
A15: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60;
A16: inside_of_circle(a,b,r) misses circle(a,b,r) by TOPREAL9:54;
A17: LSeg(p2,p4) \ {p2,p4} c= inside_of_circle(a,b,r) by A2,A4,TOPREAL9:60;
A18: p<>p2 & p<>p3
proof
assume
A19: p=p2 or p=p3;
per cases by A19;
suppose
A20: p=p3;
not p3 in {p2,p4} by A14,A12,TARSKI:def 2;
then p3 in LSeg(p2,p4) \ {p2,p4} by A9,A20,XBOOLE_0:def 5;
then p3 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A3,A17,
XBOOLE_0:def 4;
hence contradiction by A16,XBOOLE_0:def 7;
end;
suppose
A21: p=p2;
not p2 in {p1,p3} by A13,A14,TARSKI:def 2;
then p2 in LSeg(p1,p3) \ {p1,p3} by A8,A21,XBOOLE_0:def 5;
then p2 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A2,A15,
XBOOLE_0:def 4;
hence contradiction by A16,XBOOLE_0:def 7;
end;
end;
then
A22: p2,p,p3 are_mutually_distinct by A14,ZFMISC_1:def 5;
A23: p1<>p4 by A11,ZFMISC_1:def 6;
A24: p<>p1 & p<>p4
proof
assume
A25: p=p1 or p=p4;
per cases by A25;
suppose
A26: p=p1;
not p1 in {p2,p4} by A13,A23,TARSKI:def 2;
then p1 in LSeg(p2,p4) \ {p2,p4} by A9,A26,XBOOLE_0:def 5;
then p1 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A1,A17,
XBOOLE_0:def 4;
hence contradiction by A16,XBOOLE_0:def 7;
end;
suppose
A27: p=p4;
not p4 in {p1,p3} by A23,A12,TARSKI:def 2;
then p4 in LSeg(p1,p3) \ {p1,p3} by A8,A27,XBOOLE_0:def 5;
then p4 in inside_of_circle(a,b,r) /\ circle(a,b,r) by A4,A15,
XBOOLE_0:def 4;
hence contradiction by A16,XBOOLE_0:def 7;
end;
end;
then
A28: angle(p4,p,p1) = angle(p2,p,p3) by A8,A9,A18,Th15;
A29: p2<>p4 by A11,ZFMISC_1:def 6;
A30: angle(p3,p2,p)<>PI
proof
assume angle(p3,p2,p)=PI;
then angle(p3,p2,p4)=PI by A9,A18,Th10;
hence contradiction by A2,A3,A4,A14,A29,Th35;
end;
A31: p1<>p3 by A11,ZFMISC_1:def 6;
A32: angle(p,p3,p2)<>PI
proof
assume angle(p,p3,p2)=PI;
then angle(p1,p3,p2)=PI by A8,A18,Th9;
hence contradiction by A1,A2,A3,A31,A14,Th35;
end;
A33: angle(p,p1,p4)<>PI
proof
assume angle(p,p1,p4)=PI;
then angle(p3,p1,p4)=PI by A8,A24,Th9;
hence contradiction by A1,A3,A4,A31,A23,Th35;
end;
A34: angle(p,p3,p2) = angle(p1,p3,p2) by A8,A18,Th9;
A35: angle(p1,p4,p) = angle(p1,p4,p2) by A9,A24,Th10;
A36: angle(p4,p,p1)<>PI
proof
assume angle(p4,p,p1)=PI;
then p in LSeg(p1,p4) by Th11;
hence contradiction by A1,A2,A4,A9,A13,A24,Th30;
end;
then angle(p2,p,p3)<>PI by A8,A9,A24,A18,Th15;
then
A37: p2,p,p3 is_a_triangle by A22,A32,A30,Th20;
A38: angle(p1,p4,p)<>PI
proof
assume angle(p1,p4,p)=PI;
then angle(p1,p4,p2)=PI by A9,A24,Th10;
hence contradiction by A1,A2,A4,A23,A29,Th35;
end;
p4,p,p1 are_mutually_distinct by A23,A24,ZFMISC_1:def 5;
then
A39: p4,p,p1 is_a_triangle by A36,A33,A38,Th20;
angle(p1,p4,p2) = angle(p1,p3,p2) by A1,A2,A3,A4,A8,A9,A11,Th36;
hence thesis by A5,A6,A7,A35,A34,A28,A39,A37,Th22;
end;
end;
begin :: Heron's Formula and Ptolemy's Theorem
::$N Heron's Formula
::$L https://en.wikipedia.org/wiki/Heron's_formula Heron's Formula
theorem
a = |.p2-p1.| & b = |.p3-p2.| & c = |.p1-p3.| & s =
the_perimeter_of_polygon3(p1,p2,p3)/2 implies
|.the_area_of_polygon3(p1,p2,p3).| = sqrt(s*(s-a)*(s-b)*(s-c))
proof
assume that
A1: a = |.p2-p1.| and
A2: b = |.p3-p2.| and
A3: c = |.p1-p3.|;
A4: a = |.p1-p2.| by A1,Lm2;
c = |.p3-p1.| by A3,Lm2;
then
A5: c^2 = a^2 + b^2 - 2*a*b* cos angle(p1,p2,p3) by A2,A4,Th7;
assume
A6: s = the_perimeter_of_polygon3(p1,p2,p3)/2;
A7: (sin angle(p3,p2,p1))^2+(cos angle(p3,p2,p1))^2=1 by SIN_COS:29;
the_area_of_polygon3(p1,p2,p3)^2 = (a*b*sin angle(p3,p2,p1)/2)^2 by A2,A4,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 A7,SQUARE_1:9
.= (((a*b)^2-(a*b)^2*(cos angle(p3,p2,p1))^2))*2^2/2^2*(1/2)^2 by
XCMPLX_1:89
.= (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 A5,Th3
.= 16*(s-a)*(s-b)*((s-c)*s)/(2*2)*(1/2)^2 by A1,A2,A3,A6
.= s*(s-a)*(s-b)*(s-c);
hence thesis by COMPLEX1:72;
end;
::$N Ptolemy's Theorem
::$L https://en.wikipedia.org/wiki/Ptolemy's_theorem 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 that
A1: p1 in circle(a,b,r) and
A2: p2 in circle(a,b,r) and
A3: p3 in circle(a,b,r) and
A4: p4 in circle(a,b,r);
A5: |.p3-p1.| = |.p1-p3.| by Lm2;
assume that
A6: p in LSeg(p1,p3) and
A7: p in LSeg(p2,p4);
per cases;
suppose
A8: not p1,p2,p3,p4 are_mutually_distinct;
per cases by A8,ZFMISC_1:def 6;
suppose
A9: p1=p2;
then |.p2-p1.| = 0 by Lm1;
hence thesis by A9;
end;
suppose
p1=p3;
then
A10: p in {p1} by A6,RLTOPSP1:70;
then p in circle(a,b,r) by A1,TARSKI:def 1;
then p in LSeg(p2,p4) /\ circle(a,b,r) by A7,XBOOLE_0:def 4;
then p in {p2,p4} by A2,A4,TOPREAL9:61;
then
A11: p = p2 or p = p4 by TARSKI:def 2;
per cases by A10,A11,TARSKI:def 1;
suppose
A12: p1 = p2;
then |.p2-p1.| = 0 by Lm1;
hence thesis by A12;
end;
suppose
A13: p1 = p4;
then |.p4-p1.| = 0 by Lm1;
hence thesis by A5,A13,Lm2;
end;
end;
suppose
A14: p1=p4;
then |.p4-p1.| = 0 by Lm1;
hence thesis by A5,A14,Lm2;
end;
suppose
A15: p2=p3;
then |.p3-p2.| = 0 by Lm1;
hence thesis by A15;
end;
suppose
p2=p4;
then
A16: p in {p2} by A7,RLTOPSP1:70;
then p in circle(a,b,r) by A2,TARSKI:def 1;
then p in LSeg(p1,p3) /\ circle(a,b,r) by A6,XBOOLE_0:def 4;
then p in {p1,p3} by A1,A3,TOPREAL9:61;
then
A17: p = p1 or p = p3 by TARSKI:def 2;
per cases by A16,A17,TARSKI:def 1;
suppose
A18: p1 = p2;
then |.p2-p1.| = 0 by Lm1;
hence thesis by A18;
end;
suppose
A19: p2 = p3;
then |.p3-p2.| = 0 by Lm1;
hence thesis by A19;
end;
end;
suppose
A20: p3=p4;
then |.p4-p3.| = 0 by Lm1;
hence thesis by A20;
end;
end;
suppose
A21: p1,p2,p3,p4 are_mutually_distinct;
then
A22: p3<>p4 by ZFMISC_1:def 6;
then
A23: euc2cpx(p3)<> euc2cpx(p4) by EUCLID_3:4;
A24: p2<>p4 by A21,ZFMISC_1:def 6;
then
A25: angle(p3,p4,p2)<>PI by A2,A3,A4,A22,Th35;
A26: p1<>p2 by A21,ZFMISC_1:def 6;
then
A27: angle(p1,p2,p4)<>PI by A1,A2,A4,A24,Th35;
A28: p1<>p4 by A21,ZFMISC_1:def 6;
then
A29: angle(p4,p1,p2)<>PI by A1,A2,A4,A26,Th35;
A30: angle(p2,p4,p1)<>PI by A1,A2,A4,A28,A24,Th35;
p2,p4,p1 are_mutually_distinct by A26,A28,A24,ZFMISC_1:def 5;
then
A31: p2,p4,p1 is_a_triangle by A30,A29,A27,Th20;
A32: p2<>p3 by A21,ZFMISC_1:def 6;
then
A33: euc2cpx(p2)<> euc2cpx(p3) by EUCLID_3:4;
A34: angle(p2,p3,p4)<>PI by A2,A3,A4,A32,A22,Th35;
A35: not p2 in LSeg(p1,p3)
proof
assume
A36: p2 in LSeg(p1,p3);
not p2 in {p1,p3} by A26,A32,TARSKI:def 2;
then
A37: p2 in LSeg(p1,p3) \ {p1,p3} by A36,XBOOLE_0:def 5;
LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60;
then inside_of_circle(a,b,r) misses circle(a,b,r) & p2 in
inside_of_circle(a,b,r) /\ circle(a,b,r) by A2,A37,TOPREAL9:54,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7;
end;
then consider p5 such that
A38: p5 in LSeg(p1,p3) and
A39: angle(p1,p2,p5) = angle(p,p2,p3) by A6,Th28;
A40: angle(p4,p2,p3)<>PI by A2,A3,A4,A32,A24,Th35;
then
A41: angle(p1,p2,p5)<>PI by A6,A7,A35,A39,Th9;
A42: euc2cpx(p2)<> euc2cpx(p4) by A24,EUCLID_3:4;
A43: p5<>p1
proof
assume p5=p1;
then angle(p4,p2,p3) = angle(p1,p2,p1) by A6,A7,A35,A39,Th9
.= 0 by COMPLEX2:79;
hence contradiction by A34,A25,A33,A42,A23,COMPLEX2:87;
end;
A44: p5<>p3
proof
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
A45: angle(p4,p2,p3) + angle(p3,p2,p4) = 0 or angle(p4,p2,p3) + angle(p3
,p2,p4) = 0 + 2*PI by COMPLEX2:79;
assume p5=p3;
then
A46: angle(p4,p2,p3) = angle(p1,p2,p3) by A6,A7,A35,A39,Th9;
per cases by A45,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 A1,A2,A4,A26,A28,A24,A46,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 A46,COMPLEX2:70;
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 A46;
hence contradiction by COMPLEX2:70;
end;
end;
A47: angle(p,p2,p3) = angle(p4,p2,p3) by A6,A7,A35,Th9;
A48: angle(p5,p2,p3) = angle(p1,p2,p4)
proof
per cases by A47,A39,Th4;
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
A49: 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 by COMPLEX2:70;
then angle(p5,p2,p3)+2*PI>=0+2*PI by XREAL_1:6;
hence thesis by A49,COMPLEX2:70;
end;
suppose
A50: 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(p1,p2,p4)>=0 by COMPLEX2:70;
then angle(p1,p2,p4)+2*PI>=0+2*PI by XREAL_1:6;
hence thesis by A50,COMPLEX2:70;
end;
end;
A51: p5<>p2
proof
A52: LSeg(p1,p3) \ {p1,p3} c= inside_of_circle(a,b,r) by A1,A3,TOPREAL9:60;
assume
A53: p5=p2;
not p2 in {p1,p3} by A26,A32,TARSKI:def 2;
then p2 in LSeg(p1,p3) \ {p1,p3} by A38,A53,XBOOLE_0:def 5;
then inside_of_circle(a,b,r) misses circle(a,b,r) & p2 in
inside_of_circle(a,b,r) /\ circle(a,b,r) by A2,A52,TOPREAL9:54,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7;
end;
then
A54: p1,p2,p5 are_mutually_distinct by A26,A43,ZFMISC_1:def 5;
p1<>p3 by A21,ZFMISC_1:def 6;
then p2,p3,p4,p1 are_mutually_distinct by A26,A28,A32,A24,A22,
ZFMISC_1:def 6;
then
A55: angle(p2,p1,p3) = angle(p2,p4,p3) by A1,A2,A3,A4,A6,A7,Th36;
A56: angle(p3,p1,p2) = angle(p3,p4,p2)
proof
per cases;
suppose
A57: angle(p2,p1,p3)=0;
then angle(p3,p1,p2)=0 by EUCLID_3:36;
hence thesis by A55,A57,EUCLID_3:36;
end;
suppose
A58: angle(p2,p1,p3)<>0;
then angle(p3,p1,p2)=2*PI-angle(p2,p1,p3) by EUCLID_3:37;
hence thesis by A55,A58,EUCLID_3:37;
end;
end;
then
A59: angle(p5,p1,p2) = angle(p3,p4,p2) by A38,A43,Th9;
A60: angle(p2,p3,p4) = angle(p2,p5,p1)
proof
A61: euc2cpx(p2)<> euc2cpx(p5) & euc2cpx(p2)<> euc2cpx(p1) by A26,A51,
EUCLID_3:4;
A62: euc2cpx(p5)<> euc2cpx(p1) by A43,EUCLID_3:4;
per cases by A33,A42,A23,A61,A62,COMPLEX2:88;
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 A47,A39,A59;
end;
suppose
A63: 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;
angle(p2,p3,p4)<2*PI & angle(p2,p5,p1)>=0 by COMPLEX2:70;
then
A64: angle(p2,p3,p4)-angle(p2,p5,p1) < 2*PI-0 by XREAL_1:14;
angle(p2,p3,p4)-angle(p2,p5,p1) = 4*PI by A47,A39,A59,A63;
hence thesis by A64,XREAL_1:64;
end;
suppose
A65: 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;
angle(p2,p5,p1)<2*PI & angle(p2,p3,p4)>=0 by COMPLEX2:70;
then
A66: angle(p2,p5,p1)-angle(p2,p3,p4) < 2*PI-0 by XREAL_1:14;
angle(p2,p5,p1)-angle(p2,p3,p4) = 4*PI by A47,A39,A59,A65;
hence thesis by A66,XREAL_1:64;
end;
end;
A67: angle(p1,p4,p2) = angle(p1,p3,p2) by A1,A2,A3,A4,A6,A7,A21,Th36;
angle(p2,p4,p1) = angle(p2,p3,p1)
proof
per cases;
suppose
A68: angle(p1,p4,p2)=0;
then angle(p2,p4,p1)=0 by EUCLID_3:36;
hence thesis by A67,A68,EUCLID_3:36;
end;
suppose
A69: angle(p1,p4,p2)<>0;
then angle(p2,p4,p1)=2*PI-angle(p1,p4,p2) by EUCLID_3:37;
hence thesis by A67,A69,EUCLID_3:37;
end;
end;
then
A70: angle(p2,p4,p1) = angle(p2,p3,p5) by A38,A44,Th10;
A71: angle(p4,p1,p2) = angle(p3,p5,p2)
proof
A72: euc2cpx(p2)<> euc2cpx(p5) & euc2cpx(p3)<> euc2cpx(p5) by A44,A51,
EUCLID_3:4;
A73: euc2cpx(p4)<> euc2cpx(p1) & euc2cpx(p2)<> euc2cpx(p3) by A28,A32,
EUCLID_3:4;
A74: euc2cpx(p2)<> euc2cpx(p4) & euc2cpx(p2)<> euc2cpx(p1) by A26,A24,
EUCLID_3:4;
per cases by A74,A73,A72,COMPLEX2:88;
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 A70,A48;
end;
suppose
A75: 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;
angle(p4,p1,p2)<2*PI & angle(p3,p5,p2)>=0 by COMPLEX2:70;
then
A76: angle(p4,p1,p2)-angle(p3,p5,p2) < 2*PI-0 by XREAL_1:14;
angle(p4,p1,p2)-angle(p3,p5,p2) = 4*PI by A70,A48,A75;
hence thesis by A76,XREAL_1:64;
end;
suppose
A77: 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;
angle(p3,p5,p2)<2*PI & angle(p4,p1,p2)>=0 by COMPLEX2:70;
then
A78: angle(p3,p5,p2)-angle(p4,p1,p2) < 2*PI-0 by XREAL_1:14;
angle(p3,p5,p2)-angle(p4,p1,p2) = 4*PI by A70,A48,A77;
hence thesis by A78,XREAL_1:64;
end;
end;
p2,p3,p5 are_mutually_distinct by A32,A44,A51,ZFMISC_1:def 5;
then p2,p3,p5 is_a_triangle by A70,A48,A71,A30,A29,A27,Th20;
then |.p5-p3.|*|.p4-p2.| = |.p3-p2.|*|.p1-p4.| by A70,A48,A31,Th21;
then |.p5-p3.|*|.p4-p2.| = |.p3-p2.|*|.p4-p1.| by Lm2;
then
A79: |.p3-p5.|*|.p4-p2.| = |.p3-p2.|*|.p4-p1.| by Lm2;
p4,p2,p3 are_mutually_distinct by A32,A24,A22,ZFMISC_1:def 5;
then
A80: p4,p2,p3 is_a_triangle by A40,A34,A25,Th20;
A81: |.p3-p1.| = sqrt |.p3-p1.|^2 by SQUARE_1:22
.= 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 A38
,A43,A44,Th8
.= sqrt (|.p1-p5.| + |.p3-p5.|)^2 by SIN_COS:77
.= |.p1-p5.| + |.p3-p5.| by SQUARE_1:22;
angle(p5,p1,p2)<>PI by A2,A3,A4,A24,A22,A38,A43,A56,Th9,Th35;
then p1,p2,p5 is_a_triangle by A34,A60,A41,A54,Th20;
then |.p1-p5.|*|.p2-p4.| = |.p2-p1.|*|.p4-p3.| by A47,A39,A59,A80,Th21;
then |.p1-p5.|*|.p4-p2.| = |.p2-p1.|*|.p4-p3.| by Lm2;
hence |.p2-p1.|*|.p4-p3.| + |.p3-p2.|*|.p4-p1.| = |.p5-p1.|*|.p4-p2.| + |.
p3-p5.|*|.p4-p2.| by A79,Lm2
.= (|.p5-p1.| + |.p3-p5.|)*|.p4-p2.|
.= |.p3-p1.|*|.p4-p2.| by A81,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;