let r, x be Real; for m being Nat st 0 < r holds
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m
let m be Nat; ( 0 < r implies (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m )
assume A1:
r > 0
; (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m
defpred S1[ Nat] means (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * $1) = (Partial_Sums (x P_cos)) . $1;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
S1[k + 1]
thus (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * (k + 1)) =
((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 1)) + ((Maclaurin (cos,].(- r),r.[,x)) . (((2 * k) + 1) + 1))
by SERIES_1:def 1
.=
((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * k) + 1)) + ((((- 1) |^ (k + 1)) * (x |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))
by A1, Th20
.=
((Partial_Sums (x P_cos)) . k) + ((((- 1) |^ (k + 1)) * (x |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))
by A1, Th25
.=
((Partial_Sums (x P_cos)) . k) + ((x P_cos) . (k + 1))
by SIN_COS:def 21
.=
(Partial_Sums (x P_cos)) . (k + 1)
by SERIES_1:def 1
;
verum
end;
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * 0) =
(Maclaurin (cos,].(- r),r.[,x)) . (2 * 0)
by SERIES_1:def 1
.=
(((- 1) |^ 0) * (x |^ (2 * 0))) / ((2 * 0) !)
by A1, Th20
.=
(x P_cos) . 0
by SIN_COS:def 21
.=
(Partial_Sums (x P_cos)) . 0
by SERIES_1:def 1
;
then A3:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A3, A2);
hence
(Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m
; verum