let z be complex number ; :: thesis: ( z <> 0 iff 0 < |.z.| )
thus ( z <> 0 implies 0 < |.z.| ) :: thesis: ( 0 < |.z.| implies z <> 0 )

proof

assume z <> 0 ; :: thesis: 0 < |.z.|
then ( 0 <= |.z.| & 0 <> |.z.| ) by Th131, Th132;
hence 0 < |.z.| ; :: thesis: verum

end;

thus ( 0 < |.z.| implies z <> 0 ) by Th12, SQUARE_1:82; :: thesis: verum