let z be complex number ; :: thesis: ( Im z < 0 implies sin (Arg z) < 0 )
( Re z < 0 or Re z = 0 or Re z > 0 ) ;
then A1: ( Re z < 0 or Re z > 0 or z = 0 + ((Im z) * <i> ) ) by COMPLEX1:29;
assume Im z < 0 ; :: thesis: sin (Arg z) < 0
then ( Arg z in ].PI ,((3 / 2) * PI ).[ or Arg z in ].((3 / 2) * PI ),(2 * PI ).[ or Arg z = (3 / 2) * PI ) by A1, Th56, Th61, Th62;
then ( ( PI < Arg z & Arg z < (3 / 2) * PI ) or ( (3 / 2) * PI < Arg z & Arg z < 2 * PI ) or Arg z = (3 / 2) * PI ) by XXREAL_1:4;
then ( PI < Arg z & Arg z < 2 * PI ) by Lm5, Lm6, XXREAL_0:2;
then Arg z in ].PI ,(2 * PI ).[ by XXREAL_1:4;
then sin . (Arg z) < 0 by Th25;
hence sin (Arg z) < 0 by SIN_COS:def 21; :: thesis: verum