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