let x, r be Real; for n being Element of NAT st r > 0 holds
( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )
let n be Element of NAT ; ( r > 0 implies ( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) ) )
A1:
|.(0 - 0).| = 0
by ABSVALUE:2;
assume
r > 0
; ( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )
then A2:
0 in ].(0 - r),(0 + r).[
by A1, RCOMP_1:1;
A3: (Maclaurin (cos,].(- r),r.[,x)) . n =
(Taylor (cos,].(- r),r.[,0,x)) . n
by TAYLOR_2:def 1
.=
((((diff (cos,].(- r),r.[)) . n) . 0) * ((x - 0) |^ n)) / (n !)
by TAYLOR_1:def 7
.=
((cos . (0 + ((n * PI) / 2))) * (x |^ n)) / (n !)
by A2, Th14
;
(Maclaurin (sin,].(- r),r.[,x)) . n =
(Taylor (sin,].(- r),r.[,0,x)) . n
by TAYLOR_2:def 1
.=
((((diff (sin,].(- r),r.[)) . n) . 0) * ((x - 0) |^ n)) / (n !)
by TAYLOR_1:def 7
.=
((sin . (0 + ((n * PI) / 2))) * (x |^ n)) / (n !)
by A2, Th11
;
hence
( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )
by A3; verum