let z be complex number ; :: thesis: ( Arg z = 0 iff z = |.z.| )

hereby :: thesis: ( z = |.z.| implies Arg z = 0 )

assume Arg z = 0 ; :: thesis: z = |.z.|
then z = (|.z.| * (cos 0 )) + ((|.z.| * (sin 0 )) * <i> ) by Th19;
hence z = |.z.| by SIN_COS:34; :: thesis: verum

end;

assume z = |.z.| ; :: thesis: Arg z = 0
hence Arg z = 0 by Th23, COMPLEX1:132; :: thesis: verum