let r be Real; :: thesis: for a being complex number holds |.(Rotate a,r).| = |.a.|
let a be complex number ; :: thesis: |.(Rotate a,r).| = |.a.|
( Re (Rotate a,r) = |.a.| * (cos (r + (Arg a))) & Im (Rotate a,r) = |.a.| * (sin (r + (Arg a))) ) by COMPLEX1:28;
hence |.(Rotate a,r).| = sqrt (((|.a.| * (cos (r + (Arg a)))) ^2 ) + ((|.a.| * (sin (r + (Arg a)))) ^2 )) by COMPLEX1:def 16
.= sqrt ((|.a.| ^2 ) * (((cos (r + (Arg a))) ^2 ) + ((sin (r + (Arg a))) ^2 )))
.= sqrt ((|.a.| ^2 ) * 1) by SIN_COS:32
.= |.a.| by COMPLEX1:132, SQUARE_1:89 ;
:: thesis: verum