let r be Real; for a, b being Complex st Arg a = Arg b & a <> 0 & b <> 0 holds
Arg (Rotate (a,r)) = Arg (Rotate (b,r))
let a, b be Complex; ( Arg a = Arg b & a <> 0 & b <> 0 implies Arg (Rotate (a,r)) = Arg (Rotate (b,r)) )
assume that
A1:
Arg a = Arg b
and
A2:
a <> 0
and
A3:
b <> 0
; Arg (Rotate (a,r)) = Arg (Rotate (b,r))
consider i being Integer such that
A4:
Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))
by A2, Th52;
consider j being Integer such that
A5:
Arg (Rotate (b,r)) = ((2 * PI) * j) + (r + (Arg b))
by A3, Th52;
A6:
( 0 <= Arg (Rotate (a,r)) & 0 <= Arg (Rotate (b,r)) )
by COMPTRIG:34;
A7:
( Arg (Rotate (a,r)) < 2 * PI & Arg (Rotate (b,r)) < 2 * PI )
by COMPTRIG:34;
Arg (Rotate (b,r)) = ((2 * PI) * (j - i)) + (Arg (Rotate (a,r)))
by A1, A4, A5;
hence
Arg (Rotate (a,r)) = Arg (Rotate (b,r))
by A6, A7, Th2; verum