let z be complex number ; :: thesis: ( Arg z <> 0 implies ( Arg z < PI iff sin (Arg z) > 0 ) )
A1: Arg z >= 0 by COMPTRIG:52;
assume A2: Arg z <> 0 ; :: thesis: ( Arg z < PI iff sin (Arg z) > 0 )

hereby :: thesis: ( sin (Arg z) > 0 implies Arg z < PI )

assume Arg z < PI ; :: thesis: sin (Arg z) > 0
then Arg z in ].0 ,PI .[ by A2, A1, XXREAL_1:4;
then Im z > 0 by Th27;
hence sin (Arg z) > 0 by COMPTRIG:63; :: thesis: verum

end;

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

proof

assume A4: sin (Arg z) > 0 ; :: thesis: Arg z < PI
then A5: Im z > 0 by COMPTRIG:66;

now

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

suppose Re z > 0 ; :: thesis: Arg z < PI

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

end;

suppose Re z = 0 ; :: thesis: Arg z < PI

then z = 0 + ((Im z) * <i> ) by COMPLEX1:29;
hence Arg z < PI by A4, COMPTRIG:21, COMPTRIG:55, COMPTRIG:66; :: thesis: verum

end;

suppose Re z < 0 ; :: thesis: Arg z < PI

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

end;

end;

end;

hence Arg z < PI ; :: thesis: verum

end;