let a, b, c be Complex; :: thesis: ( ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) iff ( a <> b & a <> c & b <> c ) )

hereby :: thesis: ( a <> b & a <> c & b <> c & not ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI implies ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI )

assume A1: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) ; :: thesis: ( a <> b & a <> c & b <> c )

per cases ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) by A1;

suppose A2: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI ; :: thesis: ( a <> b & a <> c & b <> c )

thus ( a <> b & a <> c & b <> c ) :: thesis: verum

proof

assume A3: ( not a <> b or not a <> c or not b <> c ) ; :: thesis: contradiction

per cases ( a = b or a = c or b = c ) by A3;

suppose A4: a = b ; :: thesis: contradiction

A5: angle (a,c,a) = 0 by Th77;
( not angle (a,a,c) = 0 or not angle (c,a,a) = 0 ) by A2, A4, Th77, COMPTRIG:5;
hence contradiction by A2, A4, A5, Th78, COMPTRIG:5; :: thesis: verum

end;

suppose A6: a = c ; :: thesis: contradiction

A7: angle (a,b,a) = 0 by Th77;
( not angle (a,a,b) = 0 or not angle (b,a,a) = 0 ) by A2, A6, Th77, COMPTRIG:5;
hence contradiction by A2, A6, A7, Th78, COMPTRIG:5; :: thesis: verum

end;

suppose A8: b = c ; :: thesis: contradiction

A9: angle (b,a,b) = 0 by Th77;
( not angle (a,b,b) = 0 or not angle (b,b,a) = 0 ) by A2, A8, Th77, COMPTRIG:5;
hence contradiction by A2, A8, A9, Th78, COMPTRIG:5; :: thesis: verum

end;

end;

end;

end;

suppose A10: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ; :: thesis: ( a <> b & a <> c & b <> c )

A11: (2 + 2) * PI < 5 * PI by COMPTRIG:5, XREAL_1:68;
then A12: (2 * PI) + (2 * PI) < 5 * PI ;
thus ( a <> b & a <> c & b <> c ) :: thesis: verum

proof

assume A13: ( not a <> b or not a <> c or not b <> c ) ; :: thesis: contradiction

per cases ( a = b or b = c or a = c ) by A13;

suppose a = b ; :: thesis: contradiction

then angle (b,c,a) = 0 by Th77;
then A14: (angle (a,b,c)) + (angle (b,c,a)) < 2 * PI by Th68;
angle (c,a,b) < 2 * PI by Th68;
hence contradiction by A10, A12, A14, XREAL_1:8; :: thesis: verum

end;

suppose A15: b = c ; :: thesis: contradiction

( angle (a,b,c) < 2 * PI & angle (b,c,a) < 2 * PI ) by Th68;
then A16: (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + (2 * PI) by XREAL_1:8;
angle (c,a,b) = 0 by A15, Th77;
hence contradiction by A10, A11, A16; :: thesis: verum

end;

suppose a = c ; :: thesis: contradiction

then angle (a,b,c) = 0 by Th77;
then A17: (angle (a,b,c)) + (angle (b,c,a)) < 2 * PI by Th68;
angle (c,a,b) < 2 * PI by Th68;
hence contradiction by A10, A12, A17, XREAL_1:8; :: thesis: verum

end;

end;

end;

end;

end;

end;

assume that
A18: a <> b and
A19: a <> c and
A20: b <> c ; :: thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI )

per cases ( angle (a,b,c) = 0 or ( 0 <> angle (a,b,c) & angle (a,b,c) < PI ) or ( 0 <> angle (a,b,c) & angle (a,b,c) = PI ) or ( 0 <> angle (a,b,c) & angle (a,b,c) > PI ) ) by XXREAL_0:1;

suppose A21: angle (a,b,c) = 0 ; :: thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI )

(angle (b,c,a)) + (angle (c,a,b)) = PI

proof

per cases ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A18, A19, A20, A21, Th85;

suppose ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) ; :: thesis: (angle (b,c,a)) + (angle (c,a,b)) = PI

hence (angle (b,c,a)) + (angle (c,a,b)) = PI ; :: thesis: verum

end;

suppose ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ; :: thesis: (angle (b,c,a)) + (angle (c,a,b)) = PI

hence (angle (b,c,a)) + (angle (c,a,b)) = PI ; :: thesis: verum

end;

end;

end;

hence ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) by A21; :: thesis: verum

end;

suppose A22: ( 0 <> angle (a,b,c) & angle (a,b,c) < PI ) ; :: thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI )

0 <= angle (a,b,c) by Th68;
hence ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) by A18, A20, A22, Th82; :: thesis: verum

end;

suppose A23: ( 0 <> angle (a,b,c) & angle (a,b,c) = PI ) ; :: thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI )

then angle (b,c,a) = 0 by A18, A20, Th84;
hence ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) by A18, A20, A23, Th84; :: thesis: verum

end;

suppose ( 0 <> angle (a,b,c) & angle (a,b,c) > PI ) ; :: thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI )

hence ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) by A18, A20, Th83; :: thesis: verum

end;

end;