let a be Element of COMPLEX ; :: thesis: Rotate a,PI = - a
A1: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i> ) by Th19;
A2: |.a.| * (- (sin (Arg a))) = - (|.a.| * (sin (Arg a)))
.= - (Im a) by A1, COMPLEX1:28 ;
A3: |.a.| * (- (cos (Arg a))) = - (|.a.| * (cos (Arg a)))
.= - (Re a) by A1, COMPLEX1:28 ;
thus Rotate a,PI = (|.a.| * (- (cos (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i> ) by SIN_COS:84
.= (|.a.| * (- (cos (Arg a)))) + ((|.a.| * (- (sin (Arg a)))) * <i> ) by SIN_COS:84
.= - a by A3, A2, COMPLEX1:def 11 ; :: thesis: verum