let a, b, c be Complex; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum