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 that
A1: c2 <> 0 and
A2: (Arg c2) - (Arg c1) < 0 ; :: thesis: Arg (Rotate c2,(- (Arg c1))) = ((2 * PI ) - (Arg c1)) + (Arg c2)
set a = (- (Arg c1)) + (Arg c2);
A3: ((- (Arg c1)) + (Arg c2)) + (2 * PI ) < 0 + (2 * PI ) by A2, XREAL_1:8;
set z = Rotate c2,(- (Arg c1));
Rotate c2,(- (Arg c1)) = (|.c2.| * (cos ((- (Arg c1)) + (Arg c2)))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i> ) by COMPLEX2:def 4;
then A4: 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 A5: (Arg c1) - (Arg c1) <= ((2 * PI ) + (Arg c2)) - (Arg c1) by XREAL_1:11;
A6: |.(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 A4, A5, A3, A6, COMPTRIG:def 1; :: thesis: verum