A1:
|.(0 - 0).| = 0
by ABSVALUE:2;
let n be 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 )
let r, x be Real; ( r > 0 implies ( (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 ) )
assume
r > 0
; ( (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 )
then A2:
0 in ].(0 - r),(0 + r).[
by A1, RCOMP_1:1;
then A3:
0 in dom (cos | ].(- r),r.[)
by Th17;
A4: dom (((- 1) |^ n) (#) (cos | ].(- r),r.[)) =
dom (cos | ].(- r),r.[)
by VALUED_1:def 5
.=
].(- r),r.[
by Th17
;
A5: (Maclaurin (sin,].(- r),r.[,x)) . ((2 * n) + 1) =
((((diff (sin,].(- r),r.[)) . ((2 * n) + 1)) . 0) * ((x - 0) |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by TAYLOR_1:def 7
.=
(((((- 1) |^ n) (#) (cos | ].(- r),r.[)) . 0) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by Th19
.=
((((- 1) |^ n) * ((cos | ].(- r),r.[) . 0)) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by A2, A4, VALUED_1:def 5
.=
((((- 1) |^ n) * (cos . 0)) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by A3, FUNCT_1:47
.=
(((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by SIN_COS:30
;
A6: dom (((- 1) |^ n) (#) (sin | ].(- r),r.[)) =
dom (sin | ].(- r),r.[)
by VALUED_1:def 5
.=
].(- r),r.[
by Th17
;
A7:
0 in dom (sin | ].(- r),r.[)
by A2, Th17;
A8: (Maclaurin (cos,].(- r),r.[,x)) . (2 * n) =
((((diff (cos,].(- r),r.[)) . (2 * n)) . 0) * ((x - 0) |^ (2 * n))) / ((2 * n) !)
by TAYLOR_1:def 7
.=
(((((- 1) |^ n) (#) (cos | ].(- r),r.[)) . 0) * (x |^ (2 * n))) / ((2 * n) !)
by Th19
.=
((((- 1) |^ n) * ((cos | ].(- r),r.[) . 0)) * (x |^ (2 * n))) / ((2 * n) !)
by A2, A4, VALUED_1:def 5
.=
((((- 1) |^ n) * (cos . 0)) * (x |^ (2 * n))) / ((2 * n) !)
by A3, FUNCT_1:47
.=
(((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) !)
by SIN_COS:30
;
A9: dom (((- 1) |^ (n + 1)) (#) (sin | ].(- r),r.[)) =
dom (sin | ].(- r),r.[)
by VALUED_1:def 5
.=
].(- r),r.[
by Th17
;
A10: (Maclaurin (cos,].(- r),r.[,x)) . ((2 * n) + 1) =
((((diff (cos,].(- r),r.[)) . ((2 * n) + 1)) . 0) * ((x - 0) |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by TAYLOR_1:def 7
.=
(((((- 1) |^ (n + 1)) (#) (sin | ].(- r),r.[)) . 0) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by Th19
.=
((((- 1) |^ (n + 1)) * ((sin | ].(- r),r.[) . 0)) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by A2, A9, VALUED_1:def 5
.=
((((- 1) |^ (n + 1)) * (sin . 0)) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
by A7, FUNCT_1:47
.=
0
by SIN_COS:30
;
(Maclaurin (sin,].(- r),r.[,x)) . (2 * n) =
((((diff (sin,].(- r),r.[)) . (2 * n)) . 0) * ((x - 0) |^ (2 * n))) / ((2 * n) !)
by TAYLOR_1:def 7
.=
(((((- 1) |^ n) (#) (sin | ].(- r),r.[)) . 0) * (x |^ (2 * n))) / ((2 * n) !)
by Th19
.=
((((- 1) |^ n) * ((sin | ].(- r),r.[) . 0)) * (x |^ (2 * n))) / ((2 * n) !)
by A2, A6, VALUED_1:def 5
.=
((((- 1) |^ n) * (sin . 0)) * (x |^ (2 * n))) / ((2 * n) !)
by A7, FUNCT_1:47
.=
0
by SIN_COS:30
;
hence
( (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 )
by A5, A8, A10; verum