let z be complex number ; :: 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 A2: ( Arg z > PI & Arg z < (3 / 2) * PI ) by XXREAL_1:4;
then A3: z <> 0 by Def1;
then B4: z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i> ) by Def1;
A5: |.z.| > 0 by A3, COMPLEX1:133;
( PI < Arg z & Arg z < (3 / 2) * PI ) by A1, XXREAL_1:4;
then ( PI / 2 < Arg z & Arg z < (3 / 2) * PI ) by Lx2, XXREAL_0:2;
then Arg z in ].(PI / 2),((3 / 2) * PI ).[ by XXREAL_1:4;
then cos . (Arg z) < 0 by Th29;
then cos (Arg z) < 0 by SIN_COS:def 23;
hence Re z < 0 by B4, A5, COMPLEX1:28; :: thesis: Im z < 0
Arg z < 2 * PI by A2, Lm7, XXREAL_0:2;
then Arg z in ].PI ,(2 * PI ).[ by A2, XXREAL_1:4;
then sin . (Arg z) < 0 by Th25;
then sin (Arg z) < 0 by SIN_COS:def 21;
hence Im z < 0 by B4, A5, COMPLEX1:28; :: thesis: verum

end;

assume that
A6: Re z < 0 and
A7: Im z < 0 ; :: thesis: Arg z in ].PI ,((3 / 2) * PI ).[
z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
then A8: z <> 0 + (0 * <i> ) by A6, COMPLEX1:163;
then A9: |.z.| > 0 by COMPLEX1:133;
A10: ( 0 <= Arg z & Arg z < 2 * PI ) by Th52;
z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i> ) by A8, Def1;
then ( cos (Arg z) < 0 & sin (Arg z) < 0 ) by A9, A6, A7, COMPLEX1:28;
then ( cos . (Arg z) < 0 & sin . (Arg z) < 0 ) by SIN_COS:def 21, SIN_COS:def 23;
then ( not Arg z in [.0 ,PI .] & not Arg z in [.(- (PI / 2)),(PI / 2).] & not Arg z in [.((3 / 2) * PI ),(2 * PI ).] ) by Th24, Th28, Th32;
then ( Arg z > PI & ( Arg z < - (PI / 2) or Arg z > PI / 2 ) & Arg z < (3 / 2) * PI ) by A10, XXREAL_1:1;
hence Arg z in ].PI ,((3 / 2) * PI ).[ by XXREAL_1:4; :: thesis: verum