let a, b, c be Complex; :: thesis: ( 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 ; :: thesis: ( ((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; :: thesis: ( 0 < angle (b,c,a) & 0 < angle (c,a,b) )
thus 0 < angle (b,c,a) by A3, A4, A12, A14, A8, Lm5; :: thesis: 0 < angle (c,a,b)
thus 0 < angle (c,a,b) by A3, A4, A12, A14, A15, Lm5; :: thesis: verum