let r, x be Real; for m being Nat st 0 < r & m > 0 holds
( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_sin)) . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m )
let m be Nat; ( 0 < r & m > 0 implies ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_sin)) . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m ) )
assume that
A1:
r > 0
and
A2:
m > 0
; ( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_sin)) . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m )
A3:
m - 1 is Element of NAT
by A2, NAT_1:20;
2 * m > 2 * 0
by A2, XREAL_1:68;
then A4:
(2 * m) - 1 is Element of NAT
by NAT_1:20;
then A5: (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) =
((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) - 1)) + ((Maclaurin (sin,].(- r),r.[,x)) . (((2 * m) - 1) + 1))
by SERIES_1:def 1
.=
((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) - 1)) + 0
by A1, Th20
.=
(Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * (m - 1)) + 1)
.=
(Partial_Sums (x P_sin)) . (m - 1)
by A1, A3, Th25
;
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) =
((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) - 1)) + ((Maclaurin (cos,].(- r),r.[,x)) . (((2 * m) - 1) + 1))
by A4, SERIES_1:def 1
.=
((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) - 1)) + ((((- 1) |^ m) * (x |^ (2 * m))) / ((2 * m) !))
by A1, Th20
.=
((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * (m - 1)) + 1)) + ((x P_cos) . m)
by SIN_COS:def 21
.=
((Partial_Sums (x P_cos)) . (m - 1)) + ((x P_cos) . ((m - 1) + 1))
by A1, A3, Th25
.=
(Partial_Sums (x P_cos)) . m
by A3, SERIES_1:def 1
;
hence
( (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_sin)) . (m - 1) & (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m )
by A5; verum