let z be Complex; :: 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 :: thesis: ( ( Arg z in ].0,(PI / 2).[ & Im z > 0 ) or ( Arg z = PI / 2 & Im z > 0 ) or ( Arg z in ].(PI / 2),PI.[ & Im z > 0 ) )

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:41; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

hence Im z > 0 ; :: thesis: verum

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: verum

proof

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

now :: thesis: ( ( Re z > 0 & Arg z in ].0,PI.[ ) or ( Re z = 0 & Arg z in ].0,PI.[ ) or ( Re z < 0 & Arg z in ].0,PI.[ ) )

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:41;
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:13;
then Arg z = PI / 2 by A5, COMPTRIG:37;
hence Arg z in ].0,PI.[ by COMPTRIG:5, 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:42;
hence Arg z in ].0,PI.[ by A3; :: thesis: verum

end;

end;

end;

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

end;