let a, b, c be Complex; :: thesis: for r being Real st a <> b & b <> c holds
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))
let r be Real; :: thesis: ( a <> b & b <> c implies angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) )
set cb = c - b;
set ab = a - b;
set rc = Rotate (c,r);
set rb = Rotate (b,r);
set ra = Rotate (a,r);
set rcb = (Rotate (c,r)) - (Rotate (b,r));
set rab = (Rotate (a,r)) - (Rotate (b,r));
assume that
A1: a <> b and
A2: b <> c ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))
A3: ( 0 <= angle (a,b,c) & angle (a,b,c) < 2 * PI ) by Th68;
c - b <> 0 by A2;
then consider cbi being Integer such that
A4: Arg (Rotate ((c - b),r)) = ((2 * PI) * cbi) + (r + (Arg (c - b))) by Th52;
a - b <> 0 by A1;
then consider abi being Integer such that
A5: Arg (Rotate ((a - b),r)) = ((2 * PI) * abi) + (r + (Arg (a - b))) by Th52;
A6: ( 0 <= angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) & angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) < 2 * PI ) by Th68;
(Rotate (a,r)) - (Rotate (b,r)) = Rotate ((a - b),r) by Th57;
then A7: (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) = ((((2 * PI) * cbi) + r) + (Arg (c - b))) - ((((2 * PI) * abi) + r) + (Arg (a - b))) by A5, A4, Th57
.= ((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi)) ;

per cases ( (Arg (c - b)) - (Arg (a - b)) >= 0 or (Arg (c - b)) - (Arg (a - b)) < 0 ) ;

suppose (Arg (c - b)) - (Arg (a - b)) >= 0 ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

then A8: angle (a,b,c) = (Arg (c - b)) - (Arg (a - b)) by Def4;
thus angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) :: thesis: verum

proof

per cases ( (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 or (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ) ;

suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) by Def4;
hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A7, A8, Th2; :: thesis: verum

end;

suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = (((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))) + (2 * PI) by A7, Def4
.= ((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * ((cbi - abi) + 1)) ;
hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A8, Th2; :: thesis: verum

end;

end;

end;

end;

suppose (Arg (c - b)) - (Arg (a - b)) < 0 ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

then A9: angle (a,b,c) = (2 * PI) + ((Arg (c - b)) - (Arg (a - b))) by Def4;
thus angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) :: thesis: verum

proof

per cases ( (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 or (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ) ;

suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = ((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * ((cbi - abi) + (- 1))) by A7, Def4;
hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A9, Th2; :: thesis: verum

end;

suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ; :: thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = (((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))) + (2 * PI) by A7, Def4
.= ((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * (cbi - abi)) ;
hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A9, Th2; :: thesis: verum

end;

end;

end;

end;

end;