let z be Complex; :: thesis: ( Arg z in ].PI,((3 / 2) * PI).[ iff ( Re z < 0 & Im z < 0 ) )
thus ( Arg z in ].PI,((3 / 2) * PI).[ implies ( Re z < 0 & Im z < 0 ) ) :: thesis: ( Re z < 0 & Im z < 0 implies Arg z in ].PI,((3 / 2) * PI).[ )

proof

assume A1: Arg z in ].PI,((3 / 2) * PI).[ ; :: thesis: ( Re z < 0 & Im z < 0 )
then PI < Arg z by XXREAL_1:4;
then A2: PI / 2 < Arg z by Lm2, XXREAL_0:2;
A3: Arg z > PI by A1, XXREAL_1:4;
then z <> 0 by Def1;
then A4: ( z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>) & |.z.| > 0 ) by Def1, COMPLEX1:47;
Arg z < (3 / 2) * PI by A1, XXREAL_1:4;
then Arg z in ].(PI / 2),((3 / 2) * PI).[ by A2, XXREAL_1:4;
then cos . (Arg z) < 0 by Th13;
then cos (Arg z) < 0 by SIN_COS:def 19;
hence Re z < 0 by A4, COMPLEX1:12; :: thesis: Im z < 0
Arg z < (3 / 2) * PI by A1, XXREAL_1:4;
then Arg z < 2 * PI by Lm6, XXREAL_0:2;
then Arg z in ].PI,(2 * PI).[ by A3, XXREAL_1:4;
then sin . (Arg z) < 0 by Th9;
then sin (Arg z) < 0 by SIN_COS:def 17;
hence Im z < 0 by A4, COMPLEX1:12; :: thesis: verum

end;

assume that
A5: Re z < 0 and
A6: Im z < 0 ; :: thesis: Arg z in ].PI,((3 / 2) * PI).[
z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
then z <> 0 + (0 * <i>) by A5, COMPLEX1:77;
then A7: ( |.z.| > 0 & z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>) ) by Def1, COMPLEX1:47;
then cos (Arg z) < 0 by A5, COMPLEX1:12;
then cos . (Arg z) < 0 by SIN_COS:def 19;
then A8: not Arg z in [.((3 / 2) * PI),(2 * PI).] by Th16;
sin (Arg z) < 0 by A6, A7, COMPLEX1:12;
then sin . (Arg z) < 0 by SIN_COS:def 17;
then A9: not Arg z in [.0,PI.] by Th8;
Arg z < 2 * PI by Th34;
then A10: Arg z < (3 / 2) * PI by A8, XXREAL_1:1;
0 <= Arg z by Th34;
then Arg z > PI by A9, XXREAL_1:1;
hence Arg z in ].PI,((3 / 2) * PI).[ by A10, XXREAL_1:4; :: thesis: verum