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 |.a.| = 0 ; :: thesis: a = 0

hence a = 0 by COMPLEX1:45; :: thesis: verum

end;

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