let a, b, c be Complex; ( a <> b & b <> c & angle (a,b,c) = PI implies ( angle (b,c,a) = 0 & angle (c,a,b) = 0 ) )
assume that
A1:
a <> b
and
A2:
b <> c
and
A3:
angle (a,b,c) = PI
; ( angle (b,c,a) = 0 & angle (c,a,b) = 0 )
A4:
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)))));
A5:
Rotate (0c,(- (Arg (a + (- b))))) = 0c
by Th50;
A6: angle ((a + (- b)),0c,(c + (- b))) =
angle ((a + (- b)),(b + (- b)),(c + (- b)))
.=
angle (a,b,c)
by Th70
;
A7:
c + (- b) <> a + (- b)
by A3, Th77, COMPTRIG:5;
A8:
a - b <> 0
by A1;
then A9:
angle ((a + (- b)),0c,(c + (- b))) = angle ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c,(Rotate ((c + (- b)),(- (Arg (a + (- b)))))))
by A5, A4, Th76;
a + (- b) <> 0c
by A1;
then
|.(a + (- b)).| > 0
by COMPLEX1:47;
then A10:
( Im (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0 & Re (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) > 0 )
by COMPLEX1:12, SIN_COS:31;
then A11:
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 A12:
angle (a,b,c) = Arg (Rotate ((c + (- b)),(- (Arg (a + (- b))))))
by A6, A9, A11, Def4;
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 A5, A7, A4, Th76
;
hence
angle (b,c,a) = 0
by A3, A10, A12, Lm6; angle (c,a,b) = 0
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 A5, A8, A7, Th76
;
hence
angle (c,a,b) = 0
by A3, A10, A12, Lm6; verum