let s be Real_Sequence; ( ( for n being Nat holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ) implies for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) )
defpred S1[ Nat] means (Partial_Sums s) . $1 = (((29 / 36) - (1 / ($1 + 3))) - (3 / ((2 * ($1 + 2)) * ($1 + 3)))) - (4 / (((3 * ($1 + 1)) * ($1 + 2)) * ($1 + 3)));
assume A1:
for n being Nat holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3))
; for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))
then A2: s . 0 =
(0 + 2) / ((0 * (0 + 1)) * (0 + 3))
.=
0
by XCMPLX_1:49
;
A3:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A4:
(Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))
;
S1[n + 1]
n + 4
>= 4
by NAT_1:11;
then A5:
n + 4
> 0
by XXREAL_0:2;
n + 1
>= 1
+ 0
by NAT_1:11;
then A6:
n + 1
> 0
by NAT_1:13;
then A7:
2
* (n + 1) > 0
by XREAL_1:129;
n + 2
>= 2
by NAT_1:11;
then A8:
n + 2
> 0
by XXREAL_0:2;
then A9:
(n + 1) * (n + 2) > 0
by A6, XREAL_1:129;
then A10:
((n + 1) * (n + 2)) * 3
> 0
by XREAL_1:129;
n + 3
>= 3
by NAT_1:11;
then A11:
n + 3
> 0
by XXREAL_0:2;
then
((n + 1) * (n + 2)) * (n + 3) > 0
by A9, XREAL_1:129;
then A12:
(((n + 1) * (n + 2)) * (n + 3)) * 6
> 0
by XREAL_1:129;
(Partial_Sums s) . (n + 1) =
((((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + (s . (n + 1))
by A4, SERIES_1:def 1
.=
((((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + (((n + 1) + 2) / (((n + 1) * ((n + 1) + 1)) * ((n + 1) + 3)))
by A1
.=
((((29 / 36) - ((1 * (n + 2)) / ((n + 3) * (n + 2)))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by A8, XCMPLX_1:91
.=
((((29 / 36) - (((n + 2) * 2) / (((n + 2) * (n + 3)) * 2))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by XCMPLX_1:91
.=
(((29 / 36) - ((((n + 2) * 2) / (((n + 2) * (n + 3)) * 2)) + (3 / ((2 * (n + 2)) * (n + 3))))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
.=
(((29 / 36) - ((((n + 2) * 2) + 3) / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by XCMPLX_1:62
.=
(((29 / 36) - ((((n * 2) + 7) * (n + 1)) / (((2 * (n + 2)) * (n + 3)) * (n + 1)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by A6, XCMPLX_1:91
.=
(((29 / 36) - (((((n * 2) + 7) * (n + 1)) * 3) / ((((2 * (n + 2)) * (n + 3)) * (n + 1)) * 3))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by XCMPLX_1:91
.=
(((29 / 36) - (((((n * 2) + 7) * (n + 1)) * 3) / ((((2 * (n + 2)) * (n + 3)) * (n + 1)) * 3))) - ((4 * 2) / ((((3 * (n + 1)) * (n + 2)) * (n + 3)) * 2))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by XCMPLX_1:91
.=
((29 / 36) - ((((((n * 2) + 7) * (n + 1)) * 3) / (((6 * (n + 2)) * (n + 3)) * (n + 1))) + (8 / (((6 * (n + 1)) * (n + 2)) * (n + 3))))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
.=
((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) / ((((6 * (n + 2)) * (n + 3)) * (n + 1)) * (n + 4))) + (8 / (((6 * (n + 1)) * (n + 2)) * (n + 3))))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by A5, XCMPLX_1:91
.=
((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) + ((8 * (n + 4)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by A5, XCMPLX_1:91
.=
((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4)))
by XCMPLX_1:62
.=
((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + (((n + 3) * 6) / ((((n + 1) * (n + 2)) * (n + 4)) * 6))
by XCMPLX_1:91
.=
((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + ((((n + 3) * 6) * (n + 3)) / (((((n + 1) * (n + 2)) * (n + 4)) * 6) * (n + 3)))
by A11, XCMPLX_1:91
.=
(29 / 36) - ((((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) - ((((n + 3) * 6) * (n + 3)) / (((((n + 1) * (n + 2)) * (n + 4)) * 6) * (n + 3))))
.=
(29 / 36) - ((((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) - (((n + 3) * 6) * (n + 3))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))
by XCMPLX_1:120
.=
(29 / 36) - ((((((6 * (n + 1)) * (n + 2)) * (n + 3)) + ((9 * (n + 1)) * (n + 2))) + (8 * (n + 1))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))
.=
(29 / 36) - ((((((6 * (n + 1)) * (n + 2)) * (n + 3)) + ((9 * (n + 1)) * (n + 2))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) + ((8 * (n + 1)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))))
by XCMPLX_1:62
.=
(29 / 36) - ((((1 * (((6 * (n + 1)) * (n + 2)) * (n + 3))) / ((n + 4) * (((6 * (n + 1)) * (n + 2)) * (n + 3)))) + (((9 * (n + 1)) * (n + 2)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + ((8 * (n + 1)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))))
by XCMPLX_1:62
.=
(29 / 36) - (((1 / (n + 4)) + ((3 * ((3 * (n + 1)) * (n + 2))) / (((2 * (n + 3)) * (n + 4)) * ((3 * (n + 1)) * (n + 2))))) + ((8 * (n + 1)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))))
by A12, XCMPLX_1:91
.=
(29 / 36) - (((1 / (n + 4)) + (3 / ((2 * (n + 3)) * (n + 4)))) + ((4 * (2 * (n + 1))) / ((((3 * (n + 2)) * (n + 3)) * (n + 4)) * (2 * (n + 1)))))
by A10, XCMPLX_1:91
.=
(29 / 36) - (((1 / (n + 4)) + (3 / ((2 * (n + 3)) * (n + 4)))) + (4 / (((3 * (n + 2)) * (n + 3)) * (n + 4))))
by A7, XCMPLX_1:91
.=
(((29 / 36) - (1 / ((n + 1) + 3))) - (3 / ((2 * ((n + 1) + 2)) * ((n + 1) + 3)))) - (4 / (((3 * ((n + 1) + 1)) * ((n + 1) + 2)) * ((n + 1) + 3)))
;
hence
S1[
n + 1]
;
verum
end;
(Partial_Sums s) . (1 + 0) =
((Partial_Sums s) . 0) + (s . (1 + 0))
by SERIES_1:def 1
.=
(s . 0) + (s . 1)
by SERIES_1:def 1
.=
(1 + 2) / ((1 * (1 + 1)) * (1 + 3))
by A1, A2
.=
(((29 / 36) - (1 / (1 + 3))) - (3 / ((2 * (1 + 2)) * (1 + 3)))) - (4 / (((3 * (1 + 1)) * (1 + 2)) * (1 + 3)))
;
then A13:
S1[1]
;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A13, A3);
hence
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))
; verum