euclid12.miz
begin
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 ::
EUCLID12:1
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 ::
EUCLID12:2
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 ::
EUCLID12:3
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 ::
EUCLID12:4
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 be
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 be
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 ::
EUCLID12:5
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 be
Nat;
let S be
Subset of (
REAL n);
::
EUCLID12:def1
attr S is
being_point means ex Pn be
Element of (
REAL n) st S
=
{Pn};
end
theorem ::
EUCLID12:6
Th6: Ln is
being_line or ex Pn be
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 be
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 ::
EUCLID12:7
Ln is
being_line or Ln is
being_point by
Th6;
theorem ::
EUCLID12:8
Th7: Ln is
being_line implies not ex Pn be
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 ::
EUCLID12:9
Ln is
being_line implies not Ln is
being_point by
Th7;
begin
reserve A,B,C for
Point of (
TOP-REAL 2);
theorem ::
EUCLID12:10
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 ;
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 ::
EUCLID12:11
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 ::
EUCLID12:12
Th10: for p,q1,q2 be
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 ::
EUCLID12:13
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 ::
EUCLID12:14
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
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 ::
EUCLID12:15
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 be
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 ::
EUCLID12:16
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 be
Subset of (
REAL 2) : ex x1,x2,x3 be
Element of (
REAL 2) st P
= (
plane (x1,x2,x3)) };
hence thesis by
EUCLIDLP:def 11;
end;
theorem ::
EUCLID12:17
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 ::
EUCLID12:18
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 ::
EUCLID12:19
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 ::
EUCLID12:20
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;
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 ::
EUCLID12:21
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 ::
EUCLID12:22
Th17: (L1
/\ L2) is
being_point & A
in (L1
/\ L2) implies (L1
/\ L2)
=
{A} by
TARSKI:def 1;
begin
definition
let A,B be
Point of (
TOP-REAL 2);
::
EUCLID12:def2
func
half_length (A,B) ->
Real equals ((1
/ 2)
*
|.(A
- B).|);
correctness ;
end
theorem ::
EUCLID12:23
(
half_length (A,B))
= (
half_length (B,A)) by
EUCLID_6: 43;
theorem ::
EUCLID12:24
(
half_length (A,A))
=
0
proof
(
half_length (A,A))
= ((1
/ 2)
*
0 ) by
EUCLID_6: 42;
hence thesis;
end;
theorem ::
EUCLID12:25
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 ::
EUCLID12:26
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 ::
EUCLID12:27
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 be
Point of (
TOP-REAL 2);
::
EUCLID12:def3
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 ::
EUCLID12:28
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 ::
EUCLID12:29
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 ::
EUCLID12:30
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 ::
EUCLID12:31
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 ::
EUCLID12:32
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 ::
EUCLID12:33
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 ::
EUCLID12:34
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 ::
EUCLID12:35
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 ::
EUCLID12:36
|.(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 ::
EUCLID12:37
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 ::
EUCLID12:38
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
theorem ::
EUCLID12:39
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 ::
EUCLID12:40
L1
_|_ L2 implies L1
meets L2 by
Th31,
EUCLIDLP: 109;
theorem ::
EUCLID12:41
L1 is
being_line & L2 is
being_line & L1
misses L2 implies L1
// L2 by
Th31,
EUCLIDLP: 113;
theorem ::
EUCLID12:42
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 ::
EUCLID12:43
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 ::
EUCLID12:44
L1
_|_ L2 implies (L1
/\ L2) is
being_point by
Th33;
theorem ::
EUCLID12:45
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 ::
EUCLID12:46
L1 is
being_line & L2 is
being_line & L1
// L2 implies not L1
_|_ L2 by
Th34;
theorem ::
EUCLID12:47
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 ::
EUCLID12:48
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 ::
EUCLID12:49
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 ::
EUCLID12:50
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 ::
EUCLID12:51
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
theorem ::
EUCLID12:52
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 be
Element of (
TOP-REAL 2);
assume
A1: A
<> B;
::
EUCLID12:def4
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 ::
EUCLID12:53
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 ::
EUCLID12:54
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 ::
EUCLID12:55
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 ::
EUCLID12:56
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 ::
EUCLID12:57
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 ::
EUCLID12:58
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 ::
EUCLID12:59
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 ::
EUCLID12:60
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;
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
theorem ::
EUCLID12:61
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 ::
EUCLID12:62
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 be
Point of (
TOP-REAL 2);
assume
A1: (A,B,C)
is_a_triangle ;
::
EUCLID12:def5
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 be
Point of (
TOP-REAL 2);
assume (A,B,C)
is_a_triangle ;
::
EUCLID12:def6
func
the_radius_of_the_circumcircle (A,B,C) ->
Real equals
:
Def4:
|.((
the_circumcenter (A,B,C))
- A).|;
correctness ;
end
theorem ::
EUCLID12:63
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 ::
EUCLID12:64
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 be
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 be
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 be
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 ::
EUCLID12:65
(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 ::
EUCLID12:66
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 ::
EUCLID12:67
(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 ::
EUCLID12:68
(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 ::
EUCLID12:69
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;
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 be
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 be
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 be
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 be
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
theorem ::
EUCLID12:70
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 ;
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 ::
EUCLID12:71
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;
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,
EUCLID11: 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 ;
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;
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 ;
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;
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 ::
EUCLID12:72
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 ::
EUCLID12:73
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 ::
EUCLID12:74
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 ::
EUCLID12:75
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 ::
EUCLID12:76
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 ::
EUCLID12:77
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;
::$Notion-Name
theorem ::
EUCLID12:78
(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 ::
EUCLID12:79
(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,
EUCLID11: 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
theorem ::
EUCLID12:80
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);
::
EUCLID12:def7
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 be
Element of (
REAL 2);
hence thesis by
EUCLIDLP:def 4;
end;
end
theorem ::
EUCLID12:81
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 ::
EUCLID12:82
(
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 ::
EUCLID12:83
(
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 ::
EUCLID12:84
(
median (B,A,A))
= (
Line (A,B)) by
Th24;
theorem ::
EUCLID12:85
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 ::
EUCLID12:86
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 ::
EUCLID12:87
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 ;
::
EUCLID12:def8
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