let a, b, c be Complex; :: thesis: ( a <> b & a <> c & b <> c & angle (a,b,c) = 0 & not ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) implies ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
assume that
A1: a <> b and
A2: a <> c and
A3: b <> c and
A4: angle (a,b,c) = 0 ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
per cases ( angle (b,c,a) <> 0 or angle (c,a,b) <> 0 ) by A1, A2, A3, A4, Th81;
suppose A5: angle (b,c,a) <> 0 ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
A6: 0 <= angle (b,c,a) by Th68;
thus ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) :: thesis: verum
proof
per cases ( angle (b,c,a) < PI or angle (b,c,a) = PI or angle (b,c,a) > PI ) by XXREAL_0:1;
suppose angle (b,c,a) < PI ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A2, A3, A4, A5, A6, Th82; :: thesis: verum
end;
suppose angle (b,c,a) = PI ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A2, A3, Th84; :: thesis: verum
end;
suppose angle (b,c,a) > PI ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A2, A3, A4, Th83, COMPTRIG:5; :: thesis: verum
end;
end;
end;
end;
suppose A7: angle (c,a,b) <> 0 ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
A8: 0 <= angle (c,a,b) by Th68;
thus ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) :: thesis: verum
proof
per cases ( angle (c,a,b) < PI or angle (c,a,b) = PI or angle (c,a,b) > PI ) by XXREAL_0:1;
suppose angle (c,a,b) < PI ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A1, A2, A4, A7, A8, Th82; :: thesis: verum
end;
suppose angle (c,a,b) = PI ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A1, A2, Th84; :: thesis: verum
end;
suppose angle (c,a,b) > PI ; :: thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A1, A2, A4, Th83, COMPTRIG:5; :: thesis: verum
end;
end;
end;
end;
end;