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;