let a be Element of COMPLEX ; :: thesis: for r being Real holds Rotate (- a),r = - (Rotate a,r)
let r be Real; :: thesis: Rotate (- a),r = - (Rotate a,r)

per cases ( a <> 0c or a = 0c ) ;

suppose A1: a <> 0c ; :: thesis: Rotate (- a),r = - (Rotate a,r)

A2: ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) )

proof

per cases ( Arg a < PI or Arg a >= PI ) ;

suppose Arg a < PI ; :: thesis: ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) )

then Arg (- a) = PI + (Arg a) by A1, Th22;
then r + (Arg (- a)) = PI + (r + (Arg a)) ;
hence ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) by SIN_COS:84; :: thesis: verum

end;

suppose Arg a >= PI ; :: thesis: ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) )

then Arg (- a) = (Arg a) - PI by A1, Th22;
then r + (Arg (- a)) = ((Arg a) + r) - PI ;
hence ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) by Th6; :: thesis: verum

end;

end;

end;

|.a.| = |.(- a).| by COMPLEX1:138;
hence Rotate (- a),r = - (Rotate a,r) by A2; :: thesis: verum

end;

suppose A3: a = 0c ; :: thesis: Rotate (- a),r = - (Rotate a,r)

hence Rotate (- a),r = - 0 by Th66
.= - (Rotate a,r) by A3, Th66 ;
:: thesis: verum

end;

end;