let p1, p2, p3, p be Point of (TOP-REAL 2); ( p in LSeg (p1,p2) & p1,p2,p3 is_a_triangle & angle (p1,p3,p2) = angle (p,p3,p2) implies p = p1 )
assume A1:
p in LSeg (p1,p2)
; ( not p1,p2,p3 is_a_triangle or not angle (p1,p3,p2) = angle (p,p3,p2) or p = p1 )
assume A2:
p1,p2,p3 is_a_triangle
; ( not angle (p1,p3,p2) = angle (p,p3,p2) or p = p1 )
then A3:
angle (p3,p1,p2) <> PI
by Th20;
A4:
p1,p2,p3 are_mutually_distinct
by A2, Th20;
then
p1 <> p2
by ZFMISC_1:def 5;
then A5:
euc2cpx p2 <> euc2cpx p1
by EUCLID_3:4;
A6:
not p3 in LSeg (p1,p2)
by A2, TOPREAL9:67;
( not p1 in LSeg (p2,p3) & not p2 in LSeg (p3,p1) )
by A2, TOPREAL9:67;
then A7:
p1,p3,p2 is_a_triangle
by A6, TOPREAL9:67;
p2 <> p3
by A4, ZFMISC_1:def 5;
then A8:
|.(p2 - p3).| <> 0
by Lm1;
A9:
p2 <> p3
by A4, ZFMISC_1:def 5;
then A10:
euc2cpx p3 <> euc2cpx p2
by EUCLID_3:4;
assume A11:
angle (p1,p3,p2) = angle (p,p3,p2)
; p = p1
angle (p2,p3,p1) <> PI
by A2, Th20;
then A12:
angle (p,p3,p2) <> PI
by A11, COMPLEX2:82;
A13:
p <> p3
by A1, A2, TOPREAL9:67;
then A14:
euc2cpx p <> euc2cpx p3
by EUCLID_3:4;
p1 <> p3
by A4, ZFMISC_1:def 5;
then A15:
euc2cpx p3 <> euc2cpx p1
by EUCLID_3:4;
A16:
angle (p1,p2,p3) <> PI
by A2, Th20;
A17:
p <> p2
proof
assume
p = p2
;
contradiction
then
angle (
p1,
p3,
p2)
= 0
by A11, COMPLEX2:79;
then
( (
angle (
p3,
p2,
p1)
= 0 &
angle (
p2,
p1,
p3)
= PI ) or (
angle (
p3,
p2,
p1)
= PI &
angle (
p2,
p1,
p3)
= 0 ) )
by A10, A15, A5, COMPLEX2:87;
hence
contradiction
by A16, A3, COMPLEX2:82;
verum
end;
then A18:
angle (p3,p2,p1) = angle (p3,p2,p)
by A1, Th10;
then A19:
angle (p3,p2,p) <> PI
by A16, COMPLEX2:82;
A20:
p,p3,p2 are_mutually_distinct
by A9, A17, A13, ZFMISC_1:def 5;
A21:
euc2cpx p <> euc2cpx p2
by A17, EUCLID_3:4;
A22:
angle (p2,p1,p3) = angle (p2,p,p3)
proof
per cases
( ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) )
by A10, A15, A5, A14, A21, COMPLEX2:88;
suppose
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI )
;
angle (p2,p1,p3) = angle (p2,p,p3)end; suppose
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5
* PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5
* PI )
;
angle (p2,p1,p3) = angle (p2,p,p3)end; suppose A23:
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5
* PI )
;
angle (p2,p1,p3) = angle (p2,p,p3)
(
angle (
p2,
p1,
p3)
>= 0 &
- (angle (p2,p,p3)) > - (2 * PI) )
by COMPLEX2:70, XREAL_1:24;
then A24:
(angle (p2,p1,p3)) + (- (angle (p2,p,p3))) > 0 + (- (2 * PI))
by XREAL_1:8;
(angle (p2,p1,p3)) - (angle (p2,p,p3)) = - (4 * PI)
by A11, A18, A23;
then
4
* PI < 2
* PI
by A24, XREAL_1:24;
then
(4 * PI) / PI < (2 * PI) / PI
by XREAL_1:74;
then
4
< (2 * PI) / PI
by XCMPLX_1:89;
then
4
< 2
by XCMPLX_1:89;
hence
angle (
p2,
p1,
p3)
= angle (
p2,
p,
p3)
;
verum end; suppose A25:
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5
* PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI )
;
angle (p2,p1,p3) = angle (p2,p,p3)
(
angle (
p2,
p1,
p3)
< 2
* PI &
angle (
p2,
p,
p3)
>= 0 )
by COMPLEX2:70;
then
(angle (p2,p1,p3)) + (- (angle (p2,p,p3))) < (2 * PI) + (- 0)
by XREAL_1:8;
then
(4 * PI) / PI < (2 * PI) / PI
by A11, A18, A25, XREAL_1:74;
then
4
< (2 * PI) / PI
by XCMPLX_1:89;
then
4
< 2
by XCMPLX_1:89;
hence
angle (
p2,
p1,
p3)
= angle (
p2,
p,
p3)
;
verum end; end;
end;
then
angle (p2,p,p3) <> PI
by A3, COMPLEX2:82;
then
p,p3,p2 is_a_triangle
by A20, A12, A19, Th20;
then
|.(p2 - p3).| * |.(p - p2).| = |.(p1 - p2).| * |.(p2 - p3).|
by A7, A11, A22, Th21;
then
|.(p - p2).| = |.(p1 - p2).|
by A8, XCMPLX_1:5;
then A26: |.(p2 - p).| =
|.(p1 - p2).|
by Lm2
.=
|.(p2 - p1).|
by Lm2
;
assume A27:
p1 <> p
; contradiction
A28: |.(p2 - p1).| ^2 =
((|.(p1 - p).| ^2) + (|.(p2 - p).| ^2)) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * (cos (angle (p1,p,p2))))
by Th7
.=
((|.(p1 - p).| ^2) + (|.(p2 - p).| ^2)) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * (- 1))
by A1, A27, A17, Th8, SIN_COS:77
;