let a be Complex; :: 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 Th24;
A4: ( 0 <= Arg (- a) & Arg (- a) < 2 * PI ) by COMPTRIG:34;
A5: sin (Arg a) = (Im a) / |.a.| by A2, Th24;
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:34;
A8: |.(a * r).| = |.a.| * |.r.| by COMPLEX1:65
.= |.a.| * (- r) by A1, ABSVALUE:def 1 ;
r = r + (0 * <i>) ;
then A9: ( Re r = r & Im r = 0 ) by COMPLEX1:12;
then Im (a * r) = ((Re a) * 0) + (r * (Im a)) by COMPLEX1:9
.= r * (Im a) ;
then A10: sin (Arg (a * r)) = (r * (Im a)) / (- (|.a.| * r)) by A1, A2, A8, Th24
.= - ((r * (Im a)) / (|.a.| * r)) by XCMPLX_1:188
.= - (sin (Arg a)) by A1, A5, XCMPLX_1:91
.= sin (Arg (- a)) by A2, A6, Th23 ;
Re (a * r) = ((Re a) * r) - (0 * (Im a)) by A9, COMPLEX1:9
.= r * (Re a) ;
then cos (Arg (a * r)) = (r * (Re a)) / (- (|.a.| * r)) by A1, A2, A8, Th24
.= - ((r * (Re a)) / (|.a.| * r)) by XCMPLX_1:188
.= - (cos (Arg a)) by A1, A3, XCMPLX_1:91
.= cos (Arg (- a)) by A2, A6, Th23 ;
hence Arg (a * r) = Arg (- a) by A10, A7, A4, Th11; :: thesis: verum
end;
end;