let a, b, c be Complex; ( a <> b & b <> c & angle (a,b,c) > PI implies ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI ) )
assume that
A1:
( a <> b & b <> c )
and
A2:
angle (a,b,c) > PI
; ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI )
A3:
angle (c,b,a) < PI
A4:
(angle (a,b,c)) + (angle (c,b,a)) = (2 * PI) + 0
by A2, Th78, COMPTRIG:5;
then A5:
angle (c,b,a) <> 0
by Th68;
A6:
0 <= angle (c,b,a)
by Th68;
then
angle (b,a,c) > 0
by A1, A5, A3, Th82;
then A7:
(angle (c,a,b)) + (angle (b,a,c)) = (2 * PI) + 0
by Th78;
angle (a,c,b) > 0
by A1, A6, A5, A3, Th82;
then
(angle (b,c,a)) + (angle (a,c,b)) = (2 * PI) + 0
by Th78;
then
((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = (((2 * PI) + (2 * PI)) + (2 * PI)) - (((angle (c,b,a)) + (angle (b,a,c))) + (angle (a,c,b)))
by A4, A7;
hence A8: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) =
((((2 * PI) + (2 * PI)) + PI) + PI) - PI
by A1, A6, A5, A3, Th82
.=
5 * PI
;
( angle (b,c,a) > PI & angle (c,a,b) > PI )
A9:
angle (a,b,c) < 2 * PI
by Th68;
angle (b,c,a) < 2 * PI
by Th68;
then A10:
( ((2 * PI) + (2 * PI)) + PI = 5 * PI & (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + (2 * PI) )
by A9, XREAL_1:8;
A11:
((2 * PI) + PI) + (2 * PI) = 5 * PI
;
hereby angle (c,a,b) > PI
assume
angle (
b,
c,
a)
<= PI
;
contradictionthen A12:
(angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + PI
by A9, XREAL_1:8;
angle (
c,
a,
b)
< 2
* PI
by Th68;
hence
contradiction
by A8, A11, A12, XREAL_1:8;
verum
end;
assume
angle (c,a,b) <= PI
; contradiction
hence
contradiction
by A8, A10, XREAL_1:8; verum