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