let z be complex number ; :: thesis: ( Arg z = PI iff ( Re z < 0 & Im z = 0 ) )

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

assume A1: Arg z = PI ; :: thesis: ( Re z < 0 & Im z = 0 )

per cases ( z <> 0 or z = 0 ) ;

suppose z <> 0 ; :: thesis: ( Re z < 0 & Im z = 0 )

then ( z = (|.z.| * (cos PI)) + ((|.z.| * (sin PI)) * <i>) & - (- |.z.|) > 0 ) by A1, COMPLEX1:47, COMPTRIG:def 1;
hence ( Re z < 0 & Im z = 0 ) by COMPLEX1:def 1, COMPLEX1:def 2, SIN_COS:77; :: thesis: verum

end;

suppose z = 0 ; :: thesis: ( Re z < 0 & Im z = 0 )

hence ( Re z < 0 & Im z = 0 ) by A1, COMPTRIG:5, COMPTRIG:35; :: thesis: verum

end;

end;

end;

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