let r be Real; :: thesis: for a being complex number holds
( Rotate a,r = 0 iff a = 0 )
let a be complex number ; :: 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:163;

suppose |.a.| = 0 ; :: thesis: a = 0

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

end;

suppose ( cos (r + (Arg a)) = 0 & sin (r + (Arg a)) = 0 ) ; :: thesis: a = 0

hence a = 0 by Th11; :: thesis: verum

end;

end;

end;

assume a = 0 ; :: thesis: Rotate a,r = 0
hence Rotate a,r = 0 by COMPLEX1:130; :: thesis: verum