let r be Real; :: thesis: for a being Complex st a <> 0 holds
ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))
let a be Complex; :: 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 Th51;
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 Th50;
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 such that
A3: AR = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a)) and
A4: ( 0 <= AR & AR < 2 * PI ) by Th1, COMPTRIG:5;
( cos (r + (Arg a)) = cos AR & sin (r + (Arg a)) = sin AR ) by A3, Th8, Th9;
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