let z be Complex; :: thesis: ( Arg z <> 0 implies ( Arg z < PI iff sin (Arg z) > 0 ) )
A1: Arg z >= 0 by COMPTRIG:34;
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 Th16;
hence sin (Arg z) > 0 by COMPTRIG:45; :: thesis: verum

end;

A3: ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, 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:48;

now :: thesis: Arg z < PI

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:41;
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:13;
hence Arg z < PI by A4, COMPTRIG:5, COMPTRIG:37, COMPTRIG:48; :: thesis: verum

end;

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

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

end;

end;

end;

hence Arg z < PI ; :: thesis: verum

end;