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

proof

assume Arg z in ].0,PI.[ ; :: thesis:
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 :: thesis:

per cases by A1, A2, XXREAL_1:4;

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

hence Im z > 0 by COMPTRIG:41; :: thesis:

end;

case Arg z = PI / 2 ; :: thesis:

hence Im z > 0 by COMPTRIG:48, SIN_COS:77; :: thesis:

end;

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

hence Im z > 0 by COMPTRIG:42; :: thesis:

end;

end;

end;

hence Im z > 0 ; :: thesis:

end;

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

proof

assume A5: Im z > 0 ; :: thesis:

now :: thesis:

per cases ;

case Re z > 0 ; :: thesis:

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

end;

case Re z = 0 ; :: thesis:

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

end;

case Re z < 0 ; :: thesis:

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

end;

end;

end;

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

end;