:: Circumcenter, Circumcircle, and Centroid of a Triangle
:: by Roland Coghetto
::
:: Received December 30, 2015
:: Copyright (c) 2015-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, NAT_1, SUBSET_1, COMPLEX1, REAL_1, RELAT_1, TARSKI,
CARD_1, ARYTM_1, ARYTM_3, RVSUM_1, SQUARE_1, XXREAL_0, ZFMISC_1,
XBOOLE_0, RLTOPSP1, PRE_TOPC, MCART_1, EUCLID, INCSP_1, PROJRED2, AFF_1,
ANALOAF, EUCLID_3, SYMSP_1, EUCLIDLP, METRIC_1, JGRAPH_6, SIN_COS,
COMPLEX2, XXREAL_1, PROJPL_1, EUCLID10, EUCLID12, RUSUB_5, GTARSKI1,
SUPINF_2, PENCIL_1;
notations INT_1, EUCLIDLP, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0,
NUMBERS, XREAL_0, COMPLEX1, ORDINAL1, METRIC_1, STRUCT_0, FINSEQ_2,
SQUARE_1, RVSUM_1, PRE_TOPC, XXREAL_0, RLVECT_1, RLTOPSP1, EUCLID,
EUCLID_4, JGRAPH_6, SIN_COS, COMPLEX2, EUCLID_3, EUCLID_6, RCOMP_1,
EUCLID10, MENELAUS, TOPREAL6, GTARSKI1;
constructors SQUARE_1, EUCLID_4, EUCLIDLP, COMPLEX1, JGRAPH_6, MONOID_0,
SIN_COS, EUCLID_3, EUCLID10, INTEGRA1, MENELAUS, TOPREAL6, GTARSKI1,
COMPLEX2, COMPTRIG;
registrations INT_1, MONOID_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, EUCLID,
VALUED_0, SQUARE_1, ORDINAL1, EUCLIDLP, SIN_COS, EUCLID10;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI;
equalities EUCLID, EUCLID_4, VALUED_1, XCMPLX_0;
expansions TARSKI, EUCLID_4, XBOOLE_0, ZFMISC_1, GTARSKI1;
theorems EUCLID11, ABSVALUE, SQUARE_1, XBOOLE_0, XCMPLX_1, RVSUM_1, EUCLID_4,
XREAL_1, EUCLIDLP, TARSKI, RLVECT_1, EUCLID, TOPRNS_1, RLTOPSP1,
EUCLID_3, EUCLID_6, MENELAUS, SIN_COS, XXREAL_1, EUCLID10, ZFMISC_1,
JGRAPH_6, COMPTRIG, JORDAN1K, SPPOL_1, TOPREAL6, METRIC_1, TOPREAL9,
COMPLEX1, SIN_COS6;
begin :: Preliminaries
reserve n for Nat,
lambda,lambda2,mu,mu2 for Real,
x1,x2 for Element of REAL n,
An,Bn,Cn for Point of TOP-REAL n,
a for Real;
Lm1:
(1-lambda) * x1 = x1 - lambda * x1
proof
(1-lambda) * x1 = 1 * x1 - lambda * x1 by EUCLIDLP:11
.= x1 - lambda * x1 by RVSUM_1:52;
hence thesis;
end;
Lm2:
sin (a-PI) = - sin a
proof
sin (a- PI) = sin (-(PI - a))
.= - sin (PI - a) by SIN_COS:31;
hence thesis by EUCLID10:1;
end;
theorem Th1:
An = (1-lambda) * x1 + lambda * x2 & Bn = (1-mu) * x1 + mu * x2
implies Bn - An = (mu-lambda)*(x2-x1)
proof
assume that
A1: An = (1-lambda) * x1 + lambda * x2 and
A2: Bn = (1-mu) * x1 + mu * x2;
A3: (1-lambda) * x1 = x1 - lambda * x1 by Lm1;
Bn - An = (1-mu) * x1 + mu * x2 - (1-lambda)* x1 - lambda*x2
by A1,A2,RVSUM_1:39
.= x1 -mu * x1 + mu * x2 - (x1 -lambda * x1) - lambda * x2
by A3,Lm1
.= x1 -mu * x1 + mu * x2 - x1 + lambda * x1 - lambda * x2
by RVSUM_1:41
.= x1 - (mu * x1 - mu * x2) + -x1 + lambda * x1 - lambda * x2
by RVSUM_1:41
.= -(mu * x1 - mu * x2) + x1 - x1 + lambda * x1 - lambda * x2
.= -(mu * x1 - mu * x2) + lambda * x1 - lambda * x2 by RVSUM_1:42
.= mu * x2 - mu*x1 + lambda * x1 - lambda *x2 by RVSUM_1:35
.= mu * x2 + (- mu * x1 + lambda * x1) +- lambda *x2 by RVSUM_1:15
.= mu * x2 + ((-1)* mu * x1 + lambda * x1) +- lambda *x2
by RVSUM_1:49
.= mu * x2 + (- mu +lambda) * x1 +- lambda *x2 by RVSUM_1:50
.= (- mu + lambda) * x1 + (mu*x2 + -lambda *x2) by RVSUM_1:15
.= (-(mu-lambda))*x1 +(mu-lambda)*x2 by EUCLIDLP:11
.= (mu-lambda)*(x2-x1) by EUCLIDLP:12;
hence thesis;
end;
theorem Th2:
|.a.| = |.1-a.| implies a = 1/2
proof
assume
A1: |.a.| = |.1-a.|;
|.a.|^2 = a^2 & |.1-a.|^2 = (1-a)^2 by COMPLEX1:75;
then a^2 = (1-a) * (1-a) by A1,SQUARE_1:def 1
.= 1 - 2*a + a*a
.= 1 - 2*a + a^2 by SQUARE_1:def 1;
hence thesis;
end;
reserve Pn,PAn,PBn for Element of REAL n,
Ln for Element of line_of_REAL n;
theorem Th3:
Line(Pn,Pn)={Pn}
proof
now
hereby
let x be object;
assume x in Line(Pn,Pn);
then consider lambda be Real such that
A1: x = (1-lambda) * Pn + lambda * Pn;
x = ((1 - lambda)+ lambda) * Pn by A1,EUCLID_4:7
.= Pn by EUCLID_4:3;
hence x in {Pn} by TARSKI:def 1;
end;
let x be object;
assume x in {Pn};
then x = Pn by TARSKI:def 1;
hence x in Line(Pn,Pn) by EUCLID_4:9;
end;
then Line(Pn,Pn) c= {Pn} & {Pn} c= Line(Pn,Pn);
hence thesis;
end;
theorem Th4:
An=PAn & Bn=PBn implies Line(An,Bn)=Line(PAn,PBn)
proof
assume
A1: An=PAn & Bn=PBn;
now
hereby
let x be object;
assume x in Line(An,Bn);
then x in the set of all (1-lambda)*An + lambda*Bn
where lambda is Real by RLTOPSP1:def 14;
then consider l0 be Real such that
A2: x = (1-l0)*An+l0*Bn;
thus x in Line(PAn,PBn) by A1,A2;
end;
let x be object;
assume x in Line(PAn,PBn);
then consider l0 be Real such that
A3: x = (1-l0)*PAn+l0*PBn;
x = (1-l0)*An+l0*Bn by A1,A3;
then x in the set of all (1-lambda)*An + lambda*Bn where lambda is Real;
hence x in Line(An,Bn) by RLTOPSP1:def 14;
end;
then Line(An,Bn) c= Line(PAn,PBn) & Line(PAn,PBn) c= Line(An,Bn);
hence thesis;
end;
theorem Th5:
An <> Cn & Cn in LSeg(An,Bn) & An in Ln & Cn in Ln & Ln is being_line
implies Bn in Ln
proof
assume that
A1: An <> Cn and
A2: Cn in LSeg(An,Bn) and
A3: An in Ln and
A4: Cn in Ln and
A5: Ln is being_line;
reconsider rAn=An,rCn=Cn,rBn=Bn as Element of REAL n by EUCLID:22;
Line(rAn,rCn) = Ln by A1,A3,A4,A5,EUCLIDLP:30;
then
A6: Line(An,Cn) = Ln by Th4;
LSeg(An,Bn) c= Line(An,Bn) by RLTOPSP1:73;
then
A7: Cn in Line(An,Bn) & An in Line(An,Bn) & An <> Cn by A1,A2,EUCLID_4:41;
Line(rAn,rBn) = Line(An,Bn) & Line(rAn,rCn)=Line(An,Cn) by Th4;
then Line(An,Bn) c= Line(An,Cn) by A7,EUCLID_4:11;
hence thesis by A6,EUCLID_4:41;
end;
definition
let n being Nat;
let S being Subset of REAL n;
attr S is being_point means ex Pn being Element of REAL n st S = {Pn};
end;
theorem Th6:
Ln is being_line or ex Pn being Element of REAL n st Ln={Pn}
proof
assume
A1: not Ln is being_line;
Ln in line_of_REAL n;
then Ln in the set of all Line(x1,x2) where
x1,x2 is Element of REAL n by EUCLIDLP:def 4;
then consider x1,x2 be Element of REAL n such that
A2: Ln = Line(x1,x2);
x1 = x2 by A1,A2;
then Ln = {x1} by A2,Th3;
hence thesis;
end;
theorem
Ln is being_line or Ln is being_point by Th6;
theorem Th7:
Ln is being_line implies not ex Pn being Element of REAL n st Ln={Pn}
proof
assume
A1: Ln is being_line;
given x be Element of REAL n such that
A2: Ln = {x};
consider x1,x2 be Element of REAL n such that
A3: x1 <> x2 and
A4: Ln = Line(x1,x2) by A1;
x1 in {x} & x2 in {x} by A2,A4,EUCLID_4:9;
then x1 = x & x2 = x by TARSKI:def 1;
hence contradiction by A3;
end;
theorem
Ln is being_line implies not Ln is being_point by Th7;
begin :: Between
reserve A,B,C for Point of TOP-REAL 2;
theorem Th8:
C in LSeg(A,B) implies |.A-B.| = |.A-C.| + |.C-B.|
proof
assume
A1: C in LSeg(A,B);
per cases;
suppose A,B,C are_mutually_distinct;
hence thesis by A1,EUCLID10:57;
end;
suppose not A,B,C are_mutually_distinct;
then per cases;
suppose A=B;
then LSeg(A,B) = {A} by RLTOPSP1:70;
then |.C-B.| = |.A-B.| & |.A-C.| = |.C-C.| & |.C-C.| = 0
by A1,TARSKI:def 1,EUCLID_6:42;
hence thesis;
end;
suppose C=B;
then |.C-B.| = |.B-B.| & |.A-C.| = |.A-B.| & |.B-B.| = 0
by EUCLID_6:42;
hence thesis;
end;
suppose C=A;
then |.A-C.| = |.C-C.| & |.A-B.| = |.C-B.| & |.C-C.| = 0
by EUCLID_6:42;
hence thesis;
end;
end;
end;
theorem Th9:
|.A-B.| = |.A-C.| + |.C-B.| implies C in LSeg(A,B)
proof
assume
A1: |.A-B.| = |.A-C.| + |.C-B.|; then
A2: |.B-A.| = |.A-C.| + |.C-B.| by EUCLID_6:43
.= |.A-C.| + |.B-C.| by EUCLID_6:43;
per cases;
suppose A=B;
then |.A-C.| = 0 & |.C-B.| = 0 by A1,EUCLID_6:42;
then A=C & C=B by EUCLID_6:42;
hence thesis by RLTOPSP1:68;
end;
suppose
A3: A<>B;
per cases;
suppose C=A or C=B;
hence thesis by RLTOPSP1:68;
end;
suppose
A4: C<>A & C<>B;
set a = |.A-B.|,b = |.C-B.|, c = |.C-A.|;
a * b <> 0
proof
assume a * b = 0;
then 0 = a * b / b
.= a by A4,EUCLID_6:42,XCMPLX_1:89;
hence thesis by A3,EUCLID_6:42;
end;
then
A5: 2 * a * b <> 0;
c = a - b by A1,EUCLID_6:43;
then
A6: c^2 = (a-b) * (a-b) by SQUARE_1:def 1
.= a * a - 2 * a * b + b * b
.= a^2 -2 * a * b + b * b by SQUARE_1:def 1
.= a^2 -2 * a * b + b^2 by SQUARE_1:def 1;
c^2 = a^2+b^2-2*a*b*cos angle(A,B,C) by EUCLID_6:7;
then
A7: cos angle(A,B,C) = 1 & 0 <= angle(A,B,C) < 2*PI
by A6,A5,EUCLID11:2,XCMPLX_1:7;
A,B,C are_mutually_distinct by A3,A4;
then
A8: angle(B,C,A)=PI or angle(B,A,C)=PI by A7,COMPTRIG:61,MENELAUS:8;
not A in LSeg(B,C)
proof
assume A in LSeg(B,C);
then |.B-C.| = |.A-C.| + |.B-C.| + |.A-C.| by A2,Th8
.= 2 * |.A-C.| + |.B-C.|;
hence contradiction by A4,EUCLID_6:42;
end;
hence thesis by A8,EUCLID_6:11;
end;
end;
end;
theorem Th10:
for p,q1,q2 being Point of TOP-REAL 2 holds
p in LSeg(q1,q2) iff dist(q1,p)+dist(p,q2)=dist(q1,q2)
proof
let p,q1,q2 be Point of TOP-REAL 2;
thus p in LSeg(q1,q2) implies dist(q1,p)+dist(p,q2)=dist(q1,q2)
by JORDAN1K:29;
assume
A1: dist(q1,p)+dist(p,q2)=dist(q1,q2);
reconsider w1 = q1,w2 = p, w3 = q2 as Element of REAL 2 by EUCLID:22;
reconsider z1 = q1,z2 = p, z3 = q2 as Point of Euclid 2 by EUCLID:67;
A2: dist(z1,z2)=|.w1-w2.| & dist(z1,z3)=|.w1-w3.| &
dist(z2,z3)=|.w2-w3.| by SPPOL_1:5;
dist(z1,z2)=dist(q1,p) & dist(z1,z3)=dist(q1,q2) &
dist(z2,z3)=dist(p,q2) by TOPREAL6:def 1;
then |.q1-p.| + |.p-q2.| = |.q1-q2.| by A1,A2;
hence p in LSeg(q1,q2) by Th9;
end;
theorem Th11:
for p,q,r be Element of Euclid 2 st p,q,r are_mutually_distinct &
p=A & q=B & r=C holds A in LSeg(B,C) iff p is_between q,r
proof
let p,q,r be Element of Euclid 2;
assume that
A1: p,q,r are_mutually_distinct and
A2: p = A & q = B & r = C;
hereby
assume
A3: A in LSeg(B,C);
dist(B,C) =dist(q,r) & dist(B,A) = dist(q,p) & dist(A,C) = dist(p,r)
by A2,TOPREAL6:def 1;
then dist(q,r) = dist(q,p)+dist(p,r) by A3,Th10;
hence p is_between q,r by A1,METRIC_1:def 22;
end;
assume p is_between q,r; then
A4: dist(q,r)=dist(q,p)+dist(p,r) by METRIC_1:def 22;
dist(q,r)=|.B-C.| & dist(q,p)=|.B-A.| & dist(p,r)=|.A-C.| by A2,SPPOL_1:39;
hence A in LSeg(B,C) by A4,Th9;
end;
theorem
for p,q,r be Element of Euclid 2 st
p,q,r are_mutually_distinct & p=A & q=B & r=C holds
A in LSeg(B,C) iff p is_Between q,r
proof
let p,q,r be Element of Euclid 2;
assume that
A1: p,q,r are_mutually_distinct and
A2: p = A & q = B & r = C;
hereby
assume A in LSeg(B,C);
then p is_between q,r by A1,A2,Th11;
hence p is_Between q,r by METRIC_1:def 22;
end;
assume p is_Between q,r;
then p is_between q,r by A1,METRIC_1:def 22;
hence A in LSeg(B,C) by A1,A2,Th11;
end;
begin :: REAL 2 is a plane
reserve x,y,z,y1,y2 for Element of REAL 2;
reserve L,L1,L2,L3,L4 for Element of line_of_REAL 2;
reserve D,E,F for Point of TOP-REAL 2;
reserve b,c,d,r,s for Real;
theorem Th12:
for OO,Ox,Oy be Element of REAL 2 st
OO = |[0,0]| & Ox = |[1,0]| & Oy = |[0,1]| holds
REAL 2 = plane(OO,Ox,Oy)
proof
let OO,Ox,Oy be Element of REAL 2 such that
A1: OO = |[0,0]| and
A2: Ox = |[1,0]| and
A3: Oy = |[0,1]|;
now
let a be object;
assume a in REAL 2;
then reconsider b = a as Point of TOP-REAL 2 by EUCLID:22;
A4: b = |[b`1 + 0 , 0 + b`2]| by EUCLID:53
.= |[ b`1 * 1 , b`1 * 0]| + |[ b`2 * 0 , b`2 *1 ]| by EUCLID:56
.= b`1 * |[1,0]| + |[ b`2 * 0 , b`2 *1 ]| by EUCLID:58
.= b`1 * |[1,0]| + b`2 * |[0,1]| by EUCLID:58;
reconsider a1 = 1 - (b`1+b`2) as Real;
reconsider a2 = b`1 as Real;
reconsider a3 = b`2 as Real;
a1 * |[0,0]| = |[a1 *0,a1 * 0]| by EUCLID:58
.= |[0,0]|; then
a1 * |[0,0]| + b = |[0,0]| + |[b`1,b`2]| by EUCLID:53
.= |[0 + b`1,0 + b`2]| by EUCLID:56
.= b by EUCLID:53;
then
A5: b = (a1 * |[0,0]|) + (a2 * |[1,0]|) + (a3 * |[0,1]|)
by A4,RLVECT_1:def 3;
a1+a2+a3 = 1 & b = a1 * OO + a2 * Ox + a3 * Oy by A1,A2,A5,A3;
then a in {x where x is Element of REAL 2 : ex a1,a2,a3 be Real st
a1+a2+a3=1 & x = a1*OO+a2*Ox+a3*Oy};
hence a in plane(OO,Ox,Oy) by EUCLIDLP:def 9;
end;
then REAL 2 c= plane(OO,Ox,Oy);
hence thesis;
end;
theorem Th13:
REAL 2 is Element of plane_of_REAL 2
proof
reconsider OO=|[0,0]|,Ox=|[1,0]|,Oy=|[0,1]| as Element of REAL 2
by EUCLID:22;
REAL 2 = plane(OO,Ox,Oy) by Th12;
then REAL 2 in {P where P is Subset of REAL 2 :
ex x1,x2,x3 being Element of REAL 2 st P = plane(x1,x2,x3)};
hence thesis by EUCLIDLP:def 11;
end;
theorem Th14:
|[1,0]| <> |[0,1]| & |[1,0]| <> |[0,0]| & |[0,1]| <> |[0,0]|
proof
|[1,0]|`1 = 1 & |[1,0]|`2 = 0 & |[0,1]|`1 = 0 & |[0,1]|`2 = 1 &
|[0,0]|`1 = 0 & |[0,0]|`2 = 0 by EUCLID:52;
hence thesis;
end;
theorem Th15:
ex x st not x in L
proof
assume
A1: x in L;
reconsider OO = |[0,0]|, Ox = |[1,0]|, Oy = |[0,1]| as Element of REAL 2
by EUCLID:22;
A2: OO in L & Ox in L & Oy in L by A1;
per cases by Th6;
suppose L is being_line;
then L = Line(Ox,Oy) by A2,Th14,EUCLIDLP:30;
then OO in the set of all (1-lambda) * Ox+lambda * Oy by A1;
then consider lambda such that
A3: OO = (1-lambda) * Ox + lambda * Oy;
A4: |[0,0]| = (1-lambda) * |[1,0]| + lambda * |[0,1]| by A3
.= |[(1-lambda) * 1 , (1-lambda) * 0]| + lambda * |[0,1]|
by EUCLID:58
.= |[1-lambda , 0]| + |[lambda * 0,lambda * 1]| by EUCLID:58
.= |[1-lambda + 0 , 0 + lambda]| by EUCLID:56
.= |[1-lambda,lambda]|;
|[0,0]|`1 = 0 & |[0,0]|`2 = 0 & |[1-lambda,lambda]|`1=1-lambda &
|[1-lambda,lambda]|`2 = lambda by EUCLID:52;
hence contradiction by A4;
end;
suppose ex x st L={x};
then consider x such that
A5: L = {x};
Ox in {x} & Oy in {x} by A5,A1;
then Ox = x & Oy = x by TARSKI:def 1;
hence contradiction by Th14;
end;
end;
theorem
ex L st L is being_point & L misses L1
proof
consider x such that
A1: not x in L1 by Th15;
x in REAL 2;
then {x} c= REAL 2 by TARSKI:def 1;
then reconsider L = {x} as Subset of REAL 2;
L = Line(x,x) by Th3;
then reconsider L as Element of line_of_REAL 2 by EUCLIDLP:47;
A2: L is being_point;
now
assume L meets L1;
then consider y be object such that
A3: y in L and
A4: y in L1 by XBOOLE_0:3;
thus contradiction by A1,A3,A4,TARSKI:def 1;
end;
hence thesis by A2;
end;
theorem Th16:
not L1 // L2 implies
(ex x st L1 = {x} or L2 = {x})
or
(L1 is being_line & L2 is being_line & ex x st L1 /\ L2 = {x})
proof
assume
A1: not L1 // L2;
set n = 2;
consider x1,x2 be Element of REAL 2 such that
A2: L1 = Line(x1,x2) by EUCLIDLP:51;
consider y1,y2 be Element of REAL 2 such that
A3: L2 = Line(y1,y2) by EUCLIDLP:51;
(x2-x1) = 0*n or (y2-y1) = 0*n or for r be Real holds
not ((x2-x1) =r*(y2-y1)) by A1,A2,A3,EUCLIDLP:def 7,EUCLIDLP:def 1;
then per cases by EUCLIDLP:9;
suppose x1=x2 or y1=y2;
then L1 = {x1} or L2 = {y1} by A2,A3,Th3;
hence thesis;
end;
suppose
A4: not(x1=x2) & (y1<>y2) & for r be Real holds (x2-x1) <> r*(y2-y1);
x2-x1, y2-y1 are_lindependent2
proof
assume x2-x1, y2-y1 are_ldependent2;
then x2-x1 = 0*n or y2-y1=0*n by A1,A2,A3,EUCLIDLP:def 7,EUCLIDLP:42;
hence contradiction by A4,EUCLIDLP:9;
end;
then consider Pt be Element of REAL 2 such that
A5: Pt in L1 and
A6: Pt in L2 by A2,A3,Th13,EUCLIDLP:114,EUCLIDLP:49;
A7: {Pt} c= L1 /\ L2
proof
let t be object;
assume t in {Pt};
then t = Pt by TARSKI:def 1;
hence thesis by A5,A6,XBOOLE_0:def 4;
end;
L1 /\ L2 c= {Pt}
proof
let t be object;
assume
A8: t in L1 /\ L2;
assume
not t in {Pt};
then
A9: t <> Pt by TARSKI:def 1;
reconsider t1=t as Element of REAL 2 by A8;
t1 in L1 & t1 in L2 & Pt in L1 & Pt in L2 by A8,A5,A6,XBOOLE_0:def 4;
then Line(t1,Pt) = L1 & Line(t1,Pt) = L2
by A2,A3,A9,EUCLID_4:10,EUCLID_4:11;
then L1 = L2 & L1 is being_line & L2 is being_line by A2,A4;
hence contradiction by A1,EUCLIDLP:65;
end;
then L1 /\ L2 = {Pt} by A7;
hence thesis by A4,A2,A3;
end;
end;
theorem
not L1 // L2 implies
L1 is being_point or L2 is being_point or
(L1 is being_line & L2 is being_line & L1 /\ L2 is being_point)
by Th16;
theorem Th17:
L1 /\ L2 is being_point & A in L1 /\ L2 implies L1 /\ L2 = {A}
by TARSKI:def 1;
begin :: The midpoint of a segment
definition
let A,B be Point of TOP-REAL 2;
func half_length(A,B) -> Real equals 1/2 * |.A-B.|;
correctness;
end;
theorem
half_length(A,B) = half_length(B,A) by EUCLID_6:43;
theorem
half_length(A,A) = 0
proof
half_length(A,A) = 1/2 * 0 by EUCLID_6:42;
hence thesis;
end;
theorem Th18:
|.A - 1/2 *(A+B).| = 1/2 * |.A-B.|
proof
|.A-(1/2 * (A+B)).| = |.A -(1/2 * A + 1/2 *B).| by RLVECT_1:def 5
.= |.A - 1/2 * A - 1/2 * B.| by RLVECT_1:27
.= |. 1 * A - 1/2 * A - 1/2 * B.| by RLVECT_1:def 8
.= |.(1-1/2) * A - 1/2 * B.| by RLVECT_1:35
.= |.1/2 * (A-B).| by RLVECT_1:34
.= |.1/2.| * |.A - B.| by TOPRNS_1:7
.= 1/2 * |.A - B.| by ABSVALUE:def 1;
hence thesis;
end;
theorem Th19:
ex C st C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.|
proof
take C = 1/2 * (A+B);
thus C in LSeg(A,B) by RLTOPSP1:69;
thus thesis by Th18;
end;
theorem Th20:
|.A-B.| = |.A-C.| & B in LSeg(A,D) & C in LSeg(A,D) implies B = C
proof
assume that
A1: |.A-B.| = |.A-C.| and
A2: B in LSeg(A,D) and
A3: C in LSeg(A,D);
consider lambda such that
A4: 0 <= lambda and
lambda <= 1 and
A6: B = (1-lambda) * A + lambda * D by A2,RLTOPSP1:76;
consider mu such that
A7: 0 <= mu and
mu <= 1 and
A9: C = (1-mu) * A + mu * D by A3,RLTOPSP1:76;
A10: (1-0) * A + 0 * D = (1-0) * A + 0.TOP-REAL 2 by RLVECT_1:10
.= 1 * A by RLVECT_1:4
.= A by RLVECT_1:def 8;
reconsider x1=A,x2=D as Element of REAL 2 by EUCLID:22;
A11: A = (1-0) * x1 + 0 * x2 & B=(1-lambda) * x1+lambda * x2 by A6,A10;
A12: |.A-B.| = |.B - A.| by EUCLID_6:43
.= |.(lambda - 0)*(D-A).| by A11,Th1
.= |.lambda.|*|.D-A.| by TOPRNS_1:7
.= lambda*|.D-A.| by A4,ABSVALUE:def 1;
A13: A = (1-0) * x1 + 0 * x2 & C=(1-mu) * x1+mu * x2 by A9,A10;
A14: |.A-C.| = |.C - A.| by EUCLID_6:43
.= |.(mu - 0)*(D-A).| by A13,Th1
.= |.mu.|*|.D-A.| by TOPRNS_1:7
.= mu *|.D-A.| by A7,ABSVALUE:def 1;
per cases;
suppose A=D;
then B in {A} & C in {A} by A2,A3,RLTOPSP1:70;
then B=A & C=A by TARSKI:def 1;
hence thesis;
end;
suppose A<>D;
then |.D-A.| <>0 by EUCLID_6:42;
then lambda = mu by A14,A1,A12,XCMPLX_1:5;
hence thesis by A6,A9;
end;
end;
definition
let A,B being Point of TOP-REAL 2;
func the_midpoint_of_the_segment(A,B) -> Point of TOP-REAL 2 means
:Def1:
ex C st C in LSeg(A,B) & it = C & |.A-C.| = half_length(A,B);
existence
proof
consider C such that
A1: C in LSeg(A,B) and
A2: |.A-C.| = half_length(A,B) by Th19;
take C;
thus thesis by A1,A2;
end;
uniqueness by Th20;
end;
theorem Th21:
the_midpoint_of_the_segment(A,B) in LSeg(A,B)
proof
consider C such that
A1: C in LSeg(A,B) and
A2: C = the_midpoint_of_the_segment(A,B) and
|.A-C.| = half_length(A,B) by Def1;
thus thesis by A1,A2;
end;
theorem Th22:
the_midpoint_of_the_segment(A,B) = 1/2 * (A+B)
proof
now
1/2 * (A+B) = (1-1/2) * A + 1/2 * B by RLVECT_1:def 5;
then 1/2 * (A+B) in {(1-r)*A+r*B:0<=r<=1};
hence 1/2 * (A+B) in LSeg(A,B) by RLTOPSP1:def 2;
thus |.A-(1/2 *(A+B)).| = half_length(A,B) by Th18;
end;
hence thesis by Def1;
end;
theorem Th23:
the_midpoint_of_the_segment(A,B) = the_midpoint_of_the_segment(B,A)
proof
the_midpoint_of_the_segment(A,B) = 1/2*(B+A) by Th22
.= the_midpoint_of_the_segment(B,A) by Th22;
hence thesis;
end;
theorem Th24:
the_midpoint_of_the_segment(A,A)=A
proof
the_midpoint_of_the_segment(A,A) = 1/2*(A+A) by Th22
.= 1/2 * A + 1/2 * A by RVSUM_1:51
.= (1/2+1/2)*A by RVSUM_1:50
.= A by RVSUM_1:52;
hence thesis;
end;
theorem Th25:
the_midpoint_of_the_segment(A,B) = A implies A=B
proof
assume the_midpoint_of_the_segment(A,B) = A; then
A1: A = 1/2*(A+B) by Th22
.= 1/2 * A + 1/2 * B by RVSUM_1:51;
A2: 1/2 * A + 1/2 * A = (1/2 + 1/2) * A by RVSUM_1:50
.= A by RVSUM_1:52;
reconsider rA=A, rB=B as Element of REAL 2 by EUCLID:22;
1/2 * rA + 1/2 * rA = 1/2 * rA + 1/2 * rB by A1,A2;
then 2*(1/2*A) = 2*(1/2*B) by RVSUM_1:25;
then (2*1/2)*A = 2*(1/2*B) by RVSUM_1:49;
then 1*A=1*B by RVSUM_1:49;
then A = 1*B by RVSUM_1:52;
hence thesis by RVSUM_1:52;
end;
theorem Th26:
the_midpoint_of_the_segment(A,B) = B implies A=B
proof
assume the_midpoint_of_the_segment(A,B) = B;
then the_midpoint_of_the_segment(B,A) = B by Th23;
hence thesis by Th25;
end;
theorem Th27:
C in LSeg(A,B) & |.A-C.| = |.B-C.| implies half_length(A,B) = |.A-C.|
proof
assume that
A1: C in LSeg(A,B) and
A2: |.A-C.| = |.B-C.|;
A3: |.C-B.| = |.A-C.| by A2,EUCLID_6:43;
half_length(A,B) = 1/2* (|.A-C.|+|.C-B.|) by A1,Th8
.= 1/2* (2*|.A-C.|) by A3;
hence thesis;
end;
theorem Th28:
C in LSeg(A,B) & |.A-C.| = |.B-C.| implies
C = the_midpoint_of_the_segment(A,B)
proof
assume that
A1: C in LSeg(A,B) and
A2: |.A-C.| = |.B-C.|;
|.A-C.| = half_length(A,B) by A1,A2,Th27;
hence thesis by A1,Def1;
end;
theorem
|.A - the_midpoint_of_the_segment(A,B).|
= |. the_midpoint_of_the_segment(A,B) - B.|
proof
A1: |.A - the_midpoint_of_the_segment(A,B).| = |.A - 1/2*(A+B).| by Th22
.= 1/2*|.A-B.| by Th18;
|.the_midpoint_of_the_segment(A,B) - B.| = |.1/2*(A+B) - B.| by Th22
.= |.B - 1/2*(A+B).| by EUCLID_6:43
.= 1/2*|.B-A.| by Th18
.= 1/2*|.A-B.| by EUCLID_6:43;
hence thesis by A1;
end;
theorem Th29:
A<>B & r is positive & r <> 1 & |.A-C.| = r * |.A-B.| implies
A,B,C are_mutually_distinct
proof
assume that
A1: A<>B and
A2: r is positive and
A3: r <> 1 and
A4: |.A-C.| = r * |.A-B.|;
now
hereby
assume A=C;
then r * |.A-B.| = r * 0 by A4,EUCLID_6:42;
then |.A-B.| = 0 by A2,XCMPLX_1:5;
hence contradiction by A1,EUCLID_6:42;
end;
hereby
assume B=C;
then 1 * |.A-B.| = r * |.A-B.| & |.A-B.| <> 0 by A1,A4,EUCLID_6:42;
hence contradiction by A3,XCMPLX_1:5;
end;
end;
hence thesis by A1;
end;
theorem Th30:
C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.| implies |.B-C.| = 1/2 * |.A-B.|
proof
assume that
A1: C in LSeg(A,B) and
A2: |.A-C.| = 1/2 * |.A-B.|;
|.A-B.| = |.A-C.| + |.C-B.| by A1,Th8;
hence thesis by A2,EUCLID_6:43;
end;
begin :: Perpendicularity
theorem Th31:
L1,L2 are_coplane
proof
reconsider OO = |[0,0]|, Ox = |[1,0]|, Oy = |[0,1]| as Element of REAL 2
by EUCLID:22;
REAL 2 = plane(OO,Ox,Oy) by Th12;
hence thesis by EUCLIDLP:def 12;
end;
theorem
L1 _|_ L2 implies L1 meets L2 by Th31,EUCLIDLP:109;
theorem
L1 is being_line & L2 is being_line & L1 misses L2 implies L1//L2
by Th31,EUCLIDLP:113;
theorem Th32:
L1 <> L2 & L1 meets L2 implies
(ex x st L1 = {x} or L2 = {x})
or
(L1 is being_line & L2 is being_line & ex x st L1 /\ L2 = {x})
proof
assume that
A1: L1<>L2 and
A2: L1 meets L2;
not L1 // L2 by A1,A2,EUCLIDLP:71;
hence thesis by Th16;
end;
theorem Th33:
L1 _|_ L2 implies ex x st L1 /\ L2 = {x}
proof
assume
A1: L1 _|_ L2;
then
A2: L1 is being_line & L2 is being_line by EUCLIDLP:67;
A3: L1 <> L2 & L1 meets L2 by A1,EUCLIDLP:75,Th31,EUCLIDLP:109;
not (ex x st L1 = {x} or L2 = {x}) by A2,Th7;
hence thesis by A3,Th32;
end;
theorem
L1 _|_ L2 implies L1 /\ L2 is being_point by Th33;
theorem Th34:
L1 _|_ L2 implies not L1 // L2
proof
assume L1 _|_ L2;
then L1 <> L2 & L1 meets L2 by EUCLIDLP:75,Th31,EUCLIDLP:109;
hence thesis by EUCLIDLP:71;
end;
theorem
L1 is being_line & L2 is being_line & L1 // L2 implies not L1 _|_ L2 by Th34;
theorem Th35:
L1 is being_line implies ex L2 st x in L2 & L1 _|_ L2
proof
assume
A1: L1 is being_line;
per cases;
suppose x in L1;
consider x1 be Element of REAL 2 such that
A2: not x1 in L1 by Th15;
consider L2 such that
x1 in L2 and
A3: L1 _|_ L2 and
L1 meets L2 by A1,A2,EUCLIDLP:62;
consider L3 such that
A4: x in L3 and
A5: L3 _|_ L1 and
L3 // L2 by A3,EUCLIDLP:80;
thus thesis by A4,A5;
end;
suppose not x in L1;
then consider L2 such that
A6: x in L2 and
A7: L1 _|_ L2 and
L1 meets L2 by A1,EUCLIDLP:62;
thus thesis by A6,A7;
end;
end;
theorem Th36:
L1 _|_ L2 & L1 = Line(A,B) & L2 = Line(C,D) implies |(B-A,D-C)| = 0
proof
assume that
A1: L1 _|_ L2 and
A2: L1 = Line(A,B) and
A3: L2 = Line(C,D);
consider x1,x2,y1,y2 be Element of REAL 2 such that
A4: L1 = Line(x1,x2) and
A5: L2 = Line(y1,y2) and
A6: (x2 - x1) _|_ (y2-y1) by A1,EUCLIDLP:def 8;
A7: |(x2-x1,y2-y1)| = 0 by A6,EUCLIDLP:def 3,RVSUM_1:def 17;
A8: A in Line(x1,x2) & B in Line(x1,x2) by A2,A4,EUCLID_4:41;
then consider lambda such that
A9: A = (1-lambda) * x1 + lambda * x2;
consider mu such that
A10: B = (1-mu) * x1 + mu * x2 by A8;
A11: C in Line(y1,y2) & D in Line(y1,y2) by A3,A5,EUCLID_4:41;
then consider lambda2 such that
A12: C = (1-lambda2) * y1 + lambda2 * y2;
consider mu2 such that
A13: D = (1-mu2) * y1 + mu2 * y2 by A11;
A14: B-A = (mu-lambda) * (x2-x1) by A9,A10,Th1;
reconsider a = mu - lambda, b = mu2 - lambda2 as Real;
|(B-A,D-C)| = |(a*(x2-x1),b*(y2-y1))| by A14,A12,A13,Th1
.= a * |(x2-x1,b*(y2-y1))| by EUCLID_4:21
.= a * (b * |(x2-x1,y2-y1)|) by EUCLID_4:22
.= 0 by A7;
hence thesis;
end;
theorem Th37:
L is being_line & A in L & B in L & A <> B implies L = Line(A,B)
proof
assume
A1: L is being_line & A in L & B in L & A <> B;
reconsider x1=A,x2=B as Element of REAL 2 by EUCLID:22;
L = Line(x1,x2) by A1,EUCLID_4:10,EUCLID_4:11;
hence thesis by Th4;
end;
theorem Th38:
L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A<>C & B<>C
implies angle(A,C,B) = PI/2 or angle(A,C,B) = 3 * PI/2
proof
assume that
A1: L1 _|_ L2 and
A2: C in L1 /\ L2 and
A3: A in L1 and
A4: B in L2 and
A5: A<>C & B<>C;
A6: C in L1 & C in L2 by A2,XBOOLE_0:def 4;
now
L1 is being_line by A1,EUCLIDLP:67;
hence L1 = Line(C,A) by A3,A5,A6,Th37;
L2 is being_line by A1,EUCLIDLP:67;
hence L2 = Line(C,B) by A4,A5,A6,Th37;
end;
then |(A-C,B-C)| = 0 by A1,Th36;
hence thesis by A5,EUCLID_3:45;
end;
theorem
L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C
implies A,B,C is_a_triangle
proof
assume that
A1: L1 _|_ L2 and
A2: C in L1 /\ L2 and
A3: A in L1 and
A4: B in L2 and
A5: A<>C and
A6: B<>C;
not A in Line(B,C)
proof
assume
A7: A in Line(B,C);
A8: C in L1 & C in L2 by A2,XBOOLE_0:def 4;
A9: L1 is being_line & L2 is being_line by A1,EUCLIDLP:67;
consider x such that
A10: L1 /\ L2 = {x} by A1,Th33;
A11: L1/\L2 = {C} by A2,A10,TARSKI:def 1;
A in L2 & A in L1 by A3,A7,A4,A9,A8,A6,Th37;
then A in {C} by A11,XBOOLE_0:def 4;
hence contradiction by A5,TARSKI:def 1;
end;
hence thesis by A6,MENELAUS:13;
end;
begin :: The Perpendicular bisector of a segment
theorem Th39:
A <> B & L1 = Line(A,B) & C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.|
implies ex L2 st C in L2 & L1 _|_ L2
proof
assume
A1: A <> B & L1 = Line(A,B) & C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.|;
reconsider x1=A,x2=B,x3=C as Element of REAL 2 by EUCLID:22;
Line(A,B) = Line(x1,x2) by Th4;
then L1 is being_line by A1;
then consider L2 such that
A2: x3 in L2 and
A3: L1 _|_ L2 by Th35;
thus thesis by A2,A3;
end;
definition
let A,B being Element of TOP-REAL 2;
assume
A1: A <> B;
func the_perpendicular_bisector(A,B) -> Element of line_of_REAL 2 means
:Def2:
ex L1, L2 be Element of line_of_REAL 2 st it = L2 &
L1 = Line(A,B) & L1 _|_ L2 & L1 /\ L2 = {the_midpoint_of_the_segment(A,B)};
existence
proof
set M=the_midpoint_of_the_segment(A,B);
reconsider rA=A,rB=B as Element of REAL 2 by EUCLID:22;
reconsider L1 = Line(rA,rB) as Element of line_of_REAL 2 by EUCLIDLP:47;
A2: Line(rA,rB) = Line(A,B) by Th4;
now
thus L1 = Line(A,B) by Th4;
thus M in LSeg(A,B) by Th21;
thus |.A - M.| = |.A - 1/2*(A+B).| by Th22
.= 1/2 * |.A-B.| by Th18;
end;
then consider L2 be Element of line_of_REAL 2 such that
A3: M in L2 and
A4: L1 _|_ L2 by A1,Th39;
A5: M in LSeg(A,B) & LSeg(A,B) c= Line(A,B) by Th21,RLTOPSP1:73;
consider x such that
A6: L1/\L2 = {x} by A4,Th33;
M in {x} by A5,A2,A3,XBOOLE_0:def 4,A6;
then L1/\L2={M} & L1 = Line(A,B) & L1 _|_ L2
by A4,A6,Th4,TARSKI:def 1;
hence thesis;
end;
uniqueness
proof
let L1,L2 be Element of line_of_REAL 2 such that
A7: ex D1,D2 be Element of line_of_REAL 2 st
L1 = D2 & D1=Line(A,B) & D1_|_D2 &
D1/\D2= {the_midpoint_of_the_segment(A,B)} and
A8: ex D3, D4 be Element of line_of_REAL 2 st
L2 = D4 & D3 = Line(A,B) & D3_|_D4 &
D3/\D4 = {the_midpoint_of_the_segment(A,B)};
set M=the_midpoint_of_the_segment(A,B);
consider D1,D2 be Element of line_of_REAL 2 such that
A9: L1 = D2 and
A10: D1 = Line(A,B) and
A11: D1 _|_ D2 and
A12: D1 /\ D2 = {M} by A7;
consider D3,D4 be Element of line_of_REAL 2 such that
A13: L2 = D4 and
A14: D3 = Line(A,B) and
A15: D3 _|_ D4 and
A16: D3 /\ D4 = {M} by A8;
A17: D2 // D4 by A10,A14,A11,A15,Th13,EUCLIDLP:111;
M in D1/\D2 & M in D1/\D4 by A10,A14,A12,A16,TARSKI:def 1;
then M in D2 & M in D4 by XBOOLE_0:def 4;
hence thesis by A9,A13,A17,EUCLIDLP:71,XBOOLE_0:3;
end;
end;
theorem
A <> B implies the_perpendicular_bisector(A,B) is being_line
proof
assume A<>B;
then consider L1, L2 be Element of line_of_REAL 2 such that
A1: the_perpendicular_bisector(A,B) = L2 and
L1=Line(A,B) and
A2: L1_|_L2 and
L1/\L2= {the_midpoint_of_the_segment(A,B)} by Def2;
thus thesis by A1,A2,EUCLIDLP:67;
end;
theorem
A <> B implies
the_perpendicular_bisector(A,B) = the_perpendicular_bisector(B,A)
proof
assume
A1: A<>B;
then consider L1, L2 be Element of line_of_REAL 2 such that
A2: the_perpendicular_bisector(A,B) = L2 and
A3: L1 = Line(A,B) and
A4: L1 _|_ L2 and
A5: L1 /\ L2= {the_midpoint_of_the_segment(A,B)} by Def2;
consider L3, L4 be Element of line_of_REAL 2 such that
A6: the_perpendicular_bisector(B,A) = L4 and
A7: L3 = Line(A,B) and
A8: L3 _|_ L4 and
A9: L3 /\ L4 = {the_midpoint_of_the_segment(B,A)} by A1,Def2;
set M=the_midpoint_of_the_segment(A,B);
consider x such that
A10: L1 /\ L2 = {x} by A4,Th33;
consider y such that
A11: L3 /\ L4= {y} by A8,Th33;
A12: L2 // L4 by A3,A4,A7,A8,Th13,EUCLIDLP:111;
{x}={M} & {y}={M} by A5,A9,A10,A11,Th23;
then M in L1/\L2 & M in L3/\L4 by A10,A11,TARSKI:def 1;
then M in L1 & M in L2 & M in L3 & M in L4 by XBOOLE_0:def 4;
hence thesis by A2,A6,A12,XBOOLE_0:3,EUCLIDLP:71;
end;
theorem Th40:
A <> B & L1=Line(A,B) & C in LSeg(A,B) & |.A-C.| = 1/2 * |.A-B.| &
C in L2 & L1 _|_ L2 & D in L2 implies |.D-A.| = |.D-B.|
proof
assume that
A1: A <> B and
A2: L1=Line(A,B) and
A3: C in LSeg(A,B) and
A4: |.A-C.| = 1/2 * |.A-B.| and
A5: C in L2 and
A6: L1 _|_ L2 and
A7: D in L2;
per cases;
suppose
A8: D=C;
then |.D-A.| = 1/2 * |.A-B.| by A4,EUCLID_6:43
.= |.B-C.| by A3,A4,Th30
.= |.D-B.| by A8,EUCLID_6:43;
hence thesis;
end;
suppose
A9: D<>C;
A10: A,B,C are_mutually_distinct by A1,A4,Th29;
C in L1 & A in L1 by A3,A2,MENELAUS:12,RLTOPSP1:68;
then
A11: L1 _|_ L2 & C in L1/\L2 & A in L1 & D in L2 & A<> C & D<>C
by A5,A6,A7,A10,A9,XBOOLE_0:def 4;
C in L1 & B in L1 by A3,A2,MENELAUS:12,RLTOPSP1:68;
then
A12: L1 _|_ L2 & C in L1/\L2 & B in L1 & D in L2 & B<>C & D<>C
by A6,A7,A10,A9,A5,XBOOLE_0:def 4;
reconsider a1 = |.D-C.|, b1 = |.A-C.|, c1 = |.A-D.| as Real;
reconsider a2 = |.D-C.|, b2 = |.B-C.|, c2 = |.B-D.| as Real;
A13: cos angle(D,C,A) = 0 by A11,Th38,SIN_COS:77;
A14: cos angle(D,C,B) = 0 by A12,Th38,SIN_COS:77;
c1^2 = a1^2 + b1^2 - 2*a1*b1*cos angle(D,C,A) by EUCLID_6:7
.= a2^2 + b2^2 - 2*a2*b2*cos angle(D,C,B) by A13,A14,A3,A4,Th30
.= c2^2 by EUCLID_6:7;
then
A15: c1 = sqrt(c2^2) by SQUARE_1:22
.= c2 by SQUARE_1:22;
|.A-D.| = |.D-A.| & |.B-D.| = |.D-B.| by EUCLID_6:43;
hence thesis by A15;
end;
end;
theorem Th41:
A <> B & C in the_perpendicular_bisector(A,B) implies |.C-A.| = |.C-B.|
proof
assume that
A1: A<>B and
A2: C in the_perpendicular_bisector(A,B);
consider L1, L2 be Element of line_of_REAL 2 such that
A3: the_perpendicular_bisector(A,B) = L2 and
A4: L1 = Line(A,B) and
A5: L1 _|_ L2 and
A6: L1 /\ L2 = {the_midpoint_of_the_segment(A,B)} by A1,Def2;
set D = the_midpoint_of_the_segment(A,B);
now
thus A<>B by A1;
thus L1 = Line(A,B) by A4;
thus D in LSeg(A,B) by Th21;
consider E such that
E in LSeg(A,B) and
A7: the_midpoint_of_the_segment(A,B) = E and
A8: |.A-E.| = half_length(A,B) by Def1;
thus |.A-D.|=1/2*|.A-B.| by A7,A8;
D in L1/\L2 by A6,TARSKI:def 1;
hence D in L2 by XBOOLE_0:def 4;
thus L1 _|_ L2 by A5;
thus C in L2 by A2,A3;
end;
hence thesis by Th40;
end;
theorem Th42:
C in Line(A,B) & |.A-C.| = |.B-C.| implies C in LSeg(A,B)
proof
assume that
A1: C in Line(A,B) and
A2: |.A-C.| = |.B-C.|;
per cases;
suppose
A3: A=B;
reconsider rA=A,rB=B as Element of REAL 2 by EUCLID:22;
Line(rA,rA) = Line(A,A) & Line(rA,rB) = Line(A,B) by Th4;
then Line(A,B) = {A} by A3,Th3;
hence thesis by A1,A3,RLTOPSP1:70;
end;
suppose A<>B;
then
A4: |.A-B.| <> 0 by EUCLID_6:42;
reconsider rA=A, rB=B,rC=C as Element of REAL 2 by EUCLID:22;
C in Line(rA,rB) by A1,Th4;
then consider a such that
A5: C = (1-a) * rA + a * rB;
set n=2;
rA - rC = rA - ((1 * rA + (-a) * rA) + a * rB) by A5,EUCLIDLP:11
.= rA + ((-1)*rA + (-(-a))*rA + (-a) * rB) by EUCLIDLP:14
.= rA + ((-1)*rA + (a*rA +(-a) * rB)) by RVSUM_1:15
.= (rA - rA) + (a*rA +(-a) * rB) by RVSUM_1:15
.= 0*n + (a*rA +(-a)*rB) by EUCLIDLP:2
.= a*rA +(-a)*rB by EUCLID_4:1
.= a*(rA-rB) by EUCLIDLP:12;
then
A6: |.A-C.| = |.a.| * |.A-B.| by EUCLID:11;
rB - rC = rB - a*rB - (1-a)*rA by A5,RVSUM_1:39
.= (1*rB - a*rB) - (1-a) * rA by EUCLID_4:3
.= (1-a) * rB - (1-a) *rA by EUCLIDLP:11
.= (1-a) * (rB - rA) by EUCLIDLP:12;
then |.B-C.| = |.1-a.| * |.B-A.| by EUCLID:11
.= |.1-a.| * |.A-B.| by EUCLID_6:43;
then |.a.| = |.1-a.| by A6,A2,A4,XCMPLX_1:5;
then a = 1/2 by Th2;
then C = (1-1/2) * A + 1/2 * B by A5;
then C in {(1-r) * A + r * B : 0 <= r & r <= 1};
hence thesis by RLTOPSP1:def 2;
end;
end;
theorem Th43:
A <> B implies
the_midpoint_of_the_segment(A,B) in the_perpendicular_bisector(A,B)
proof
assume A<>B;
then consider L1, L2 be Element of line_of_REAL 2 such that
A1: the_perpendicular_bisector(A,B)= L2 and
L1 = Line(A,B) & L1 _|_ L2 and
A2: L1 /\ L2 = {the_midpoint_of_the_segment(A,B)} by Def2;
the_midpoint_of_the_segment(A,B) in L1/\L2 by A2,TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th44:
A<>B & L1 = Line(A,B) & L1 _|_ L2 & the_midpoint_of_the_segment(A,B) in L2
implies L2 = the_perpendicular_bisector(A,B)
proof
assume that
A1: A<>B and
A2: L1 = Line(A,B) and
A3: L1 _|_ L2 and
A4: the_midpoint_of_the_segment(A,B) in L2;
set M = the_midpoint_of_the_segment(A,B);
consider L3, L4 be Element of line_of_REAL 2 such that
A5: the_perpendicular_bisector(A,B) = L4 and
A6: L3 = Line(A,B) and
A7: L3 _|_ L4 and
A8: L3 /\ L4 = {the_midpoint_of_the_segment(A,B)} by A1,Def2;
A9: L2 // L4 by A2,A3,A6,A7,Th13,EUCLIDLP:111;
M in L3/\L4 by A8,TARSKI:def 1;
then M in L2 & M in L4 by A4,XBOOLE_0:def 4;
hence thesis by A5,A9,XBOOLE_0:3,EUCLIDLP:71;
end;
theorem Th45:
A <> B & |.C-A.| = |.C-B.| implies C in the_perpendicular_bisector(A,B)
proof
assume that
A1: A <> B and
A2: |.C-A.| = |.C-B.|;
assume
A3: not C in the_perpendicular_bisector(A,B);
consider L1, L2 be Element of line_of_REAL 2 such that
the_perpendicular_bisector(A,B) = L2 and
A4: L1 = Line(A,B) and
A5: L1 _|_ L2 and
L1 /\ L2 = {the_midpoint_of_the_segment(A,B)} by A1,Def2;
reconsider rA=A,rB=B,rC=C as Element of REAL 2 by EUCLID:22;
L1 is being_line by A5,EUCLIDLP:67;
then consider L3 such that
A6: rC in L3 and
A7: L1 _|_ L3 by Th35;
consider x such that
A8: L1 /\ L3 = {x} by A7,Th33;
reconsider D=x as Point of TOP-REAL 2 by EUCLID:22;
A9: D in L1/\L3 by A8,TARSKI:def 1;
A10:
now
assume A=D or C=D or B=D;
then per cases;
suppose
A11: A=D;
now
thus L1 _|_ L3 by A7;
thus A in L3 /\ L1 by A11,A8,TARSKI:def 1;
thus C in L3 & B in L1 by A6,A4,RLTOPSP1:72;
A<>C
proof
assume
A12: A=C;
then |.C-B.| = 0 by A2,EUCLID_6:42;
hence contradiction by A12,A1,EUCLID_6:42;
end;
hence A<>C & B<>A by A1;
end;
then
A13: cos angle(C,A,B) = 0 by SIN_COS:77,Th38;
set z1=|.B-C.|;
set z2=|.C-A.|;
set z3=|.B-A.|;
A14: z1^2 = z2^2+z3^2-2*z2*z3*cos angle(C,A,B) by EUCLID_6:7
.= z2^2+z3^2 by A13;
z1^2 = z1^2+z3^2 by A14,A2,EUCLID_6:43;
then z3=0 by SQUARE_1:12;
hence contradiction by A1,EUCLID_6:42;
end;
suppose C=D;
then C in L1/\L3 by A8,TARSKI:def 1;
then
A15: C in Line(A,B) by A4,XBOOLE_0:def 4;
A16: |.A-C.| = |.C-B.| by A2,EUCLID_6:43
.= |.B-C.| by EUCLID_6:43;
then C in LSeg(A,B) by A15,Th42;
then C = the_midpoint_of_the_segment(A,B) by A16,Th28;
hence contradiction by A3,A1,Th43;
end;
suppose
A17: B=D;
now
thus L1 _|_ L3 by A7;
thus B in L3 /\ L1 by A17,A8,TARSKI:def 1;
thus C in L3 & A in L1 by A6,A4,RLTOPSP1:72;
B<>C
proof
assume
A18: B=C;
then |.C-A.| = 0 by A2,EUCLID_6:42;
hence contradiction by A18,A1,EUCLID_6:42;
end;
hence B<>C & B<>A by A1;
end;
then
A19: angle(C,B,A) = PI/2 or angle(C,B,A) = PI + PI/2 by Th38;
set z1=|.A-C.|;
set z2=|.C-B.|;
set z3=|.A-B.|;
z1^2 = z2^2+z3^2-2*z2*z3*cos angle(C,B,A) by EUCLID_6:7
.= z2^2+z3^2 by A19,SIN_COS:77;
then z1^2 = z1^2+z3^2 by A2,EUCLID_6:43;
then z3 = 0 by SQUARE_1:12;
hence contradiction by A1,EUCLID_6:42;
end;
end;
A20: L1 _|_ L3 & D in L1 /\ L3 & A in L1 & C in L3 &
A <> D & C <> D by A7,A8,TARSKI:def 1,A4,RLTOPSP1:72,A6,A10;
A21: L1 _|_ L3 & D in L1 /\ L3 & B in L1 & C in L3 &
B <> D & C <> D by A7,A8,TARSKI:def 1,A4,RLTOPSP1:72,A6,A10;
set a1 = |.A-D.|;
set b1 = |.C-D.|;
set c1 = |.C-A.|;
A22: c1^2 = a1^2 + b1^2 - 2 * a1 * b1 * cos angle(A,D,C) by EUCLID_6:7
.= a1^2 + b1^2 - 2 * a1 * b1 * 0 by A20,SIN_COS:77,Th38
.= a1^2 + b1^2;
set a2 = |.B-D.|;
set b2 = |.C-D.|;
set c2 = |.C-B.|;
c2^2 = a2^2 + b2^2 - 2 * a2 * b2 * cos angle(B,D,C) by EUCLID_6:7
.= a2^2 + b2^2 - 2 * a2 * b2 * 0 by A21,Th38,SIN_COS:77
.= a2^2 + b2^2;
then
A23: a1^2 + b1^2 = a2^2+b2^2 by A2,A22;
now
assume a1 = -a2;
then -(-a2) <= -0;
then a2 = 0;
hence contradiction by A10,EUCLID_6:42;
end;
then D in L1 & |.A-D.|=|.B-D.| by SQUARE_1:40,A9,A23,XBOOLE_0:def 4;
then D in LSeg(A,B) & |.A-D.| = |.B-D.| by A4,Th42;
then D = the_midpoint_of_the_segment(A,B) & D in L3
by Th28,A9,XBOOLE_0:def 4;
hence contradiction by A3,A6,A1,A4,A7,Th44;
end;
begin :: The circumcircle of a triangle
theorem Th46:
A,B,C is_a_triangle implies
the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C)
is being_point
proof
assume
A1: A,B,C is_a_triangle;
then
A2: A,B,C are_mutually_distinct by EUCLID_6:20;
set MAB = the_perpendicular_bisector(A,B);
set MiAB = the_midpoint_of_the_segment(A,B);
set MBC = the_perpendicular_bisector(B,C);
set MiBC = the_midpoint_of_the_segment(B,C);
consider LAB1,LAB2 be Element of line_of_REAL 2 such that
A3: MAB = LAB2 and
A4: LAB1 = Line(A,B) and
A5: LAB1 _|_ LAB2 and
LAB1 /\ LAB2 = {MiAB} by A2,Def2;
consider LBC1,LBC2 be Element of line_of_REAL 2 such that
A6: MBC = LBC2 and
A7: LBC1 = Line(B,C) and
A8: LBC1 _|_ LBC2 and
LBC1 /\ LBC2 = {MiBC} by A2,Def2;
now
hereby
assume LAB2 // LBC2;
then LBC1 _|_ LAB2 by A8,EUCLIDLP:61;
then
A9: LAB1 // LBC1 by A5,Th13,EUCLIDLP:111;
B in LAB1 & B in LBC1 by A4,A7,RLTOPSP1:72;
then LAB1=LBC1 by A9,EUCLIDLP:71,XBOOLE_0:3;
then C in LAB1 by A7,RLTOPSP1:72;
then C,A,B are_collinear by A2,A4,MENELAUS:13;
hence contradiction by A1,MENELAUS:15;
end;
thus LAB2 is being_line by A5,EUCLIDLP:67;
thus LBC2 is being_line by A8,EUCLIDLP:67;
end;
then not LAB2 // LBC2 & not LAB2 is being_point & not LBC2 is being_point
by Th7;
hence thesis by A3,A6,Th16;
end;
theorem Th47:
A,B,C is_a_triangle implies ex D st
the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C) = {D} &
the_perpendicular_bisector(B,C) /\ the_perpendicular_bisector(C,A) = {D} &
the_perpendicular_bisector(C,A) /\ the_perpendicular_bisector(A,B) = {D} &
|.D-A.| = |.D-B.| & |.D-A.| = |.D-C.| & |.D-B.| = |.D-C.|
proof
assume
A1: A,B,C is_a_triangle;
then
A2: A,B,C are_mutually_distinct by EUCLID_6:20;
set MAB = the_perpendicular_bisector(A,B);
set MiAB = the_midpoint_of_the_segment(A,B);
set MBC = the_perpendicular_bisector(B,C);
set MiBC = the_midpoint_of_the_segment(B,C);
set MCA = the_perpendicular_bisector(C,A);
set MiCA = the_midpoint_of_the_segment(C,A);
MAB /\ MBC is being_point by A1,Th46;
then consider x such that
A3: MAB /\ MBC ={x};
B,C,A is_a_triangle by A1,MENELAUS:15;
then MBC /\ MCA is being_point by Th46;
then consider y such that
A4: MBC /\ MCA ={y};
C,A,B is_a_triangle by A1,MENELAUS:15;
then MCA /\ MAB is being_point by Th46;
then consider z such that
A5: MCA /\ MAB ={z};
x in MAB/\MBC by A3,TARSKI:def 1;
then
A6: x in MAB & x in MBC by XBOOLE_0:def 4;
reconsider Px=x as Point of TOP-REAL 2 by EUCLID:22;
A7: |.Px-A.| = |.Px-B.| & |.Px-B.|=|.Px-C.| by A6,Th41;
y in MBC/\MCA by A4,TARSKI:def 1;
then
A8: y in MBC & y in MCA by XBOOLE_0:def 4;
reconsider Py=y as Point of TOP-REAL 2 by EUCLID:22;
|.Py-B.| = |.Py-C.| & |.Py-C.| = |.Py-A.| by A8,Th41;
then Py in MAB by A2,Th45;
then Py in MAB/\MBC by A8,XBOOLE_0:def 4;
then
A9: Py = Px by A3,TARSKI:def 1;
z in MCA/\MAB by A5,TARSKI:def 1;
then
A10: z in MCA & z in MAB by XBOOLE_0:def 4;
reconsider Pz=z as Point of TOP-REAL 2 by EUCLID:22;
|.Pz-C.| = |.Pz-A.| & |.Pz-A.| = |.Pz-B.| by A10,Th41;
then Pz in MBC by A2,Th45;
then
A11: Pz in MBC/\MCA by A10,XBOOLE_0:def 4;
take Px;
thus thesis by A7,A3,A4,A5,TARSKI:def 1,A11,A9;
end;
definition
let A,B,C being Point of TOP-REAL 2;
assume
A1: A,B,C is_a_triangle;
func the_circumcenter(A,B,C) -> Point of TOP-REAL 2 means
:Def3:
the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C) = {it} &
the_perpendicular_bisector(B,C) /\ the_perpendicular_bisector(C,A) = {it} &
the_perpendicular_bisector(C,A) /\ the_perpendicular_bisector(A,B) = {it};
existence
proof
consider D such that
A2: the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C) = {D} &
the_perpendicular_bisector(B,C) /\ the_perpendicular_bisector(C,A) = {D} &
the_perpendicular_bisector(C,A) /\ the_perpendicular_bisector(A,B) = {D}
and
|.D-A.| = |.D-B.| & |.D-A.| = |.D-C.| & |.D-B.| = |.D-C.| by A1,Th47;
thus thesis by A2;
end;
uniqueness by ZFMISC_1:3;
end;
definition
let A,B,C being Point of TOP-REAL 2;
assume A,B,C is_a_triangle;
func the_radius_of_the_circumcircle(A,B,C) -> Real equals
:Def4:
|.the_circumcenter(A,B,C)-A.|;
correctness;
end;
theorem Th48:
A,B,C is_a_triangle implies ex a,b,r st A in circle(a,b,r) &
B in circle(a,b,r) & C in circle(a,b,r)
proof
assume A,B,C is_a_triangle;
then consider D such that
the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C) = {D}
and
the_perpendicular_bisector(B,C) /\ the_perpendicular_bisector(C,A) = {D}
and
the_perpendicular_bisector(C,A) /\ the_perpendicular_bisector(A,B) = {D}
and
A1: |.D-A.| = |.D-B.| and
A2: |.D-A.| = |.D-C.| and
|.D-B.| = |.D-C.| by Th47;
take a=D`1,b=D`2,r=|.D-A.|;
A3: D=|[a,b]| by EUCLID:53;
now
|.A-|[a,b]|.|=r by A3,EUCLID_6:43;
hence A in circle(a,b,r) by TOPREAL9:43;
|.B-|[a,b]|.|=r by A1,A3,EUCLID_6:43;
hence B in circle(a,b,r) by TOPREAL9:43;
|.C-|[a,b]|.|=r by A2,A3,EUCLID_6:43;
hence C in circle(a,b,r) by TOPREAL9:43;
end;
hence thesis;
end;
theorem Th49:
A,B,C is_a_triangle & A in circle(a,b,r) & B in circle(a,b,r) &
C in circle(a,b,r)
implies |[a,b]| = the_circumcenter(A,B,C) & r = |.the_circumcenter(A,B,C)-A.|
proof
assume that
A1: A,B,C is_a_triangle and
A2: A in circle(a,b,r) and
A3: B in circle(a,b,r) and
A4: C in circle(a,b,r);
A in {p where p is Point of TOP-REAL 2: |.p - |[a,b]|.| = r}
by A2,JGRAPH_6:def 5;
then consider Ar be Point of TOP-REAL 2 such that
A5: Ar = A and
A6: |.Ar - |[a,b]|.| = r;
B in {p where p is Point of TOP-REAL 2: |.p - |[a,b]|.| = r}
by A3,JGRAPH_6:def 5;
then consider Br be Point of TOP-REAL 2 such that
A7: Br = B and
A8: |.Br - |[a,b]|.| = r;
C in {p where p is Point of TOP-REAL 2: |.p - |[a,b]|.| = r}
by A4,JGRAPH_6:def 5;
then consider Cr be Point of TOP-REAL 2 such that
A9: Cr = C and
A10: |.Cr - |[a,b]|.| = r;
A12: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
A13: |.A - |[a,b]|.| = |.|[a,b]| - B.| &
|.B - |[a,b]|.| = |.|[a,b]| - C.| &
|.C - |[a,b]|.| = |.|[a,b]| - A.| by A5,A6,A7,A8,A9,A10,EUCLID_6:43;
|[a,b]| in the_perpendicular_bisector(A,B) &
|[a,b]| in the_perpendicular_bisector(B,C) &
|[a,b]| in the_perpendicular_bisector(C,A) by A13,A12,EUCLID_6:43,Th45;
then
A20: |[a,b]| in the_perpendicular_bisector(A,B) /\
the_perpendicular_bisector(B,C) &
|[a,b]| in the_perpendicular_bisector(B,C) /\
the_perpendicular_bisector(C,A) &
|[a,b]| in the_perpendicular_bisector(C,A) /\
the_perpendicular_bisector(A,B) by XBOOLE_0:def 4;
A,B,C is_a_triangle & B,C,A is_a_triangle &
C,A,B is_a_triangle by A1,MENELAUS:15;
then
{|[a,b]|} = the_perpendicular_bisector(A,B) /\
the_perpendicular_bisector(B,C) &
{|[a,b]|} = the_perpendicular_bisector(B,C) /\
the_perpendicular_bisector(C,A) &
{|[a,b]|} = the_perpendicular_bisector(C,A) /\
the_perpendicular_bisector(A,B) by A20,Th17,Th46;
hence |[a,b]| = the_circumcenter(A,B,C) by A1,Def3;
hence thesis by A5,A6,EUCLID_6:43;
end;
theorem
A,B,C is_a_triangle implies the_radius_of_the_circumcircle(A,B,C) > 0
proof
assume
A1: A,B,C is_a_triangle;
then
A2: A,B,C are_mutually_distinct by EUCLID_6:20;
assume
A3: the_radius_of_the_circumcircle(A,B,C) <= 0;
A4: |.the_circumcenter(A,B,C)-A.| = 0 by A1,A3,Def4;
consider a,b,r such that
A5: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) by A1,Th48;
A6: r = 0 by A1,A4,A5,Th49;
circle(a,b,0) = {|[a,b]|} by EUCLID10:36;
then A = |[a,b]| & B = |[a,b]| & C = |[a,b]|
by A5,A6,TARSKI:def 1;
hence contradiction by A2;
end;
theorem Th50:
A,B,C is_a_triangle implies
|.the_circumcenter(A,B,C)-A.| = |.the_circumcenter(A,B,C)-B.| &
|.the_circumcenter(A,B,C)-A.| = |.the_circumcenter(A,B,C)-C.| &
|.the_circumcenter(A,B,C)-B.| = |.the_circumcenter(A,B,C)-C.|
proof
assume
A1: A,B,C is_a_triangle;
then consider D such that
A2: the_perpendicular_bisector(A,B) /\ the_perpendicular_bisector(B,C) = {D} &
the_perpendicular_bisector(B,C) /\ the_perpendicular_bisector(C,A) = {D} &
the_perpendicular_bisector(C,A) /\ the_perpendicular_bisector(A,B) = {D}
and
A3: |.D-A.| = |.D-B.| & |.D-A.| = |.D-C.| & |.D-B.| = |.D-C.| by Th47;
the_circumcenter(A,B,C) = D by A1,A2,Def3;
hence thesis by A3;
end;
theorem
A,B,C is_a_triangle implies
the_radius_of_the_circumcircle(A,B,C) = |.the_circumcenter(A,B,C)-B.| &
the_radius_of_the_circumcircle(A,B,C) = |.the_circumcenter(A,B,C)-C.|
proof
assume
A1: A,B,C is_a_triangle;
then |.the_circumcenter(A,B,C)-A.| = |.the_circumcenter(A,B,C)-B.| &
|.the_circumcenter(A,B,C)-A.| = |.the_circumcenter(A,B,C)-C.| by Th50;
hence thesis by A1,Def4;
end;
theorem
A,B,C is_a_triangle &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) &
A in circle(c,d,s) & B in circle(c,d,s) & C in circle(c,d,s)
implies a=c & b=d & r=s
proof
assume that
A1: A,B,C is_a_triangle and
A2: A in circle(a,b,r) and
A3: B in circle(a,b,r) and
A4: C in circle(a,b,r) and
A5: A in circle(c,d,s) and
A6: B in circle(c,d,s) and
A7: C in circle(c,d,s);
A8: |[a,b]| = the_circumcenter(A,B,C) & r = |.the_circumcenter(A,B,C)-A.| &
|[c,d]| = the_circumcenter(A,B,C) & s = |.the_circumcenter(A,B,C)-A.|
by A1,A2,A3,A4,A5,A6,A7,Th49;
|[a,b]|`1 = a & |[a,b]|`2 = b & |[c,d]|`1 = c & |[c,d]|`2 = d by EUCLID:52;
hence thesis by A8;
end;
theorem
r <> s implies circle(a,b,r) misses circle(a,b,s)
proof
assume
A1: r <> s;
per cases;
suppose not r is positive or not s is positive;
then per cases;
suppose
A2: r = 0;
then
A3: circle(a,b,r) = {|[a,b]|} by EUCLID10:36;
assume circle(a,b,r) meets circle(a,b,s);
then consider p be object such that
A4: p in circle(a,b,r) and
A5: p in circle(a,b,s) by XBOOLE_0:3;
p in {p where p is Point of TOP-REAL 2: |.p - |[a,b]|.| = s}
by A5,JGRAPH_6:def 5;
then consider p1 be Point of TOP-REAL 2 such that
A6: p = p1 and
A7: |.p1 - |[a,b]|.| = s;
s = |.|[a,b]| - |[a,b]|.| by A6,A7,A4,A3,TARSKI:def 1
.= 0 by EUCLID_6:42;
hence contradiction by A2,A1;
end;
suppose r < 0 or s < 0;
then circle(a,b,r) is empty or circle(a,b,s) is empty;
hence thesis;
end;
suppose
A8: s = 0;
then
A9: circle(a,b,s) = {|[a,b]|} by EUCLID10:36;
assume circle(a,b,r) meets circle(a,b,s);
then consider p be object such that
A10: p in circle(a,b,s) and
A11: p in circle(a,b,r) by XBOOLE_0:3;
p in {p where p is Point of TOP-REAL 2: |.p - |[a,b]|.| = r}
by A11,JGRAPH_6:def 5;
then consider p1 be Point of TOP-REAL 2 such that
A12: p = p1 and
A13: |.p1 - |[a,b]|.| = r;
r = |.|[a,b]| - |[a,b]|.| by A12,A13,A10,A9,TARSKI:def 1
.= 0 by EUCLID_6:42;
hence contradiction by A8,A1;
end;
end;
suppose
r is positive & s is positive;
assume circle(a,b,r) meets circle(a,b,s);
then consider p be object such that
A15: p in circle(a,b,r) and
A16: p in circle(a,b,s) by XBOOLE_0:3;
p in {p where p is Point of TOP-REAL 2: |. p - |[a,b]|.| = r}
by A15,JGRAPH_6:def 5;
then consider p1 be Point of TOP-REAL 2 such that
A17: p = p1 and
A18: |.p1 - |[a,b]|.| = r;
p in {p where p is Point of TOP-REAL 2: |. p - |[a,b]|.| = s}
by A16,JGRAPH_6:def 5;
then consider p2 be Point of TOP-REAL 2 such that
A19: p = p2 and
A20: |.p2 - |[a,b]|.| = s;
thus contradiction by A17,A19,A18,A1,A20;
end;
end;
begin :: Extended Law of sines
theorem Th51:
A,B,C is_a_triangle &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) &
A,B,D is_a_triangle &
A in circle(a,b,r) & B in circle(a,b,r) & D in circle(a,b,r) &
C <> D implies
the_diameter_of_the_circumcircle(A,B,C)
= the_diameter_of_the_circumcircle(D,B,C) or
the_diameter_of_the_circumcircle(A,B,C)
= - the_diameter_of_the_circumcircle(D,B,C)
proof
assume that
A1: A,B,C is_a_triangle &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) and
A2: A,B,D is_a_triangle &
A in circle(a,b,r) & B in circle(a,b,r) & D in circle(a,b,r) and
A3: C<>D;
A4: B,A,C is_a_triangle by A1,MENELAUS:15;
A5: D,B,C is_a_triangle
proof
A6: now
A,B,D are_mutually_distinct by A2,EUCLID_6:20;
hence D<>B;
A,B,C are_mutually_distinct by A1,EUCLID_6:20;
hence B<>C;
thus D<>C by A3;
end;
then
A7: D,B,C are_mutually_distinct;
now
hereby
assume angle(D,B,C) = PI or angle(B,C,D)=PI or angle(C,D,B)=PI;
then per cases;
suppose angle(D,B,C)=PI; then
A8: B in LSeg(D,C) by EUCLID_6:11;
B in LSeg(D,B) & B<>C by A6,RLTOPSP1:68;
hence contradiction by A6,A1,A2,A8,EUCLID_6:30;
end;
suppose angle(B,C,D)=PI; then
A9: C in LSeg(B,D) by EUCLID_6:11;
C in LSeg(D,C) & C<>D by A3,RLTOPSP1:68;
hence contradiction by A6,A1,A2,A9,EUCLID_6:30;
end;
suppose angle(C,D,B)=PI; then
A10: D in LSeg(C,B) by EUCLID_6:11;
D in LSeg(B,D) & B<>D by A6,RLTOPSP1:68;
hence contradiction by A6,A1,A2,A10,EUCLID_6:30;
end;
end;
end;
hence thesis by A7,EUCLID_6:20;
end;
then
A11: B,D,C is_a_triangle & B,A,C is_a_triangle by A1,MENELAUS:15;
A12: the_diameter_of_the_circumcircle(A,B,C)
= - the_diameter_of_the_circumcircle(B,A,C) &
the_diameter_of_the_circumcircle(D,B,C)
= - the_diameter_of_the_circumcircle(B,D,C) by A1,A5,EUCLID10:47;
now
A,B,C are_mutually_distinct by A1,EUCLID_6:20;
hence A<>B & B<>C & A<>C;
D,B,C are_mutually_distinct by A5,EUCLID_6:20;
hence B<>D & C<>D;
end;
then
A13: angle(B,A,C) = angle(B,D,C) or
angle(B,A,C) = angle(B,D,C) - PI or
angle(B,A,C) = angle(B,D,C) + PI by A1,A2,EUCLID_6:34;
A14: now
assume
A15: sin angle(B,A,C) = sin angle(B,D,C);
thus the_diameter_of_the_circumcircle(A,B,C)
= - the_diameter_of_the_circumcircle(B,A,C) by A1,EUCLID10:47
.= - - |.C-B.| / sin angle(B,A,C) by A4,EUCLID10:45
.= - the_diameter_of_the_circumcircle(B,D,C) by A11,EUCLID10:45,A15
.= the_diameter_of_the_circumcircle(D,B,C) by A5,EUCLID10:47;
end;
now
assume
A16: sin angle(B,A,C) = - sin angle(B,D,C);
thus the_diameter_of_the_circumcircle(A,B,C)
= - the_diameter_of_the_circumcircle(B,A,C) by A1,EUCLID10:47
.= - - |.C-B.| / sin angle(B,A,C) by A11,EUCLID10:45
.= (-|.C-B.|) / sin angle(B,D,C) by A16,XCMPLX_1:192
.= - |.C-B.| / sin angle(B,D,C)
.= the_diameter_of_the_circumcircle(B,D,C) by A11,EUCLID10:45;
end;
hence thesis by A13,Lm2,SIN_COS:79,A14,A12;
end;
theorem Th52:
A,B,C is_a_triangle &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
implies
the_diameter_of_the_circumcircle(A,B,C) = 2 * r or
the_diameter_of_the_circumcircle(A,B,C) = - 2 * r
proof
assume that
A1: A,B,C is_a_triangle and
A2: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
A3: r is positive by A1,A2,EUCLID10:37;
then consider D be Point of TOP-REAL 2 such that
A4: C <> D and
A5: D in circle(a,b,r) and
A6: |[a,b]| in LSeg(C,D) by A2,EUCLID_6:32;
A7: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
per cases;
suppose
A8: D=B;
then
A9: B,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg(B,C)
by A6,A7,A2,A3,EUCLID10:38;
A10: B,A,C is_a_triangle by A1,MENELAUS:15;
A11: the_diameter_of_the_circumcircle(A,B,C)
= - the_diameter_of_the_circumcircle(B,A,C) by A1,EUCLID10:47
.= - (|.C-B.|/sin angle(C,A,B)) by A10,EUCLID10:44;
angle(B,A,C) in ].0,PI.[ or angle(B,A,C) in ].PI,2*PI.[
proof
A12: 0 <= angle(B,A,C) < PI or angle(B,A,C) = PI or
PI < angle(B,A,C) < 2*PI by EUCLID11:3;
0 < angle(B,A,C) < PI or PI < angle(B,A,C) < 2*PI
by A12,A1,EUCLID10:30,A2,A7,EUCLID_6:35;
hence thesis by XXREAL_1:4;
end;
then per cases;
suppose
A13: angle(B,A,C) in ].0,PI.[;
then 0 < angle(B,A,C) < PI & B,A,C are_mutually_distinct
by A7,XXREAL_1:4;
then 0 < angle(A,C,B) < PI by EUCLID11:5;
then
A14: C,A,B is_a_triangle & angle(B,A,C) in ].0,PI.[ &
angle(A,C,B) in ].0,PI.[ & |[a,b]| in LSeg(C,B)
by A13,A1,MENELAUS:15,A6,A8,XXREAL_1:4;
angle(C,A,B) = 2*PI - angle(B,A,C) by A1,EUCLID10:31
.= 2*PI - PI/2 by A14,A2,EUCLID10:39
.= 3*PI/2;
then the_diameter_of_the_circumcircle(A,B,C)
= |.B-C.| by EUCLID_6:43,A11,SIN_COS:77
.= 2*r by A9,A2,A3,EUCLID10:58;
hence thesis;
end;
suppose angle(B,A,C) in ].PI,2*PI.[;
then PI < angle(B,A,C) < 2*PI & B,A,C are_mutually_distinct
by A7,XXREAL_1:4;
then PI < angle(A,C,B) < 2*PI by EUCLID11:2,8;
then 2*PI - angle(A,C,B) < 2*PI - PI & 0 < 2*PI - angle(A,C,B) &
angle(B,C,A) = 2*PI - angle(A,C,B)
by A1,EUCLID10:31,XREAL_1:15,XREAL_1:50;
then 0 < angle(B,C,A) < PI & B,C,A are_mutually_distinct by A7;
then 0 < angle(A,B,C) < PI & 0 < angle(C,A,B) < PI by EUCLID11:5;
then B,A,C is_a_triangle & angle(C,A,B) in ].0,PI.[ &
angle(A,B,C) in ].0,PI.[ & |[a,b]| in LSeg(B,C)
by A1,MENELAUS:15,A6,A8,XXREAL_1:4;
then sin angle(C,A,B) = 1 by SIN_COS:77,A2,EUCLID10:39;
then the_diameter_of_the_circumcircle(A,B,C)
= - |.B-C.| by A11,EUCLID_6:43
.= - 2*r by A9,A2,A3,EUCLID10:58;
hence thesis;
end;
end;
suppose
A15: D<>B;
then
A16: D,B,C are_mutually_distinct by A4,A7;
A17: now
hereby
assume angle(D,B,C) = PI or angle(B,C,D)=PI or angle(C,D,B)=PI;
then per cases;
suppose angle(D,B,C)=PI; then
A18: B in LSeg(D,C) by EUCLID_6:11;
B in LSeg(D,B) & B<>C & B in circle(a,b,r) & C in circle(a,b,r) &
D in circle(a,b,r) by A2,A5,A7,RLTOPSP1:68;
hence contradiction by A15,A18,EUCLID_6:30;
end;
suppose angle(B,C,D)=PI;
then
A19: C in LSeg(B,D) by EUCLID_6:11;
C in LSeg(B,C) & C<>D & B in circle(a,b,r) & C in circle(a,b,r) &
D in circle(a,b,r) by A2,A5,A4,RLTOPSP1:68;
hence contradiction by A7,A19,EUCLID_6:30;
end;
suppose angle(C,D,B)=PI;
then
A20: D in LSeg(C,B) by EUCLID_6:11;
D in LSeg(C,D) & D<>B & B in circle(a,b,r) & C in circle(a,b,r)&
D in circle(a,b,r) by A15,A2,A5,RLTOPSP1:68;
hence contradiction by A4,A20,EUCLID_6:30;
end;
end;
end;
then
A21: D,B,C is_a_triangle by A16,EUCLID_6:20;
per cases;
suppose
A22: A=D;
A23: A,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg(A,C)
by A22,A6,A7,A2,A3,EUCLID10:38;
A24: the_diameter_of_the_circumcircle(A,B,C) = |.C-A.|/sin angle(C,B,A)
by A1,EUCLID10:44;
angle(C,B,A) in ].0,PI.[ or angle(C,B,A) in ].PI,2*PI.[
proof
0 <= angle(C,B,A) < PI or angle(C,B,A) = PI or
PI < angle(C,B,A) < 2*PI by EUCLID11:3;
then 0 < angle(C,B,A) < PI or PI < angle(C,B,A) < 2*PI
by A2,A7,EUCLID_6:35,A1,EUCLID10:30;
hence thesis by XXREAL_1:4;
end;
then per cases;
suppose
A25: angle(C,B,A) in ].0,PI.[;
then 0 < angle(C,B,A) < PI & C,B,A are_mutually_distinct
by A7,XXREAL_1:4;
then 0 < angle(B,A,C) < PI by EUCLID11:5;
then C,B,A is_a_triangle &
angle(C,B,A) in ].0,PI.[ &
angle(B,A,C) in ].0,PI.[ &
|[a,b]| in LSeg(A,C) by A25,A1,MENELAUS:15,A6,A22,XXREAL_1:4;
then the_diameter_of_the_circumcircle(A,B,C)
= |.C-A.| / 1 by A24,A1,A2,EUCLID10:39,SIN_COS:77
.= |.A-C.| by EUCLID_6:43
.= 2*r by A23,A2,A3,EUCLID10:58;
hence thesis;
end;
suppose angle(C,B,A) in ].PI,2*PI.[;
then PI < angle(C,B,A) & ((2*PI <= 2*PI) & angle(C,B,A) < 2*PI)
by XXREAL_1:4;
then
A26: 2*PI - angle(C,B,A) < 2*PI - PI & 0 < 2*PI - angle(C,B,A) &
angle(A,B,C) = 2*PI - angle(C,B,A)
by A1,EUCLID10:31,XREAL_1:15,XREAL_1:50;
then 0 < angle(B,C,A) < PI & 0 < angle(C,A,B) < PI by A7,EUCLID11:5;
then
A27: C,B,A is_a_triangle & angle(A,B,C) in ].0,PI.[ &
angle(B,C,A) in ].0,PI.[ &
|[a,b]| in LSeg(C,A) by A26,XXREAL_1:4,A1,MENELAUS:15,A6,A22;
angle(C,B,A) = 2*PI - angle(A,B,C) by A1,EUCLID10:31
.= 2*PI - PI/2 by A27,A2,EUCLID10:39
.= 3*PI/2;
then the_diameter_of_the_circumcircle(A,B,C)
= |.C-A.| / (-1) by A1,EUCLID10:44,SIN_COS:77
.= -|.C-A.|
.= -|.A-C.| by EUCLID_6:43
.= - 2*r by A23,A2,A3,EUCLID10:58;
hence thesis;
end;
end;
suppose
A28: A <> D;
then
A29: A,B,D are_mutually_distinct by A15,A7;
A30: D,B,C are_mutually_distinct by A15,A4,A7;
A31: D,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg(D,C)
by A6,A5,A4,A2,A3,EUCLID10:38;
A32: angle(C,B,D) in ].0,PI.[ or angle(C,B,D) in ].PI,2*PI.[
proof
0 <= angle(C,B,D) < PI or angle(C,B,D) = PI or
PI < angle(C,B,D) < 2*PI by EUCLID11:3;
then 0 < angle(C,B,D) < PI or PI < angle(C,B,D) < 2*PI
by A21,EUCLID10:30,A5,A2,EUCLID_6:35,A15,A7;
hence thesis by XXREAL_1:4;
end;
now
hereby
assume angle(A,B,D) = PI or angle(B,D,A)=PI or angle(D,A,B)=PI;
then per cases;
suppose angle(A,B,D)=PI;
then
A33: B in LSeg(A,D) by EUCLID_6:11;
B in LSeg(A,B) & B<>D & B in circle(a,b,r) & A in circle(a,b,r) &
D in circle(a,b,r) by A2,A5,A15,RLTOPSP1:68;
hence contradiction by A7,A33,EUCLID_6:30;
end;
suppose angle(B,D,A)=PI;
then
A34: D in LSeg(B,A) by EUCLID_6:11;
D in LSeg(B,D) & D<>A & B in circle(a,b,r) & A in circle(a,b,r) &
D in circle(a,b,r) by A2,A5,A28,RLTOPSP1:68;
hence contradiction by A15,A34,EUCLID_6:30;
end;
suppose angle(D,A,B)=PI;
then
A35: A in LSeg(D,B) by EUCLID_6:11;
A in LSeg(D,A) & A<>B & B in circle(a,b,r) & A in circle(a,b,r) &
D in circle(a,b,r) by A2,A5,A7,RLTOPSP1:68;
hence contradiction by A28,A35,EUCLID_6:30;
end;
end;
end;
then A,B,D is_a_triangle & A,B,C is_a_triangle by A29,A1,EUCLID_6:20;
then per cases by A4,A5,A2,Th51;
suppose
A36: the_diameter_of_the_circumcircle(A,B,C)
= the_diameter_of_the_circumcircle(D,B,C);
per cases by A32;
suppose
A37: angle(C,B,D) in ].0,PI.[;
now
thus angle(C,B,D) in ].0,PI.[ by A37;
0 < angle(C,B,D) < PI & C,B,D are_mutually_distinct
by A37,A15,A4,A7,XXREAL_1:4;
then 0 < angle(B,D,C) < PI by EUCLID11:5;
hence angle(B,D,C) in ].0,PI.[ by XXREAL_1:4;
thus |[a,b]| in LSeg(D,C) by A6;
end;
then sin angle(C,B,D) = 1
by SIN_COS:77,A17,A16,EUCLID_6:20,A5,A2,EUCLID10:39;
then the_diameter_of_the_circumcircle(D,B,C)
= |.C-D.|/1 by A17,A16,EUCLID_6:20,EUCLID10:44
.= |.D-C.| by EUCLID_6:43
.= 2 * r by A31,A5,A2,A3,EUCLID10:58;
hence thesis by A36;
end;
suppose angle(C,B,D) in ].PI,2*PI.[;
then PI < angle(C,B,D) & ((2*PI <= 2*PI) & angle(C,B,D) < 2*PI)
by XXREAL_1:4;
then
A38: 2*PI - angle(C,B,D) < 2*PI - PI & 0 < 2*PI - angle(C,B,D) &
angle(D,B,C) = 2*PI - angle(C,B,D)
by A21,EUCLID10:31,XREAL_1:15,XREAL_1:50;
0 < angle(B,C,D) < PI & 0 < angle(C,D,B) < PI
by A38,A30,EUCLID11:5;
then
A39: C,B,D is_a_triangle & angle(D,B,C) in ].0,PI.[ &
angle(B,C,D) in ].0,PI.[ & |[a,b]| in LSeg(C,D)
by A38,XXREAL_1:4,A21,MENELAUS:15,A6;
A40: angle(C,B,D) = 2*PI - angle(D,B,C) by A21,EUCLID10:31
.= 2*PI - PI/2 by A39,A5,A2,EUCLID10:39
.= 3*PI/2;
the_diameter_of_the_circumcircle(D,B,C)
= |.C-D.|/sin angle(C,B,D) by A17,A16,EUCLID_6:20,EUCLID10:44
.= -|.C-D.|/1 by A40,SIN_COS:77
.= -|.D-C.| by EUCLID_6:43
.= - 2*r by A31,A5,A2,A3,EUCLID10:58;
hence thesis by A36;
end;
end;
suppose
A41: the_diameter_of_the_circumcircle(A,B,C)
= - the_diameter_of_the_circumcircle(D,B,C);
per cases by A32;
suppose
A42: angle(C,B,D) in ].0,PI.[;
A43: now
thus angle(C,B,D) in ].0,PI.[ by A42;
0 < angle(C,B,D) < PI & C,B,D are_mutually_distinct
by A42,A15,A4,A7,XXREAL_1:4;
then 0 < angle(B,D,C) < PI by EUCLID11:5;
hence angle(B,D,C) in ].0,PI.[ by XXREAL_1:4;
thus |[a,b]| in LSeg(D,C) by A6;
end;
the_diameter_of_the_circumcircle(D,B,C)
= |.C-D.| / sin(angle(C,B,D)) by A17,A16,EUCLID_6:20,EUCLID10:44
.= |.C-D.|/1
by A43,SIN_COS:77,A17,A16,EUCLID_6:20,A5,A2,EUCLID10:39
.= |.D-C.| by EUCLID_6:43
.= 2 * r by A31,A2,A5,A3,EUCLID10:58;
hence thesis by A41;
end;
suppose angle(C,B,D) in ].PI,2*PI.[;
then PI < angle(C,B,D) & ((2*PI <= 2*PI) & angle(C,B,D) < 2*PI)
by XXREAL_1:4;
then
A44: 2*PI - angle(C,B,D) < 2*PI - PI & 0 < 2*PI - angle(C,B,D) &
angle(D,B,C) = 2*PI - angle(C,B,D)
by A21,EUCLID10:31,XREAL_1:15,XREAL_1:50;
then 0 < angle(B,C,D) < PI & 0 < angle(C,D,B) < PI
by A30,EUCLID11:5;
then
A45: C,B,D is_a_triangle & angle(D,B,C) in ].0,PI.[ &
angle(B,C,D) in ].0,PI.[ & |[a,b]| in LSeg(C,D)
by XXREAL_1:4,A44,A21,MENELAUS:15,A6;
A46: angle(C,B,D) = 2*PI - angle(D,B,C) by A21,EUCLID10:31
.= 2*PI - PI/2 by A45,A5,A2,EUCLID10:39
.= 3*PI/2;
the_diameter_of_the_circumcircle(D,B,C)
= |.C-D.| / (-1)
by A46,SIN_COS:77,A17,A16,EUCLID_6:20,EUCLID10:44
.= -|.C-D.|
.= -|.D-C.| by EUCLID_6:43
.= - 2*r by A31,A5,A2,A3,EUCLID10:58;
hence thesis by A41;
end;
end;
end;
end;
end;
theorem Th53:
A,B,C is_a_triangle & 0 < angle(C,B,A) < PI implies
the_diameter_of_the_circumcircle(A,B,C) > 0
proof
assume that
A1: A,B,C is_a_triangle and
A2: 0 < angle(C,B,A) < PI;
A,B,C are_mutually_distinct by A1,EUCLID_6:20; then
A3: |.C-A.| >=0 & |.C-A.| <> 0 by EUCLID_6:42;
2 * PI * 0 < angle(C,B,A) & angle(C,B,A) < PI + 2 * PI * 0 by A2;
then sin(angle(C,B,A)) > 0 & |.C-A.| > 0 by A3,SIN_COS6:11;
then |.C-A.| / sin(angle(C,B,A)) > 0 by XREAL_1:139;
hence thesis by A1,EUCLID10:44;
end;
theorem Th54:
A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI implies
the_diameter_of_the_circumcircle(A,B,C) < 0
proof
assume that
A1: A,B,C is_a_triangle and
A2: PI < angle(C,B,A) < 2 * PI;
A,B,C are_mutually_distinct by A1,EUCLID_6:20;
then
A3: |.C-A.| >=0 & |.C-A.| <> 0 by EUCLID_6:42;
PI + 2 * PI * 0 < angle(C,B,A) & angle(C,B,A) < 2 * PI + 2 * PI * 0 by A2;
then |.C-A.| / sin(angle(C,B,A)) < 0 by XREAL_1:142,A3,SIN_COS6:12;
hence thesis by A1,EUCLID10:44;
end;
theorem Th55:
A,B,C is_a_triangle & 0 < angle(C,B,A) < PI &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) implies
the_diameter_of_the_circumcircle(A,B,C) = 2 * r
proof
assume that
A1: A,B,C is_a_triangle and
A2: 0 < angle(C,B,A) < PI and
A3: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
A4: the_diameter_of_the_circumcircle(A,B,C) = 2 * r or
the_diameter_of_the_circumcircle(A,B,C) = - 2 * r by A1,A3,Th52;
r > 0 by A1,A3,EUCLID10:37;
hence thesis by A1,A2,Th53,A4;
end;
theorem Th56:
A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) implies
the_diameter_of_the_circumcircle(A,B,C) = - 2 * r
proof
assume that
A1: A,B,C is_a_triangle and
A2: PI < angle(C,B,A) < 2 * PI and
A3: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
A4: the_diameter_of_the_circumcircle(A,B,C) = 2 * r or
the_diameter_of_the_circumcircle(A,B,C) = - 2 * r by A1,A3,Th52;
r > 0 by A1,A3,EUCLID10:37;
hence thesis by A1,A2,Th54,A4;
end;
theorem Th57:
A,B,C is_a_triangle & 0 < angle(C,B,A) < PI &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
implies
|.A-B.| = 2 * r * sin angle(A,C,B) &
|.B-C.| = 2 * r * sin angle(B,A,C) &
|.C-A.| = 2 * r * sin angle(C,B,A)
proof
assume that
A1: A,B,C is_a_triangle and
A2: 0 < angle(C,B,A) < PI and
A3: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
the_diameter_of_the_circumcircle(A,B,C) = 2 * r by A1,A2,A3,Th55;
hence thesis by A1,EUCLID10:50;
end;
theorem Th58:
A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
implies
|.A-B.| = - 2 * r * sin angle(A,C,B) &
|.B-C.| = - 2 * r * sin angle(B,A,C) &
|.C-A.| = - 2 * r * sin angle(C,B,A)
proof
assume that
A1: A,B,C is_a_triangle and
A2: PI < angle(C,B,A) < 2 * PI and
A3: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
the_diameter_of_the_circumcircle(A,B,C) = - 2 * r by A1,A2,A3,Th56;
then |.A-B.| = (- 2 * r) * sin angle(A,C,B) &
|.B-C.| = (- 2 * r) * sin angle(B,A,C) &
|.C-A.| = (- 2 * r) * sin angle(C,B,A) by A1,EUCLID10:50;
hence thesis;
end;
::$N Extended law of sines
theorem
A,B,C is_a_triangle & 0 < angle(C,B,A) < PI &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
implies
|.A-B.| / sin angle(A,C,B) = 2 * r &
|.B-C.| / sin angle(B,A,C) = 2 * r &
|.C-A.| / sin angle(C,B,A) = 2 * r
proof
assume that
A1: A,B,C is_a_triangle and
A2: 0 < angle(C,B,A) < PI and
A3: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
A,B,C are_mutually_distinct by A1,EUCLID_6:20; then
A4: C,B,A are_mutually_distinct & B,A,C are_mutually_distinct;
2 * PI * 0 < angle(C,B,A) & angle(C,B,A) < PI + 2 * PI * 0 by A2; then
A5: sin(angle(C,B,A)) > 0 by SIN_COS6:11;
2 * PI * 0 < angle(B,A,C) & angle(B,A,C) < PI + 2 * PI * 0
by A2,A4,EUCLID11:5; then
A6: sin(angle(B,A,C)) > 0 by SIN_COS6:11;
2 * PI * 0 < angle(A,C,B) & angle(A,C,B) < PI + 2 * PI * 0
by A2,A4,EUCLID11:5; then
A7: sin(angle(A,C,B)) > 0 by SIN_COS6:11;
|.A-B.| / sin angle(A,C,B) = (2 * r) * sin angle(A,C,B) / sin angle(A,C,B)
&
|.B-C.| / sin angle(B,A,C) = (2 * r) * sin angle(B,A,C) / sin angle(B,A,C)
&
|.C-A.| / sin angle(C,B,A) = (2 * r) * sin angle(C,B,A) / sin angle(C,B,A)
by A1,A2,A3,Th57;
hence thesis by A5,A6,A7,XCMPLX_1:89;
end;
theorem
A,B,C is_a_triangle & PI < angle(C,B,A) < 2 * PI &
A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r)
implies
|.A-B.| / sin angle(A,C,B) = - 2 * r &
|.B-C.| / sin angle(B,A,C) = - 2 * r &
|.C-A.| / sin angle(C,B,A) = - 2 * r
proof
assume that
A1: A,B,C is_a_triangle and
A2: PI < angle(C,B,A) < 2 * PI and
A3: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r);
A,B,C are_mutually_distinct by A1,EUCLID_6:20;
then
A4: C,B,A are_mutually_distinct & B,A,C are_mutually_distinct;
PI + 2 * PI * 0 < angle(C,B,A) & angle(C,B,A) < 2 * PI + 2 * PI * 0 by A2;
then
A5: sin(angle(C,B,A)) < 0 by SIN_COS6:12;
PI + 2 * PI * 0 < angle(B,A,C) &
angle(B,A,C) < 2 * PI + 2 * PI * 0 by A2,A4,EUCLID11:8,EUCLID11:2;
then
A6: sin(angle(B,A,C)) < 0 by SIN_COS6:12;
PI + 2 * PI * 0 < angle(A,C,B) & angle(A,C,B) < 2 * PI + 2 * PI * 0
by A2,A4,EUCLID11:2,8; then
A7: sin(angle(A,C,B)) < 0 by SIN_COS6:12;
|.A-B.| = -(2 * r) * sin angle(A,C,B) &
|.B-C.| = -(2 * r) * sin angle(B,A,C) &
|.C-A.| = -(2 * r) * sin angle(C,B,A) by A1,A2,A3,Th58;
then |.A-B.| / sin angle(A,C,B) = -(2 * r) * sin angle(A,C,B) /
sin angle(A,C,B) & |.B-C.| / sin angle(B,A,C) = -(2 * r) *
sin angle(B,A,C) / sin angle(B,A,C) & |.C-A.| / sin angle(C,B,A) =
-(2 * r) * sin angle(C,B,A) / sin angle(C,B,A);
hence thesis by A5,A6,A7,XCMPLX_1:89;
end;
begin :: The centroid of a triangle
theorem Th59:
A,B,C is_a_triangle &
D = (1-1/2) * B + 1/2 * C &
E = (1-1/2) * C + 1/2 * A &
F = (1-1/2) * A + 1/2 * B
implies Line(A,D),Line(B,E),Line(C,F) are_concurrent
proof
assume that
A1: A,B,C is_a_triangle and
A2: D = (1-1/2) * B + 1/2 * C and
A3: E = (1-1/2) * C + 1/2 * A and
A4: F = (1-1/2) * A + 1/2 * B;
set lambda = 1/2;
set mu = 1/2;
set nu = 1/2;
(lambda/(1-lambda)) * (mu/(1-mu)) * (nu/(1-nu)) =1;
hence thesis by A1,A2,A3,A4,MENELAUS:22;
end;
definition
let A,B,C be Point of TOP-REAL 2;
func median(A,B,C) -> Element of line_of_REAL 2 equals
Line(A,the_midpoint_of_the_segment(B,C));
coherence
proof
reconsider rA=A,rB=the_midpoint_of_the_segment(B,C) as Element of REAL 2
by EUCLID:22;
Line(rA,rB) = Line(A,the_midpoint_of_the_segment(B,C)) by Th4;
then Line(A,the_midpoint_of_the_segment(B,C)) in the set of all
Line(x1,x2) where x1,x2 is Element of REAL 2;
hence thesis by EUCLIDLP:def 4;
end;
end;
theorem Th60:
median(A,A,A)={A}
proof
reconsider rA=A as Element of REAL 2 by EUCLID:22;
Line(rA,rA) = Line(A,A) by Th4;
then Line(A,A) = {A} by Th3;
hence thesis by Th24;
end;
theorem
median(A,A,B)=Line(A,B)
proof
per cases;
suppose
A1: A <> B;
the_midpoint_of_the_segment(A,B) in LSeg(A,B) by Th21;
then the_midpoint_of_the_segment(A,B) in Line(A,B) & A in Line(A,B) &
the_midpoint_of_the_segment(A,B) <> A
by A1,Th25,MENELAUS:12,RLTOPSP1:72;
hence thesis by RLTOPSP1:75;
end;
suppose
A2: A=B;
reconsider rA=A as Element of REAL 2 by EUCLID:22;
A3: Line(rA,rA)=Line(A,B) by Th4,A2;
Line(rA,rA) = {A} by Th3;
hence thesis by A2,A3,Th60;
end;
end;
theorem
median(A,B,A)=Line(A,B)
proof
per cases;
suppose
A1: A <> B;
the_midpoint_of_the_segment(B,A) in LSeg(B,A) by Th21;
then the_midpoint_of_the_segment(B,A) in Line(B,A) & A in Line(B,A) &
the_midpoint_of_the_segment(B,A) <> A
by A1,Th26,MENELAUS:12,RLTOPSP1:72;
hence thesis by RLTOPSP1:75;
end;
suppose
A2: A=B;
reconsider rA=A as Element of REAL 2 by EUCLID:22;
A3: Line(rA,rA)=Line(A,B) by Th4,A2;
Line(rA,rA) = {A} by Th3;
hence thesis by A2,A3,Th60;
end;
end;
theorem
median(B,A,A)=Line(A,B) by Th24;
theorem Th61:
A,B,C is_a_triangle implies median(A,B,C) is being_line
proof
assume
A1: A,B,C is_a_triangle;
A2: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
assume not median(A,B,C) is being_line;
then consider x such that
A3: median(A,B,C)={x} by Th6;
set D = the_midpoint_of_the_segment(B,C);
A in median(A,B,C) & D in median(A,B,C) by EUCLID_4:41;
then A = x & D = x by A3,TARSKI:def 1;
then A in LSeg(B,C) & LSeg(B,C) c= Line(B,C) by Th21,RLTOPSP1:73;
hence contradiction by A1,A2,MENELAUS:13;
end;
theorem Th62:
A,B,C is_a_triangle implies ex D st D in median(A,B,C) & D in median(B,C,A) &
D in median(C,A,B)
proof
assume
A1: A,B,C is_a_triangle;
set D = the_midpoint_of_the_segment(B,C);
set E = the_midpoint_of_the_segment(C,A);
set F = the_midpoint_of_the_segment(A,B);
A2: now
thus the_midpoint_of_the_segment(B,C) = 1/2 * (B+C) by Th22
.= (1-1/2) * B + 1/2 * C
by RLVECT_1:def 5;
thus the_midpoint_of_the_segment(C,A) = 1/2 * (C+A) by Th22
.= (1-1/2) * C + 1/2 * A
by RLVECT_1:def 5;
thus the_midpoint_of_the_segment(A,B) = 1/2 * (A+B) by Th22
.= (1-1/2) * A + 1/2 * B
by RLVECT_1:def 5;
end;
then
A3: Line(A,D),Line(B,E),Line(C,F) are_concurrent by A1,Th59;
reconsider rA=A,rD=D,rB=B,rC=C,rE=E,rF=F as Element of REAL 2 by EUCLID:22;
Line(rA,rD)=Line(A,D) &
Line(rB,rE)=Line(B,E) &
Line(rC,rF)=Line(C,F) by Th4;
then reconsider LAD = Line(A,D),LBE=Line(B,E),
LCF=Line(C,F) as Subset of REAL 2;
now
assume
A5: Line(A,D) is_parallel_to Line(B,E) &
Line(B,E) is_parallel_to Line(C,F) &
Line(C,F) is_parallel_to Line(A,D);
F=(1-1/2)*A+1/2*B &
D=(1-1/2)*B+1/2*C &
(1-1/2)+1/2*1/2 <> 0 & C,A,B is_a_triangle by A1,A2,MENELAUS:15;
hence contradiction by A5,MENELAUS:16;
end;
hence thesis by A3,MENELAUS:def 1;
end;
theorem Th63:
A,B,C is_a_triangle implies ex D st
median(A,B,C) /\ median(B,C,A) = {D} &
median(B,C,A) /\ median(C,A,B) = {D} &
median(C,A,B) /\ median(A,B,C) = {D}
proof
assume
A1: A,B,C is_a_triangle;
then consider D such that
A2: D in median(A,B,C) and
A3: D in median(B,C,A) and
A4: D in median(C,A,B) by Th62;
A5: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
reconsider rA=A,rB=B,rC=C,
rBC=the_midpoint_of_the_segment(B,C),
rCA=the_midpoint_of_the_segment(C,A),
rAB=the_midpoint_of_the_segment(A,B) as Element of REAL 2 by EUCLID:22;
reconsider L1 = Line(rA,rBC), L2 = Line(rB,rCA), L3 = Line(rC,rAB) as
Element of line_of_REAL 2 by EUCLIDLP:47;
A6: B,C,A is_a_triangle & C,B,A is_a_triangle by A1,MENELAUS:15;
A7: C,A,B is_a_triangle by A1,MENELAUS:15;
A8: L1 = Line(A,the_midpoint_of_the_segment(B,C)) &
L2 = Line(B,the_midpoint_of_the_segment(C,A)) &
L3 = Line(C,the_midpoint_of_the_segment(A,B)) by Th4;
then
A9: L1 is being_line & L2 is being_line & L3 is being_line
by A1,A2,A3,A4,A6,A7,Th61;
D in L1 & D in L2 & D in L3 by A2,A3,A4,Th4;
then
A10: D in L1/\L2 & D in L1/\L3 & D in L2/\L3 by XBOOLE_0:def 4;
now
L1 <> L2
proof
assume
A11: L1 = L2;
A12: A in Line(A,the_midpoint_of_the_segment(B,C)) &
the_midpoint_of_the_segment(B,C) in
Line(A,the_midpoint_of_the_segment(B,C)) &
B in Line(B,the_midpoint_of_the_segment(C,A)) &
the_midpoint_of_the_segment(C,A) in
Line(B,the_midpoint_of_the_segment(C,A)) &
C in Line(C,the_midpoint_of_the_segment(A,B)) &
the_midpoint_of_the_segment(A,B) in
Line(C,the_midpoint_of_the_segment(A,B))
by RLTOPSP1:72;
A in L1 & B in L1 & A in L2 & B in L2 &
the_midpoint_of_the_segment(B,C) in L1 &
the_midpoint_of_the_segment(B,C) in L2 &
the_midpoint_of_the_segment(C,A) in L1 &
the_midpoint_of_the_segment(C,A) in L2
by A12,A11,Th4;
then L1 = Line(rA,rB) by A5,A9,EUCLIDLP:30;
then
A13: L1 = Line(A,B) by Th4;
B<>the_midpoint_of_the_segment(B,C) & B in L1 &
the_midpoint_of_the_segment(B,C) in LSeg(B,C) &
the_midpoint_of_the_segment(B,C) in L1 & L1 is being_line
by A2,A8,A1,Th61,RLTOPSP1:72,A11,Th21,A5,Th25;
then A in L1 & B in L1 & C in L1 by A12,Th4,Th5;
then C,A,B are_collinear by A13,A5,MENELAUS:13;
hence contradiction by A1,MENELAUS:15;
end;
hence not L1 // L2 by A10,XBOOLE_0:4,EUCLIDLP:71;
thus L1 is being_line & L2 is being_line & not L1 is being_point &
not L2 is being_point by A8,A1,A2,A3,A6,Th61,Th7;
end;
then consider x such that
A14: L1/\L2 = {x} by Th16;
now
L1 <> L3
proof
assume
A15: L1 = L3;
A16: A in Line(A,the_midpoint_of_the_segment(B,C)) &
the_midpoint_of_the_segment(B,C) in
Line(A,the_midpoint_of_the_segment(B,C)) &
B in Line(B,the_midpoint_of_the_segment(C,A)) &
the_midpoint_of_the_segment(C,A) in
Line(B,the_midpoint_of_the_segment(C,A)) &
C in Line(C,the_midpoint_of_the_segment(A,B)) &
the_midpoint_of_the_segment(A,B) in
Line(C,the_midpoint_of_the_segment(A,B))
by RLTOPSP1:72;
A in L1 & C in L1 & A in L3 & C in L3 &
the_midpoint_of_the_segment(B,C) in L1 &
the_midpoint_of_the_segment(B,C) in L3 &
the_midpoint_of_the_segment(A,B) in L1 &
the_midpoint_of_the_segment(A,B) in L3
by A15,Th4,A16;
then L1 = Line(rA,rC) by A5,A9,EUCLIDLP:30;
then
A17: L1 = Line(A,C) by Th4;
A<>the_midpoint_of_the_segment(A,B) & A in L1 &
the_midpoint_of_the_segment(A,B) in LSeg(A,B) &
the_midpoint_of_the_segment(A,B) in L1 & L1 is being_line
by A2,A5,Th25,A8,A1,Th61,A15,RLTOPSP1:72,Th21;
then A in L1 & C in L1 & B in L1 by A16,A15,Th4,Th5;
then B,A,C are_collinear by A17,A5,MENELAUS:13;
hence contradiction by A1,MENELAUS:15;
end;
hence not L1 // L3 by A10,XBOOLE_0:4,EUCLIDLP:71;
thus L1 is being_line & L3 is being_line & not L1 is being_point &
not L3 is being_point by A2,A4,A8,A1,A7,Th61,Th7;
end;
then consider y such that
A18: L1/\L3 = {y} by Th16;
now
L2 <> L3
proof
assume
A19: L2 = L3;
A20: A in Line(A,the_midpoint_of_the_segment(B,C)) &
the_midpoint_of_the_segment(B,C) in
Line(A,the_midpoint_of_the_segment(B,C)) &
B in Line(B,the_midpoint_of_the_segment(C,A)) &
the_midpoint_of_the_segment(C,A) in
Line(B,the_midpoint_of_the_segment(C,A)) &
C in Line(C,the_midpoint_of_the_segment(A,B)) &
the_midpoint_of_the_segment(A,B) in
Line(C,the_midpoint_of_the_segment(A,B))
by RLTOPSP1:72;
then B in L2 & C in L2 & B in L3 & C in L3 & rCA in L2 & rAB in L2
& rCA in L3 & rAB in L3 by A19,Th4;
then L2 = Line(rB,rC) by A5,A9,EUCLIDLP:30;
then
A21: L2 = Line(B,C) by Th4;
C<>the_midpoint_of_the_segment(C,A) & C in L2 &
the_midpoint_of_the_segment(C,A) in LSeg(C,A) &
the_midpoint_of_the_segment(C,A) in L2 & L2 is being_line
by A3,A5,Th25,RLTOPSP1:72,A19,Th21,A6,Th61,A8;
then B in L2 & C in L2 & A in L2 by A20,Th4,Th5;
hence contradiction by A21,A5,A1,MENELAUS:13;
end;
hence not L2 // L3 by A10,XBOOLE_0:4,EUCLIDLP:71;
thus L2 is being_line & L3 is being_line & not L2 is being_point &
not L3 is being_point by A3,A4,A8,A6,A7,Th61,Th7;
end;
then consider z such that
A22: L2/\L3 = {z} by Th16;
D=x & D=y & D=z by A10,A14,A18,A22,TARSKI:def 1;
hence thesis by A14,A18,A22,A8;
end;
definition
let A,B,C be Point of TOP-REAL 2;
assume
A1: A,B,C is_a_triangle;
func the_centroid_of_the_triangle(A,B,C) -> Point of TOP-REAL 2 means
median(A,B,C) /\ median(B,C,A) = {it} &
median(B,C,A) /\ median(C,A,B) = {it} &
median(C,A,B) /\ median(A,B,C) = {it};
existence by A1,Th63;
uniqueness by ZFMISC_1:3;
end;