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;