let a, b, c be Complex; :: thesis: ( a <> b & b <> c & angle (a,b,c) > PI implies ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI ) )
assume that
A1: ( a <> b & b <> c ) and
A2: angle (a,b,c) > PI ; :: thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI )
A3: angle (c,b,a) < PI
proof
assume not angle (c,b,a) < PI ; :: thesis: contradiction
then (angle (a,b,c)) + (angle (c,b,a)) > PI + PI by A2, XREAL_1:8;
hence contradiction by A2, Th78, COMPTRIG:5; :: thesis: verum
end;
A4: (angle (a,b,c)) + (angle (c,b,a)) = (2 * PI) + 0 by A2, Th78, COMPTRIG:5;
then A5: angle (c,b,a) <> 0 by Th68;
A6: 0 <= angle (c,b,a) by Th68;
then angle (b,a,c) > 0 by A1, A5, A3, Th82;
then A7: (angle (c,a,b)) + (angle (b,a,c)) = (2 * PI) + 0 by Th78;
angle (a,c,b) > 0 by A1, A6, A5, A3, Th82;
then (angle (b,c,a)) + (angle (a,c,b)) = (2 * PI) + 0 by Th78;
then ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = (((2 * PI) + (2 * PI)) + (2 * PI)) - (((angle (c,b,a)) + (angle (b,a,c))) + (angle (a,c,b))) by A4, A7;
hence A8: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = ((((2 * PI) + (2 * PI)) + PI) + PI) - PI by A1, A6, A5, A3, Th82
.= 5 * PI ;
:: thesis: ( angle (b,c,a) > PI & angle (c,a,b) > PI )
A9: angle (a,b,c) < 2 * PI by Th68;
angle (b,c,a) < 2 * PI by Th68;
then A10: ( ((2 * PI) + (2 * PI)) + PI = 5 * PI & (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + (2 * PI) ) by A9, XREAL_1:8;
A11: ((2 * PI) + PI) + (2 * PI) = 5 * PI ;
hereby :: thesis: angle (c,a,b) > PI
assume angle (b,c,a) <= PI ; :: thesis: contradiction
then A12: (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + PI by A9, XREAL_1:8;
angle (c,a,b) < 2 * PI by Th68;
hence contradiction by A8, A11, A12, XREAL_1:8; :: thesis: verum
end;
assume angle (c,a,b) <= PI ; :: thesis: contradiction
hence contradiction by A8, A10, XREAL_1:8; :: thesis: verum