let z be Complex; :: 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 COMPTRIG:62;
hence z = |.z.| by SIN_COS:31; :: thesis: verum

end;

assume z = |.z.| ; :: thesis: Arg z = 0
hence Arg z = 0 by COMPTRIG:35, COMPLEX1:46; :: thesis: verum