let p1, p2, p3, p be Point of (TOP-REAL 2); ( |.(p1 - p3).| = |.(p2 - p3).| & p in LSeg (p1,p2) & p <> p3 & p <> p1 & ( angle (p3,p,p1) = PI / 2 or angle (p3,p,p1) = (3 / 2) * PI ) implies angle (p1,p3,p) = angle (p,p3,p2) )
assume A1:
|.(p1 - p3).| = |.(p2 - p3).|
; ( not p in LSeg (p1,p2) or not p <> p3 or not p <> p1 or ( not angle (p3,p,p1) = PI / 2 & not angle (p3,p,p1) = (3 / 2) * PI ) or angle (p1,p3,p) = angle (p,p3,p2) )
then A2:
|.(p3 - p1).| = |.(p2 - p3).|
by Lm2;
assume A3:
p in LSeg (p1,p2)
; ( not p <> p3 or not p <> p1 or ( not angle (p3,p,p1) = PI / 2 & not angle (p3,p,p1) = (3 / 2) * PI ) or angle (p1,p3,p) = angle (p,p3,p2) )
assume that
A4:
p <> p3
and
A5:
p <> p1
; ( ( not angle (p3,p,p1) = PI / 2 & not angle (p3,p,p1) = (3 / 2) * PI ) or angle (p1,p3,p) = angle (p,p3,p2) )
assume A6:
( angle (p3,p,p1) = PI / 2 or angle (p3,p,p1) = (3 / 2) * PI )
; angle (p1,p3,p) = angle (p,p3,p2)
per cases
( p1 = p2 or p1 <> p2 )
;
suppose A8:
p1 <> p2
;
angle (p1,p3,p) = angle (p,p3,p2)per cases
( p <> p2 or p = p2 )
;
suppose A9:
p <> p2
;
angle (p1,p3,p) = angle (p,p3,p2)
p2 <> p3
then A11:
euc2cpx p2 <> euc2cpx p3
by EUCLID_3:4;
p1 <> p3
then A13:
euc2cpx p1 <> euc2cpx p3
by EUCLID_3:4;
A14:
(
euc2cpx p <> euc2cpx p1 &
euc2cpx p <> euc2cpx p3 )
by A4, A5, EUCLID_3:4;
A15:
(
angle (
p1,
p,
p3)
= angle (
p3,
p,
p2) &
euc2cpx p <> euc2cpx p2 )
by A3, A5, A6, A9, Th14, EUCLID_3:4;
A16:
angle (
p3,
p1,
p) =
angle (
p3,
p1,
p2)
by A3, A5, Th10
.=
angle (
p1,
p2,
p3)
by A2, A8, Th16
.=
angle (
p,
p2,
p3)
by A3, A9, Th9
;
A17:
angle (
p,
p3,
p1)
= angle (
p2,
p3,
p)
proof
per cases
( ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5 * PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5 * PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5 * PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5 * PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) )
by A16, A14, A13, A11, A15, COMPLEX2:88;
suppose
( (
((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI &
((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) or (
((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5
* PI &
((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5
* PI ) )
;
angle (p,p3,p1) = angle (p2,p3,p)end; suppose A18:
(
((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI &
((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5
* PI )
;
angle (p,p3,p1) = angle (p2,p3,p)
(
angle (
p2,
p3,
p)
< 2
* PI &
angle (
p,
p3,
p1)
>= 0 )
by COMPLEX2:70;
then A19:
(angle (p2,p3,p)) - (angle (p,p3,p1)) < (2 * PI) - 0
by XREAL_1:14;
(angle (p2,p3,p)) - (angle (p,p3,p1)) = 4
* PI
by A18;
hence
angle (
p,
p3,
p1)
= angle (
p2,
p3,
p)
by A19, XREAL_1:64;
verum end; suppose A20:
(
((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5
* PI &
((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI )
;
angle (p,p3,p1) = angle (p2,p3,p)
(
angle (
p,
p3,
p1)
< 2
* PI &
angle (
p2,
p3,
p)
>= 0 )
by COMPLEX2:70;
then A21:
(angle (p,p3,p1)) - (angle (p2,p3,p)) < (2 * PI) - 0
by XREAL_1:14;
(angle (p,p3,p1)) - (angle (p2,p3,p)) = 4
* PI
by A20;
hence
angle (
p,
p3,
p1)
= angle (
p2,
p3,
p)
by A21, XREAL_1:64;
verum end; end;
end; per cases
( angle (p,p3,p1) = 0 or angle (p,p3,p1) <> 0 )
;
suppose A23:
angle (
p,
p3,
p1)
<> 0
;
angle (p1,p3,p) = angle (p,p3,p2)then
angle (
p1,
p3,
p)
= (2 * PI) - (angle (p,p3,p1))
by EUCLID_3:37;
hence
angle (
p1,
p3,
p)
= angle (
p,
p3,
p2)
by A17, A23, EUCLID_3:37;
verum end; end; end; end; end; end;