let c1, c2 be Complex; ( c2 <> 0 & (Arg c2) - (Arg c1) >= 0 implies Arg (Rotate (c2,(- (Arg c1)))) = (Arg c2) - (Arg c1) )
assume that
A1:
c2 <> 0
and
A2:
(Arg c2) - (Arg c1) >= 0
; Arg (Rotate (c2,(- (Arg c1)))) = (Arg c2) - (Arg c1)
set a = (- (Arg c1)) + (Arg c2);
set z = Rotate (c2,(- (Arg c1)));
( Arg c2 < 2 * PI & 0 <= Arg c1 )
by COMPTRIG:34;
then
(Arg c2) + 0 < (2 * PI) + (Arg c1)
by XREAL_1:8;
then A3:
( Rotate (c2,(- (Arg c1))) = (|.c2.| * (cos ((- (Arg c1)) + (Arg c2)))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i>) & (Arg c2) - (Arg c1) < ((2 * PI) + (Arg c1)) - (Arg c1) )
by COMPLEX2:def 2, XREAL_1:9;
A4:
|.(Rotate (c2,(- (Arg c1)))).| = |.c2.|
by COMPLEX2:53;
then
Rotate (c2,(- (Arg c1))) <> 0
by A1, COMPLEX1:44, COMPLEX1:45;
hence
Arg (Rotate (c2,(- (Arg c1)))) = (Arg c2) - (Arg c1)
by A2, A3, A4, COMPTRIG:def 1; verum