let z be complex number ; :: thesis: ( Arg z in ].0 ,PI .[ iff Im z > 0 )
thus ( Arg z in ].0 ,PI .[ implies Im z > 0 ) :: thesis: ( Im z > 0 implies Arg z in ].0 ,PI .[ )

proof

assume Arg z in ].0 ,PI .[ ; :: thesis: Im z > 0
then A1: ( 0 < Arg z & Arg z < PI ) by XXREAL_1:4;
A2: ( Arg z < PI / 2 or Arg z = PI / 2 or Arg z > PI / 2 ) by XXREAL_0:1;

now

per cases ( Arg z in ].0 ,(PI / 2).[ or Arg z = PI / 2 or Arg z in ].(PI / 2),PI .[ ) by A1, A2, XXREAL_1:4;

case Arg z in ].0 ,(PI / 2).[ ; :: thesis: Im z > 0

hence Im z > 0 by COMPTRIG:59; :: thesis: verum

end;

case Arg z = PI / 2 ; :: thesis: Im z > 0

hence Im z > 0 by COMPTRIG:66, SIN_COS:82; :: thesis: verum

end;

case Arg z in ].(PI / 2),PI .[ ; :: thesis: Im z > 0

hence Im z > 0 by COMPTRIG:60; :: thesis: verum

end;

end;

end;

hence Im z > 0 ; :: thesis: verum

end;

A3: ].(PI / 2),PI .[ c= ].0 ,PI .[ by COMPTRIG:21, XXREAL_1:46;
A4: ].0 ,(PI / 2).[ c= ].0 ,PI .[ by COMPTRIG:21, XXREAL_1:46;
thus ( Im z > 0 implies Arg z in ].0 ,PI .[ ) :: thesis: verum

proof

assume A5: Im z > 0 ; :: thesis: Arg z in ].0 ,PI .[

now

per cases ( Re z > 0 or Re z = 0 or Re z < 0 ) ;

case Re z > 0 ; :: thesis: Arg z in ].0 ,PI .[

then Arg z in ].0 ,(PI / 2).[ by A5, COMPTRIG:59;
hence Arg z in ].0 ,PI .[ by A4; :: thesis: verum

end;

case Re z = 0 ; :: thesis: Arg z in ].0 ,PI .[

then z = 0 + ((Im z) * <i> ) by COMPLEX1:29;
then Arg z = PI / 2 by A5, COMPTRIG:55;
hence Arg z in ].0 ,PI .[ by COMPTRIG:21, XXREAL_1:4; :: thesis: verum

end;

case Re z < 0 ; :: thesis: Arg z in ].0 ,PI .[

then Arg z in ].(PI / 2),PI .[ by A5, COMPTRIG:60;
hence Arg z in ].0 ,PI .[ by A3; :: thesis: verum

end;

end;

end;

hence Arg z in ].0 ,PI .[ ; :: thesis: verum

end;