let a, b, c be Complex; ( a <> b & b <> c & 0 < angle (a,b,c) & angle (a,b,c) < PI implies ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI & 0 < angle (b,c,a) & 0 < angle (c,a,b) ) )
assume that
A1:
a <> b
and
A2:
b <> c
and
A3:
0 < angle (a,b,c)
and
A4:
angle (a,b,c) < PI
; ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI & 0 < angle (b,c,a) & 0 < angle (c,a,b) )
A5:
c - b <> 0
by A2;
set r = - (Arg (a + (- b)));
set A = Rotate ((a + (- b)),(- (Arg (a + (- b)))));
set B = Rotate ((c + (- b)),(- (Arg (a + (- b)))));
A6:
Rotate (0c,(- (Arg (a + (- b))))) = 0c
by Th50;
A7:
c + (- b) <> a + (- b)
by A3, Th77;
A8: angle (b,c,a) =
angle ((b + (- b)),(c + (- b)),(a + (- b)))
by Th70
.=
angle (0c,(Rotate ((c + (- b)),(- (Arg (a + (- b)))))),(Rotate ((a + (- b)),(- (Arg (a + (- b)))))))
by A6, A7, A5, Th76
;
A9: angle ((a + (- b)),0c,(c + (- b))) =
angle ((a + (- b)),(b + (- b)),(c + (- b)))
.=
angle (a,b,c)
by Th70
;
A10:
a - b <> 0
by A1;
then A11:
angle ((a + (- b)),0c,(c + (- b))) = angle ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c,(Rotate ((c + (- b)),(- (Arg (a + (- b)))))))
by A6, A5, Th76;
a + (- b) <> 0c
by A1;
then
|.(a + (- b)).| > 0
by COMPLEX1:47;
then A12:
( Im (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0 & Re (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) > 0 )
by COMPLEX1:12, SIN_COS:31;
then A13:
Arg (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0c
by Th19;
then
(Arg ((Rotate ((c + (- b)),(- (Arg (a + (- b)))))) - 0c)) - (Arg ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))) - 0c)) >= 0
by COMPTRIG:34;
then A14:
angle (a,b,c) = Arg (Rotate ((c + (- b)),(- (Arg (a + (- b))))))
by A9, A11, A13, Def4;
A15: angle (c,a,b) =
angle ((c + (- b)),(a + (- b)),(b + (- b)))
by Th70
.=
angle ((Rotate ((c + (- b)),(- (Arg (a + (- b)))))),(Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c)
by A6, A10, A7, Th76
;
hence
((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI
by A3, A4, A9, A11, A12, A14, A8, Lm5; ( 0 < angle (b,c,a) & 0 < angle (c,a,b) )
thus
0 < angle (b,c,a)
by A3, A4, A12, A14, A8, Lm5; 0 < angle (c,a,b)
thus
0 < angle (c,a,b)
by A3, A4, A12, A14, A15, Lm5; verum