let c1, c2 be Element of COMPLEX ; :: thesis: ( c2 <> 0 & (Arg c2) - (Arg c1) >= 0 implies Arg (Rotate c2,(- (Arg c1))) = (Arg c2) - (Arg c1) )
assume A1: ( c2 <> 0 & (Arg c2) - (Arg c1) >= 0 ) ; :: thesis: Arg (Rotate c2,(- (Arg c1))) = (Arg c2) - (Arg c1)
set z = Rotate c2,(- (Arg c1));
set a = (- (Arg c1)) + (Arg c2);
Rotate c2,(- (Arg c1)) = (|.c2.| * (cos ((- (Arg c1)) + (Arg c2)))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i> ) by COMPLEX2:def 4;
then A2: Rotate c2,(- (Arg c1)) = (|.c2.| * (cos ((- (Arg c1)) + (Arg c2)))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i> ) ;
( Arg c2 < 2 * PI & 0 <= Arg c1 ) by COMPTRIG:52;
then (Arg c2) + 0 < (2 * PI ) + (Arg c1) by XREAL_1:10;
then A3: (Arg c2) - (Arg c1) < ((2 * PI ) + (Arg c1)) - (Arg c1) by XREAL_1:11;
A4: |.(Rotate c2,(- (Arg c1))).| = |.c2.| by COMPLEX2:67;
then Rotate c2,(- (Arg c1)) <> 0 by A1, COMPLEX1:130, COMPLEX1:131;
hence Arg (Rotate c2,(- (Arg c1))) = (Arg c2) - (Arg c1) by A1, A2, A3, A4, COMPTRIG:def 1; :: thesis: verum