let p1, p2, p3, p be Point of (TOP-REAL 2); ( p in LSeg (p1,p2) & not p3 in LSeg (p1,p2) & angle (p1,p3,p2) > PI & p <> p2 implies angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A1:
p in LSeg (p1,p2)
; ( p3 in LSeg (p1,p2) or not angle (p1,p3,p2) > PI or not p <> p2 or angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A2:
not p3 in LSeg (p1,p2)
; ( not angle (p1,p3,p2) > PI or not p <> p2 or angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A3:
angle (p1,p3,p2) > PI
; ( not p <> p2 or angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A4:
p <> p2
; angle (p,p3,p2) >= angle (p1,p3,p2)
assume A5:
angle (p,p3,p2) < angle (p1,p3,p2)
; contradiction
per cases
( p = p1 or p1 = p2 or ( p1 <> p2 & p <> p1 ) )
;
suppose
p = p1
;
contradictionhence
contradiction
by A5;
verum end; suppose A7:
(
p1 <> p2 &
p <> p1 )
;
contradictionthen A8:
euc2cpx p2 <> euc2cpx p1
by EUCLID_3:4;
A9:
euc2cpx p <> euc2cpx p2
by A4, EUCLID_3:4;
A10:
angle (
p3,
p2,
p1)
= angle (
p3,
p2,
p)
by A1, A4, Th10;
A11:
euc2cpx p <> euc2cpx p1
by A7, EUCLID_3:4;
A12:
euc2cpx p <> euc2cpx p3
by A1, A2, EUCLID_3:4;
A13:
p3 <> p1
by A2, RLTOPSP1:68;
then A14:
euc2cpx p3 <> euc2cpx p1
by EUCLID_3:4;
A15:
p3 <> p2
by A2, RLTOPSP1:68;
then A16:
euc2cpx p3 <> euc2cpx p2
by EUCLID_3:4;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (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 A16, A14, A8, A12, A9, 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 (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (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 (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))end; suppose A17:
(
((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 (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))A18:
(
angle (
p1,
p3,
p2)
>= 0 &
angle (
p2,
p1,
p3)
>= 0 )
by COMPLEX2:70;
angle (
p2,
p,
p3)
< 2
* PI
by COMPLEX2:70;
then A19:
- (angle (p2,p,p3)) > - (2 * PI)
by XREAL_1:24;
angle (
p,
p3,
p2)
< 2
* PI
by COMPLEX2:70;
then
- (angle (p,p3,p2)) > - (2 * PI)
by XREAL_1:24;
then
(- (angle (p,p3,p2))) + (- (angle (p2,p,p3))) > (- (2 * PI)) + (- (2 * PI))
by A19, XREAL_1:8;
then
((angle (p1,p3,p2)) + (angle (p2,p1,p3))) + ((- (angle (p,p3,p2))) - (angle (p2,p,p3))) > (0 + 0) + ((- (2 * PI)) - (2 * PI))
by A18, XREAL_1:8;
hence
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
by A10, A17;
verum end; suppose A20:
(
((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 (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
(
angle (
p2,
p1,
p3)
< 2
* PI &
angle (
p1,
p3,
p2)
< 2
* PI )
by COMPLEX2:70;
then A21:
(angle (p2,p1,p3)) + (angle (p1,p3,p2)) < (2 * PI) + (2 * PI)
by XREAL_1:8;
(
angle (
p,
p3,
p2)
>= 0 &
angle (
p2,
p,
p3)
>= 0 )
by COMPLEX2:70;
then
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + ((- (angle (p,p3,p2))) - (angle (p2,p,p3))) < ((2 * PI) + (2 * PI)) + (0 + 0)
by A21, XREAL_1:8;
hence
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
by A10, A20;
verum end; end;
end; then
angle (
p2,
p1,
p3)
< angle (
p2,
p,
p3)
by A5, XREAL_1:8;
then A22:
angle (
p,
p1,
p3)
< angle (
p2,
p,
p3)
by A1, Th9;
per cases
( ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) )
by A1, A4, A14, A12, A11, Th13, COMPLEX2:88;
suppose A23:
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI )
;
contradiction
p1,
p3,
p2 are_mutually_distinct
by A7, A13, A15, ZFMISC_1:def 5;
then
angle (
p2,
p1,
p3)
> PI
by A3, Th24;
then A24:
angle (
p,
p1,
p3)
> PI
by A1, A7, Th9;
p,
p1,
p3 are_mutually_distinct
by A1, A2, A7, A13, ZFMISC_1:def 5;
then
(
angle (
p1,
p3,
p)
> PI &
angle (
p3,
p,
p1)
> PI )
by A24, Th24;
then
(angle (p3,p,p1)) + (angle (p1,p3,p)) > PI + PI
by XREAL_1:8;
then A25:
((angle (p3,p,p1)) + (angle (p1,p3,p))) + (angle (p,p1,p3)) > (2 * PI) + PI
by A24, XREAL_1:8;
1
* PI < 3
* PI
by XREAL_1:68;
hence
contradiction
by A23, A25;
verum end; suppose A26:
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = 3
* PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI )
;
contradictionA27:
(
angle (
p,
p1,
p3)
>= 0 &
angle (
p1,
p3,
p)
>= 0 )
by COMPLEX2:70;
angle (
p2,
p,
p3)
= ((angle (p,p1,p3)) + (angle (p1,p3,p))) + (2 * PI)
by A26;
then
angle (
p2,
p,
p3)
>= 0 + (2 * PI)
by A27, XREAL_1:6;
hence
contradiction
by COMPLEX2:70;
verum end; suppose A28:
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5
* PI )
;
contradiction
(
angle (
p,
p1,
p3)
< 2
* PI &
angle (
p1,
p3,
p)
< 2
* PI )
by COMPLEX2:70;
then
(angle (p,p1,p3)) + (angle (p1,p3,p)) < (2 * PI) + (2 * PI)
by XREAL_1:8;
then
(angle (p2,p,p3)) + (4 * PI) < 0 + (4 * PI)
by A28;
then
angle (
p2,
p,
p3)
< 0
by XREAL_1:6;
hence
contradiction
by COMPLEX2:70;
verum end; suppose
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = 3
* PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5
* PI )
;
contradictionthen
(angle (p2,p,p3)) + (2 * PI) = (angle (p,p1,p3)) + (angle (p1,p3,p))
;
then
(angle (p2,p,p3)) + (2 * PI) < (angle (p2,p,p3)) + (angle (p1,p3,p))
by A22, XREAL_1:6;
then
2
* PI < angle (
p1,
p3,
p)
by XREAL_1:6;
hence
contradiction
by COMPLEX2:70;
verum end; end; end; end;