let z be Complex; ( 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 ) )
( 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).[
;
( 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:47;
cos . (Arg z) > 0
by A1, Th15;
then
cos (Arg z) > 0
by SIN_COS:def 19;
hence
Re z > 0
by A4, COMPLEX1:12;
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 Th9;
then
sin (Arg z) < 0
by SIN_COS:def 17;
hence
Im z < 0
by A4, COMPLEX1:12;
verum
end;
assume that
A5:
Re z > 0
and
A6:
Im z < 0
; Arg z in ].((3 / 2) * PI),(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
sin (Arg z) < 0
by A6, COMPLEX1:12;
then
sin . (Arg z) < 0
by SIN_COS:def 17;
then A8:
not Arg z in [.0,PI.]
by Th8;
cos (Arg z) > 0
by A5, A7, COMPLEX1:12;
then
cos . (Arg z) > 0
by SIN_COS:def 19;
then
not Arg z in [.(PI / 2),((3 / 2) * PI).]
by Th14;
then A9:
( Arg z < PI / 2 or Arg z > (3 / 2) * PI )
by XXREAL_1:1;
0 <= Arg z
by Th34;
then A10:
Arg z > PI
by A8, XXREAL_1:1;
Arg z < 2 * PI
by Th34;
hence
Arg z in ].((3 / 2) * PI),(2 * PI).[
by A10, A9, Lm2, XXREAL_0:2, XXREAL_1:4; verum