let z be Complex; :: thesis: ( Arg z = 0 iff ( Re z >= 0 & Im z = 0 ) )
A1: |.z.| = |.z.| + (0 * <i>) ;

hereby :: thesis: ( Re z >= 0 & Im z = 0 implies Arg z = 0 )

assume Arg z = 0 ; :: thesis: ( Re z >= 0 & Im z = 0 )
then A2: z = |.z.| by Th13;
then Re z = |.z.| by A1, COMPLEX1:12;
hence ( Re z >= 0 & Im z = 0 ) by A1, A2, COMPLEX1:12, COMPLEX1:46; :: thesis: verum

end;

assume that
A3: Re z >= 0 and
A4: Im z = 0 ; :: thesis: Arg z = 0
z = (Re z) + (0 * <i>) by A4, COMPLEX1:13;
hence Arg z = 0 by A3, COMPTRIG:35; :: thesis: verum