let a be complex number ; :: thesis: for r being Real st r < 0 holds
Arg (a * r) = Arg (- a)
let r be Real; :: thesis: ( r < 0 implies Arg (a * r) = Arg (- a) )
assume A1: r < 0 ; :: thesis: Arg (a * r) = Arg (- a)

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: Arg (a * r) = Arg (- a)

hence Arg (a * r) = Arg (- a) ; :: thesis: verum

end;

suppose A2: a <> 0 ; :: thesis: Arg (a * r) = Arg (- a)

then A3: cos (Arg a) = (Re a) / |.a.| by Th39;
A4: ( 0 <= Arg (- a) & Arg (- a) < 2 * PI ) by COMPTRIG:52;
A5: sin (Arg a) = (Im a) / |.a.| by A2, Th39;
set b = a * r;
A6: a in COMPLEX by XCMPLX_0:def 2;
A7: ( 0 <= Arg (a * r) & Arg (a * r) < 2 * PI ) by COMPTRIG:52;
A8: |.(a * r).| = |.a.| * (abs r) by COMPLEX1:151
.= |.a.| * (- r) by A1, ABSVALUE:def 1 ;
r = r + (0 * <i> ) ;
then A9: ( Re r = r & Im r = 0 ) by COMPLEX1:28;
then Im (a * r) = ((Re a) * 0 ) + (r * (Im a)) by COMPLEX1:24
.= r * (Im a) ;
then A10: sin (Arg (a * r)) = (r * (Im a)) / (- (|.a.| * r)) by A1, A2, A8, Th39
.= - ((r * (Im a)) / (|.a.| * r)) by XCMPLX_1:189
.= - (sin (Arg a)) by A1, A5, XCMPLX_1:92
.= sin (Arg (- a)) by A2, A6, Th38 ;
Re (a * r) = ((Re a) * r) - (0 * (Im a)) by A9, COMPLEX1:24
.= r * (Re a) ;
then cos (Arg (a * r)) = (r * (Re a)) / (- (|.a.| * r)) by A1, A2, A8, Th39
.= - ((r * (Re a)) / (|.a.| * r)) by XCMPLX_1:189
.= - (cos (Arg a)) by A1, A3, XCMPLX_1:92
.= cos (Arg (- a)) by A2, A6, Th38 ;
hence Arg (a * r) = Arg (- a) by A10, A7, A4, Th12; :: thesis: verum

end;

end;