let c1, c2 be Complex; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum