let s be Real_Sequence; ( ( for n being Nat holds s . n = (((- 1) |^ n) * (2 |^ (n + 1))) / (((2 |^ (n + 1)) + ((- 1) |^ (n + 1))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) ) implies for n being Nat holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))) )
defpred S1[ Nat] means (Partial_Sums s) . $1 = (1 / 3) + (((- 1) |^ ($1 + 2)) / (3 * ((2 |^ ($1 + 2)) + ((- 1) |^ ($1 + 2)))));
assume A1:
for n being Nat holds s . n = (((- 1) |^ n) * (2 |^ (n + 1))) / (((2 |^ (n + 1)) + ((- 1) |^ (n + 1))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))
; for n being Nat holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))
A2:
for n being Nat st S1[n] holds
S1[n + 1]
(Partial_Sums s) . 0 =
s . 0
by SERIES_1:def 1
.=
(((- 1) |^ 0) * (2 |^ (0 + 1))) / (((2 |^ (0 + 1)) + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2))))
by A1
.=
(1 * (2 |^ (0 + 1))) / (((2 |^ (0 + 1)) + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2))))
by NEWTON:4
.=
(1 * 2) / (((2 |^ (0 + 1)) + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2))))
.=
(1 * 2) / ((2 + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2))))
.=
(1 * 2) / ((2 + (- 1)) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2))))
.=
(1 * 2) / ((2 + (- 1)) * ((2 * 2) + ((- 1) |^ (0 + 2))))
by WSIERP_1:1
.=
(1 * 2) / ((2 + (- 1)) * ((2 * 2) + ((- 1) * (- 1))))
by WSIERP_1:1
.=
(1 / 3) + (((- 1) * (- 1)) / (3 * ((2 * 2) + ((- 1) * (- 1)))))
.=
(1 / 3) + (((- 1) |^ 2) / (3 * ((2 * 2) + ((- 1) * (- 1)))))
by WSIERP_1:1
.=
(1 / 3) + (((- 1) |^ 2) / (3 * ((2 * 2) + ((- 1) |^ 2))))
by WSIERP_1:1
.=
(1 / 3) + (((- 1) |^ (0 + 2)) / (3 * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2)))))
by WSIERP_1:1
;
then A5:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A5, A2);
hence
for n being Nat holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))
; verum