let z be complex number ; :: thesis: ( Re z < 0 implies cos (Arg z) < 0 )
assume A1: Re z < 0 ; :: thesis: cos (Arg z) < 0
( Im z < 0 or Im z = 0 or Im z > 0 ) ;
then ( Im z < 0 or Im z > 0 or z = (Re z) + (0 * <i> ) ) by COMPLEX1:29;
then ( Arg z in ].(PI / 2),PI .[ or Arg z in ].PI ,((3 / 2) * PI ).[ or Arg z = PI ) by A1, Th54, Th60, Th61;
then ( ( PI / 2 < Arg z & Arg z < PI ) or ( PI < Arg z & Arg z < (3 / 2) * PI ) or Arg z = PI ) by XXREAL_1:4;
then ( PI / 2 < Arg z & Arg z < (3 / 2) * PI ) by Lx2, Lm6, XXREAL_0:2;
then Arg z in ].(PI / 2),((3 / 2) * PI ).[ by XXREAL_1:4;
then cos . (Arg z) < 0 by Th29;
hence cos (Arg z) < 0 by SIN_COS:def 23; :: thesis: verum