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:6;
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 2;
then A4: Rotate (c2,(- (Arg c1))) = (|.c2.| * (cos (((2 * PI) * 1) + ((- (Arg c1)) + (Arg c2))))) + ((|.c2.| * (sin ((- (Arg c1)) + (Arg c2)))) * <i>) by COMPLEX2:9
.= (|.c2.| * (cos ((2 * PI) + ((- (Arg c1)) + (Arg c2))))) + ((|.c2.| * (sin (((2 * PI) * 1) + ((- (Arg c1)) + (Arg c2))))) * <i>) by COMPLEX2:8 ;
( 0 <= Arg c2 & Arg c1 <= 2 * PI ) by COMPTRIG:34;
then (Arg c1) + 0 <= (2 * PI) + (Arg c2) by XREAL_1:7;
then A5: (Arg c1) - (Arg c1) <= ((2 * PI) + (Arg c2)) - (Arg c1) by XREAL_1:9;
A6: |.(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)))) = ((2 * PI) - (Arg c1)) + (Arg c2) by A4, A5, A3, A6, COMPTRIG:def 1; :: thesis: verum