let a be Complex; :: thesis: for r being Real holds
( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) )
let r be Real; :: thesis: ( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) )
a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) by COMPTRIG:62;
then A1: ( Re a = |.a.| * (cos (Arg a)) & Im a = |.a.| * (sin (Arg a)) ) by COMPLEX1:12;
thus Re (Rotate (a,r)) = |.a.| * (cos (r + (Arg a))) by COMPLEX1:12
.= |.a.| * (((cos r) * (cos (Arg a))) - ((sin r) * (sin (Arg a)))) by SIN_COS:75
.= ((Re a) * (cos r)) - ((Im a) * (sin r)) by A1 ; :: thesis: Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r))
thus Im (Rotate (a,r)) = |.a.| * (sin (r + (Arg a))) by COMPLEX1:12
.= |.a.| * (((sin r) * (cos (Arg a))) + ((cos r) * (sin (Arg a)))) by SIN_COS:75
.= ((Re a) * (sin r)) + ((Im a) * (cos r)) by A1 ; :: thesis: verum