let z be Complex; :: 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 )

reconsider zz = |.z.| as Element of REAL by XREAL_0:def 1;
A3: ( z = (zz * (cos PI)) + ((|.z.| * (sin PI)) * <i>) & - (- |.z.|) > 0 ) by A1, COMPLEX1:47, COMPTRIG:def 1, A2;
( cos PI = - 1 & sin PI = 0 ) by SIN_COS:77;
then A5: z = (zz * (- 1)) + ((zz * 0) * <i>) by A3;
hence Re z < 0 by COMPLEX1:def 1, A3; :: thesis: Im z = 0
thus Im z = 0 by COMPLEX1:def 2, A5; :: 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
A6: Re z < 0 and
A7: Im z = 0 ; :: thesis: Arg z = PI
z = (Re z) + (0 * <i>) by A7, COMPLEX1:13;
hence Arg z = PI by A6, COMPTRIG:36; :: thesis: verum