let a be Complex; for r being Real st r > 0 holds
Arg (a * r) = Arg a
let r be Real; ( r > 0 implies Arg (a * r) = Arg a )
assume A1:
r > 0
; Arg (a * r) = Arg a
per cases
( a = 0 or a <> 0 )
;
suppose A2:
a <> 0
;
Arg (a * r) = Arg athen A3:
sin (Arg a) = (Im a) / |.a.|
by Th24;
set b =
a * r;
A4:
|.(a * r).| =
|.a.| * |.r.|
by COMPLEX1:65
.=
|.a.| * r
by A1, ABSVALUE:def 1
;
A5:
cos (Arg a) = (Re a) / |.a.|
by A2, Th24;
A6:
(
0 <= Arg a &
Arg a < 2
* PI )
by COMPTRIG:34;
r = r + (0 * <i>)
;
then A7:
(
Re r = r &
Im r = 0 )
by COMPLEX1:12;
then A8:
Im (a * r) =
((Re a) * 0) + (r * (Im a))
by COMPLEX1:9
.=
r * (Im a)
;
A9:
sin (Arg (a * r)) =
(Im (a * r)) / |.(a * r).|
by A1, A2, Th24
.=
sin (Arg a)
by A1, A8, A4, A3, XCMPLX_1:91
;
A10:
(
0 <= Arg (a * r) &
Arg (a * r) < 2
* PI )
by COMPTRIG:34;
A11:
Re (a * r) =
((Re a) * r) - (0 * (Im a))
by A7, COMPLEX1:9
.=
r * (Re a)
;
cos (Arg (a * r)) =
(Re (a * r)) / |.(a * r).|
by A1, A2, Th24
.=
cos (Arg a)
by A1, A11, A4, A5, XCMPLX_1:91
;
hence
Arg (a * r) = Arg a
by A9, A10, A6, Th11;
verum end; end;