theorem Th20: :: TAYLOR_2:20

for n being Nat
for r, x being Real st r > 0 holds
( (Maclaurin (sin,].(- r),r.[,x)) . (2 * n) = 0 & (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) = (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !) & (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) = (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !) & (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) = 0 )