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 A2: z <> 0 ; :: thesis: ( Re z < 0 & Im z = 0 )

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

end;

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

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

end;

end;

end;

assume A4: ( Re z < 0 & Im z = 0 ) ; :: thesis: Arg z = PI
then z = (Re z) + (0 * <i> ) by COMPLEX1:29;
hence Arg z = PI by A4, COMPTRIG:54; :: thesis: verum