let z be complex number ; :: 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 Th24;
then Re z = |.z.| by A1, COMPLEX1:28;
hence ( Re z >= 0 & Im z = 0 ) by A1, A2, COMPLEX1:28, COMPLEX1:132; :: 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:29;
hence Arg z = 0 by A3, COMPTRIG:53; :: thesis: verum