let n be Element of NAT ; :: thesis: 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; :: thesis: ( 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 A1: r > 0 ; :: thesis: ( (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 )
abs (0 - 0 ) = 0 by ABSVALUE:7;
then A2: 0 in ].(0 - r),(0 + r).[ by A1, RCOMP_1:8;
A3: dom (((- 1) |^ n) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A4: 0 in dom (sin | ].(- r),r.[) by A2, Th17;
A5: dom (((- 1) |^ n) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A6: 0 in dom (cos | ].(- r),r.[) by A2, Th17;
A7: dom (((- 1) |^ (n + 1)) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A8: (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, A3, VALUED_1:def 5
.= ((((- 1) |^ n) * (sin . 0 )) * (x |^ (2 * n))) / ((2 * n) ! ) by A4, FUNCT_1:70
.= 0 by SIN_COS:33 ;
A9: (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, A5, VALUED_1:def 5
.= ((((- 1) |^ n) * (cos . 0 )) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) ! ) by A6, FUNCT_1:70
.= (((- 1) |^ n) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) ! ) by SIN_COS:33 ;
A10: (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, A5, VALUED_1:def 5
.= ((((- 1) |^ n) * (cos . 0 )) * (x |^ (2 * n))) / ((2 * n) ! ) by A6, FUNCT_1:70
.= (((- 1) |^ n) * (x |^ (2 * n))) / ((2 * n) ! ) by SIN_COS:33 ;
(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, A7, VALUED_1:def 5
.= ((((- 1) |^ (n + 1)) * (sin . 0 )) * (x |^ ((2 * n) + 1))) / (((2 * n) + 1) ! ) by A4, FUNCT_1:70
.= 0 by SIN_COS:33 ;
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 A8, A9, A10; :: thesis: verum