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)) )
assume a <> 0 ; :: thesis: ex i being Integer st Arg (Rotate a,r) = ((2 * PI ) * i) + (r + (Arg a))
then A1: Rotate a,r <> 0c by Th66;
A2: |.a.| = |.(Rotate a,r).| by Th67;
consider AR being real number such that
A3: AR = ((2 * PI ) * (- [\((r + (Arg a)) / (2 * PI ))/])) + (r + (Arg a)) and
A4: 0 <= AR and
A5: AR < 2 * PI by Th2, COMPTRIG:21;
reconsider ar = AR as Real by XREAL_0:def 1;
A6: cos (r + (Arg a)) = cos ar by A3, Th10;
A7: sin (r + (Arg a)) = sin ar by A3, Th9;
take i = - [\((r + (Arg a)) / (2 * PI ))/]; :: thesis: Arg (Rotate a,r) = ((2 * PI ) * i) + (r + (Arg a))
thus Arg (Rotate a,r) = ((2 * PI ) * i) + (r + (Arg a)) by A1, A2, A3, A4, A5, A6, A7, COMPTRIG:def 1; :: thesis: verum