let r be Real; :: thesis: for a being complex number st a <> 0 holds
ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))
let a be complex number ; :: thesis: ( a <> 0 implies ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a)) )
A1: |.a.| = |.(Rotate (a,r)).| by Th67;
assume a <> 0 ; :: thesis: ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))
then A2: Rotate (a,r) <> 0c by Th66;
take - [\((r + (Arg a)) / (2 * PI))/] ; :: thesis: Arg (Rotate (a,r)) = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a))
consider AR being real number such that
A3: AR = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a)) and
A4: ( 0 <= AR & AR < 2 * PI ) by Th2, COMPTRIG:5;
reconsider ar = AR as Real by XREAL_0:def 1;
( cos (r + (Arg a)) = cos ar & sin (r + (Arg a)) = sin ar ) by A3, Th9, Th10;
hence Arg (Rotate (a,r)) = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a)) by A2, A1, A3, A4, COMPTRIG:def 1; :: thesis: verum