let r be Real; :: thesis: for a being Complex holds
( Rotate (a,r) = 0 iff a = 0 )
let a be Complex; :: thesis: ( Rotate (a,r) = 0 iff a = 0 )
hereby :: thesis: ( a = 0 implies Rotate (a,r) = 0 )
assume Rotate (a,r) = 0 ; :: thesis: a = 0
then A1: Rotate (a,r) = 0 + (0 * <i>) ;
per cases ( |.a.| = 0 or ( cos (r + (Arg a)) = 0 & sin (r + (Arg a)) = 0 ) ) by A1, COMPLEX1:77;
suppose ( cos (r + (Arg a)) = 0 & sin (r + (Arg a)) = 0 ) ; :: thesis: a = 0
hence a = 0 by Th10; :: thesis: verum
end;
end;
end;
assume a = 0 ; :: thesis: Rotate (a,r) = 0
hence Rotate (a,r) = 0 by COMPLEX1:44; :: thesis: verum