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.| by Th131;
hence 0 < |.z.| by Th132; :: thesis: verum

end;

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