let a, b, c be Element of 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);
A1: (Rotate a,r) - (Rotate b,r) = Rotate (a - b),r by Th73;
assume ( a <> b & b <> c ) ; :: thesis: angle a,b,c = angle (Rotate a,r),(Rotate b,r),(Rotate c,r)
then A2: ( a - b <> 0 & c - b <> 0 ) ;
then consider abi being Integer such that
A3: Arg (Rotate (a - b),r) = ((2 * PI ) * abi) + (r + (Arg (a - b))) by Th68;
consider cbi being Integer such that
A4: Arg (Rotate (c - b),r) = ((2 * PI ) * cbi) + (r + (Arg (c - b))) by A2, Th68;
A5: ( 0 <= angle a,b,c & angle a,b,c < 2 * PI ) by Th84;
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 Th84;
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 A1, A3, A4, Th73
.= ((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 Def6;
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 Def6;
hence angle a,b,c = angle (Rotate a,r),(Rotate b,r),(Rotate c,r) by A5, A6, A7, A8, Th3; :: 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, Def6
.= ((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 A5, A6, A8, Th3; :: 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 Def6;
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, Def6;
hence angle a,b,c = angle (Rotate a,r),(Rotate b,r),(Rotate c,r) by A5, A6, A9, Th3; :: 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, Def6
.= ((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 A5, A6, A9, Th3; :: thesis: verum

end;

end;

end;

end;

end;