let a, b be Element of COMPLEX ; :: thesis: for r being Real holds Rotate (a + b),r = (Rotate a,r) + (Rotate b,r)
let r be Real; :: thesis: Rotate (a + b),r = (Rotate a,r) + (Rotate b,r)
set ab = a + b;
set rab = Rotate (a + b),r;
set ra = Rotate a,r;
set rb = Rotate b,r;
A1: ( Re (Rotate (a + b),r) = ((Re (a + b)) * (cos r)) - ((Im (a + b)) * (sin r)) & Im (Rotate (a + b),r) = ((Re (a + b)) * (sin r)) + ((Im (a + b)) * (cos r)) ) by Th70;
A2: ( Re (Rotate a,r) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Im (Rotate a,r) = ((Re a) * (sin r)) + ((Im a) * (cos r)) ) by Th70;
A3: ( Re (Rotate b,r) = ((Re b) * (cos r)) - ((Im b) * (sin r)) & Im (Rotate b,r) = ((Re b) * (sin r)) + ((Im b) * (cos r)) ) by Th70;
A4: ( Re (a + b) = (Re a) + (Re b) & Im (a + b) = (Im a) + (Im b) ) by COMPLEX1:19;
A5: Re ((Rotate a,r) + (Rotate b,r)) = (((Re a) * (cos r)) - ((Im a) * (sin r))) + (((Re b) * (cos r)) - ((Im b) * (sin r))) by A2, A3, COMPLEX1:19
.= Re (Rotate (a + b),r) by A1, A4 ;
Im ((Rotate a,r) + (Rotate b,r)) = (((Re a) * (sin r)) + ((Im a) * (cos r))) + (((Re b) * (sin r)) + ((Im b) * (cos r))) by A2, A3, COMPLEX1:19
.= Im (Rotate (a + b),r) by A1, A4 ;
hence Rotate (a + b),r = (Rotate a,r) + (Rotate b,r) by A5, COMPLEX1:9; :: thesis: verum