let a, b, c be Element of 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 Th66;
A6: angle (a + (- b)),0c ,(c + (- b)) = angle (a + (- b)),(b + (- b)),(c + (- b))
.= angle a,b,c by Th86 ;
A7: c + (- b) <> a + (- b) by A3, Th93, COMPTRIG:21;
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, Th92;
a + (- b) <> 0c by A1;
then |.(a + (- b)).| > 0 by COMPLEX1:133;
then A10: ( Im (Rotate (a + (- b)),(- (Arg (a + (- b))))) = 0 & Re (Rotate (a + (- b)),(- (Arg (a + (- b))))) > 0 ) by COMPLEX1:28, SIN_COS:34;
then A11: Arg (Rotate (a + (- b)),(- (Arg (a + (- b))))) = 0c by Th34;
then (Arg ((Rotate (c + (- b)),(- (Arg (a + (- b))))) - 0c )) - (Arg ((Rotate (a + (- b)),(- (Arg (a + (- b))))) - 0c )) >= 0 by COMPTRIG:52;
then A12: angle a,b,c = Arg (Rotate (c + (- b)),(- (Arg (a + (- b))))) by A6, A9, A11, Def6;
angle b,c,a = angle (b + (- b)),(c + (- b)),(a + (- b)) by Th86
.= angle 0c ,(Rotate (c + (- b)),(- (Arg (a + (- b))))),(Rotate (a + (- b)),(- (Arg (a + (- b))))) by A5, A7, A4, Th92 ;
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 Th86
.= angle (Rotate (c + (- b)),(- (Arg (a + (- b))))),(Rotate (a + (- b)),(- (Arg (a + (- b))))),0c by A5, A8, A7, Th92 ;
hence angle c,a,b = 0 by A3, A10, A12, Lm6; :: thesis: verum