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

proof

assume A1: Arg z in ].((3 / 2) * PI ),(2 * PI ).[ ; :: thesis: ( Re z > 0 & Im z < 0 )
then A2: Arg z < 2 * PI by XXREAL_1:4;
A3: Arg z > (3 / 2) * 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:133;
cos . (Arg z) > 0 by A1, Th31;
then cos (Arg z) > 0 by SIN_COS:def 23;
hence Re z > 0 by A4, COMPLEX1:28; :: thesis: Im z < 0
Arg z > PI by A3, Lm5, 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 A4, COMPLEX1:28; :: thesis: verum

end;

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