let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( |.(p1 - p3).| = |.(p2 - p3).| & p in LSeg p1,p2 & p <> p3 implies ( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) ) )
assume A1:
|.(p1 - p3).| = |.(p2 - p3).|
; :: thesis: ( not p in LSeg p1,p2 or not p <> p3 or ( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) ) )
assume A2:
p in LSeg p1,p2
; :: thesis: ( not p <> p3 or ( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) ) )
assume A3:
p <> p3
; :: thesis: ( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) )
per cases
( p1 = p2 or p1 <> p2 )
;
suppose A4:
p1 = p2
;
:: thesis: ( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) )then
LSeg p1,
p2 = {p1}
by RLTOPSP1:71;
then A5:
(
p = p1 &
p = p2 )
by A2, A4, TARSKI:def 1;
p2 - p1 = 0. (TOP-REAL 2)
by A4, EUCLID:46;
hence
( (
angle p1,
p3,
p = angle p,
p3,
p2 implies
|.(p1 - p).| = |.(p - p2).| ) & (
|.(p1 - p).| = |.(p - p2).| implies
|((p3 - p),(p2 - p1))| = 0 ) & (
|((p3 - p),(p2 - p1))| = 0 implies
angle p1,
p3,
p = angle p,
p3,
p2 ) )
by A5, EUCLID_2:54;
:: thesis: verum end; suppose
p1 <> p2
;
:: thesis: ( ( angle p1,p3,p = angle p,p3,p2 implies |.(p1 - p).| = |.(p - p2).| ) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) )thus
(
angle p1,
p3,
p = angle p,
p3,
p2 implies
|.(p1 - p).| = |.(p - p2).| )
:: thesis: ( ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) & ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 ) )proof
assume A6:
angle p1,
p3,
p = angle p,
p3,
p2
;
:: thesis: |.(p1 - p).| = |.(p - p2).|
A7:
|.(p - p1).| ^2 =
((|.(p1 - p3).| ^2 ) + (|.(p - p3).| ^2 )) - (((2 * |.(p1 - p3).|) * |.(p - p3).|) * (cos (angle p1,p3,p)))
by Th7
.=
((|.(p - p3).| ^2 ) + (|.(p2 - p3).| ^2 )) - (((2 * |.(p - p3).|) * |.(p2 - p3).|) * (cos (angle p,p3,p2)))
by A1, A6
.=
|.(p2 - p).| ^2
by Th7
;
thus |.(p1 - p).| =
|.(p - p1).|
by Lm2
.=
sqrt (|.(p2 - p).| ^2 )
by A7, SQUARE_1:89
.=
|.(p2 - p).|
by SQUARE_1:89
.=
|.(p - p2).|
by Lm2
;
:: thesis: verum
end; thus
(
|.(p1 - p).| = |.(p - p2).| implies
|((p3 - p),(p2 - p1))| = 0 )
:: thesis: ( |((p3 - p),(p2 - p1))| = 0 implies angle p1,p3,p = angle p,p3,p2 )proof
assume A8:
|.(p1 - p).| = |.(p - p2).|
;
:: thesis: |((p3 - p),(p2 - p1))| = 0
per cases
( p = p2 or p <> p2 )
;
suppose A10:
p <> p2
;
:: thesis: |((p3 - p),(p2 - p1))| = 0 then A11:
|.(p2 - p).| <> 0
by Lm1;
|.(p1 - p).| <> 0
by A8, A10, Lm1;
then A12:
p <> p1
by Lm1;
A13:
|.(p3 - p).| <> 0
by A3, Lm1;
A14:
|.(p3 - p1).| ^2 = ((|.(p1 - p).| ^2 ) + (|.(p3 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p3 - p).|) * (cos (angle p1,p,p3)))
by Th7;
A15:
|.(p2 - p3).| ^2 = ((|.(p3 - p).| ^2 ) + (|.(p2 - p).| ^2 )) - (((2 * |.(p3 - p).|) * |.(p2 - p).|) * (cos (angle p3,p,p2)))
by Th7;
A16:
|.(p3 - p1).| = |.(p2 - p3).|
by A1, Lm2;
A17:
|.(p1 - p).| = |.(p2 - p).|
by A8, Lm2;
then
((2 * |.(p1 - p).|) * (cos (angle p1,p,p3))) * |.(p3 - p).| = ((2 * |.(p2 - p).|) * (cos (angle p3,p,p2))) * |.(p3 - p).|
by A14, A15, A16;
then
(2 * (cos (angle p1,p,p3))) * |.(p2 - p).| = (2 * (cos (angle p3,p,p2))) * |.(p2 - p).|
by A13, A17, XCMPLX_1:5;
then A18:
2
* (cos (angle p1,p,p3)) = 2
* (cos (angle p3,p,p2))
by A11, XCMPLX_1:5;
A19:
cos (angle p1,p,p3) = - (cos (angle p3,p,p2))
proof
per cases
( (angle p1,p,p3) + (angle p3,p,p2) = PI or (angle p1,p,p3) + (angle p3,p,p2) = 3 * PI )
by A2, A10, A12, Th13;
suppose
(angle p1,p,p3) + (angle p3,p,p2) = 3
* PI
;
:: thesis: cos (angle p1,p,p3) = - (cos (angle p3,p,p2))hence cos (angle p1,p,p3) =
cos ((PI - (angle p3,p,p2)) + (2 * PI ))
.=
cos (PI + (- (angle p3,p,p2)))
by SIN_COS:84
.=
- (cos (- (angle p3,p,p2)))
by SIN_COS:84
.=
- (cos (angle p3,p,p2))
by SIN_COS:34
;
:: thesis: verum end;
end;
(
0 <= angle p3,
p,
p2 &
angle p3,
p,
p2 < 2
* PI )
by COMPLEX2:84;
then
(
angle p3,
p,
p2 = PI / 2 or
angle p3,
p,
p2 = (3 / 2) * PI )
by A18, A19, COMPTRIG:34;
then
|((p3 - p),(p2 - p))| = 0
by A3, A10, EUCLID_3:54;
hence
|((p3 - p),(p2 - p1))| = 0
by A2, A10, Th17;
:: thesis: verum end;
end; thus
(
|((p3 - p),(p2 - p1))| = 0 implies
angle p1,
p3,
p = angle p,
p3,
p2 )
:: thesis: verumproof
assume A20:
|((p3 - p),(p2 - p1))| = 0
;
:: thesis: angle p1,p3,p = angle p,p3,p2
then A21:
0 =
- |((p3 - p),(p2 - p1))|
.=
|((p3 - p),(- (p2 - p1)))|
by EUCLID_2:44
.=
|((p3 - p),(p1 - p2))|
by EUCLID:48
;
per cases
( ( p2 = p & p1 = p ) or p1 <> p or p2 <> p )
;
suppose A22:
p1 <> p
;
:: thesis: angle p1,p3,p = angle p,p3,p2then
|((p3 - p),(p1 - p))| = 0
by A2, A21, Th17;
then
(
angle p3,
p,
p1 = PI / 2 or
angle p3,
p,
p1 = (3 / 2) * PI )
by A3, A22, EUCLID_3:54;
hence
angle p1,
p3,
p = angle p,
p3,
p2
by A1, A2, A3, A22, Th18;
:: thesis: verum end; suppose A23:
p2 <> p
;
:: thesis: angle p1,p3,p = angle p,p3,p2then
|((p3 - p),(p2 - p))| = 0
by A2, A20, Th17;
then
(
angle p3,
p,
p2 = PI / 2 or
angle p3,
p,
p2 = (3 / 2) * PI )
by A3, A23, EUCLID_3:54;
then A24:
angle p2,
p3,
p = angle p,
p3,
p1
by A1, A2, A3, A23, Th18;
per cases
( angle p2,p3,p = 0 or angle p2,p3,p <> 0 )
;
suppose A26:
angle p2,
p3,
p <> 0
;
:: thesis: angle p1,p3,p = angle p,p3,p2then
angle p,
p3,
p2 = (2 * PI ) - (angle p2,p3,p)
by EUCLID_3:46;
hence
angle p1,
p3,
p = angle p,
p3,
p2
by A24, A26, EUCLID_3:46;
:: thesis: verum end; end;
end; end;