let z be Complex; :: thesis:
A1: Arg z >= 0 by COMPTRIG:34;
assume A2: Arg z <> 0 ; :: thesis:

hereby :: thesis:

assume Arg z < PI ; :: thesis:
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:

end;

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

proof

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

now :: thesis:

per cases ;

suppose Re z > 0 ; :: thesis:

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

end;

suppose Re z = 0 ; :: thesis:

then z = 0 + ((Im z) * <i>) by COMPLEX1:13;
hence Arg z < PI by A4, COMPTRIG:5, COMPTRIG:37, COMPTRIG:48; :: thesis:

end;

suppose Re z < 0 ; :: thesis:

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

end;

end;

end;

hence Arg z < PI ; :: thesis:

end;