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 i = - [\((r + (Arg a)) / (2 * PI ))/]; :: thesis: Arg (Rotate a,r) = ((2 * PI ) * i) + (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:21;
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 ) * i) + (r + (Arg a)) by A2, A1, A3, A4, COMPTRIG:def 1; :: thesis: verum