let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ) implies for n being Element of 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))) )
assume A1:
for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3))
; :: thesis: for n being Element of 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
;
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)));
(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 A3:
S1[1]
;
A4:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume A5:
(
n >= 1 &
(Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) )
;
:: thesis: S1[n + 1]
n + 1
>= 1
+ 0
by NAT_1:11;
then A6:
n + 1
> 0
by NAT_1:13;
(
n + 2
>= 2 &
n + 3
>= 3 &
n + 4
>= 4 )
by NAT_1:11;
then A7:
(
n + 2
> 0 &
n + 3
> 0 &
n + 4
> 0 )
by XXREAL_0:2;
then A8:
(
(n + 1) * (n + 2) > 0 & 2
* (n + 1) > 0 )
by A6, XREAL_1:131;
then A9:
(
((n + 1) * (n + 2)) * (n + 3) > 0 &
((n + 1) * (n + 2)) * 3
> 0 )
by A7, XREAL_1:131;
then A10:
(((n + 1) * (n + 2)) * (n + 3)) * 6
> 0
by XREAL_1:131;
n in NAT
by ORDINAL1:def 13;
then (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 A5, 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 A7, XCMPLX_1:92
.=
((((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:92
.=
(((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:63
.=
(((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:92
.=
(((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:92
.=
(((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:92
.=
((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 A7, XCMPLX_1:92
.=
((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 A7, XCMPLX_1:92
.=
((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:63
.=
((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:92
.=
((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 A7, XCMPLX_1:92
.=
(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:121
.=
(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:63
.=
(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:63
.=
(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 A10, XCMPLX_1:92
.=
(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 A9, XCMPLX_1:92
.=
(29 / 36) - (((1 / (n + 4)) + (3 / ((2 * (n + 3)) * (n + 4)))) + (4 / (((3 * (n + 2)) * (n + 3)) * (n + 4))))
by A8, XCMPLX_1:92
.=
(((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]
;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A3, A4);
hence
for n being Element of 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)))
; :: thesis: verum