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)) ;