let a be 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, Th12;
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:79; :: 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, Th12;
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 Th5; :: thesis: verum

end;

end;

end;

|.a.| = |.(- a).| by COMPLEX1:52;
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 Th50
.= - (Rotate (a,r)) by A3, Th50 ;
:: thesis: verum

end;

end;