let r be Real; :: thesis: for a being Complex holds |.(Rotate (a,r)).| = |.a.|
let a be Complex; :: 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:12;
hence |.(Rotate (a,r)).| = sqrt (((|.a.| * (cos (r + (Arg a)))) ^2) + ((|.a.| * (sin (r + (Arg a)))) ^2)) by COMPLEX1:def 12
.= sqrt ((|.a.| ^2) * (((cos (r + (Arg a))) ^2) + ((sin (r + (Arg a))) ^2)))
.= sqrt ((|.a.| ^2) * 1) by SIN_COS:29
.= |.a.| by COMPLEX1:46, SQUARE_1:22 ;
:: thesis: verum