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 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:52;
then (Arg c2) + 0 < (2 * PI ) + (Arg c1) by XREAL_1:10;
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 4, 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 A2, A3, A4, COMPTRIG:def 1; :: thesis: verum