let x be Real; :: thesis: ( x < 0 implies Arg (x * <i> ) = (3 / 2) * PI )
A1: ( 0 <= Arg (0 + (x * <i> )) & Arg (0 + (x * <i> )) < 2 * PI ) by Th52;
assume A2: x < 0 ; :: thesis: Arg (x * <i> ) = (3 / 2) * PI
then A3: 0 + (x * <i> ) <> 0 ;
then A4: 0 + (x * <i> ) = (|.(0 + (x * <i> )).| * (cos (Arg (0 + (x * <i> ))))) + ((|.(0 + (x * <i> )).| * (sin (Arg (0 + (x * <i> ))))) * <i> ) by Def1;
|.(0 + (x * <i> )).| <> 0 by A3, COMPLEX1:131;
then cos (Arg (0 + (x * <i> ))) = 0 by A4, COMPLEX1:163;
then ( Arg (0 + (x * <i> )) = (3 / 2) * PI or |.(0 + (x * <i> )).| * 1 = x ) by A1, A4, Th34, SIN_COS:82;
hence Arg (x * <i> ) = (3 / 2) * PI by A2, COMPLEX1:132; :: thesis: verum