let c1, c2 be Element of COMPLEX ; :: thesis: ( c2 <> 0 & (Arg c2) - (Arg c1) < 0 implies Arg (Rotate c2,(- (Arg c1))) = ((2 * PI ) - (Arg c1)) + (Arg c2) )
assume A1: ( c2 <> 0 & (Arg c2) - (Arg c1) < 0 ) ; :: thesis: Arg (Rotate c2,(- (Arg c1))) = ((2 * PI ) - (Arg c1)) + (Arg c2)
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 Rotate c2,(- (Arg c1)) = (|.c2.| * (cos ((- (Arg c1)) + (Arg c2)))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i> ) ;
then A2: Rotate c2,(- (Arg c1)) = (|.c2.| * (cos (((2 * PI ) * 1) + ((- (Arg c1)) + (Arg c2))))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i> ) by COMPLEX2:10
.= (|.c2.| * (cos ((2 * PI ) + ((- (Arg c1)) + (Arg c2))))) + ((|.c2.| * (sin (((2 * PI ) * 1) + ((- (Arg c1)) + (Arg c2))))) * <i> ) by COMPLEX2:9 ;
( 0 <= Arg c2 & Arg c1 <= 2 * PI ) by COMPTRIG:52;
then (Arg c1) + 0 <= (2 * PI ) + (Arg c2) by XREAL_1:9;
then A3: (Arg c1) - (Arg c1) <= ((2 * PI ) + (Arg c2)) - (Arg c1) by XREAL_1:11;
A4: ((- (Arg c1)) + (Arg c2)) + (2 * PI ) < 0 + (2 * PI ) by A1, XREAL_1:8;
A5: |.(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))) = ((2 * PI ) - (Arg c1)) + (Arg c2) by A2, A3, A4, A5, COMPTRIG:def 1; :: thesis: verum