let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = 1 / ((n + 1) ^2) ) implies for n being Nat holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 <= 2 - (1 / ($1 + 1));
assume A1: for n being Nat holds s . n = 1 / ((n + 1) ^2) ; :: thesis: for n being Nat holds (Partial_Sums s) . n <= 2 - (1 / (n + 1))
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ; :: thesis: S₁[n + 1]
then A3: ((Partial_Sums s) . n) + (1 / ((n + 2) ^2)) <= (2 - (1 / (n + 1))) + (1 / ((n + 2) ^2)) by XREAL_1:7;
((n ^2) + (3 * n)) + 3 > ((n ^2) + (3 * n)) + 2 by XREAL_1:8;
then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > ((n + 2) * (n + 1)) / (((n + 2) ^2) * (n + 1)) by XREAL_1:74;
then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > (n + 2) / ((n + 2) * (n + 2)) by XCMPLX_1:91;
then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > ((n + 2) / (n + 2)) / (n + 2) by XCMPLX_1:78;
then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > 1 / (n + 2) by XCMPLX_1:60;
then (- 1) * ((((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2))) < (- 1) * (1 / (n + 2)) by XREAL_1:69;
then A4: (- ((((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)))) + 2 < (- (1 / (n + 2))) + 2 by XREAL_1:8;
(Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums s) . n) + (1 / (((n + 1) + 1) ^2)) by A1 ;
then (Partial_Sums s) . (n + 1) <= 2 - ((1 / (n + 1)) - (1 / ((n + 2) ^2))) by A3;
then (Partial_Sums s) . (n + 1) <= 2 - (((1 * ((n + 2) ^2)) - (1 * (n + 1))) / ((n + 1) * ((n + 2) ^2))) by XCMPLX_1:130;
hence S₁[n + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

(Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1
.= 1 / ((0 + 1) ^2) by A1
.= 1 ;
then A5: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A2);
hence for n being Nat holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ; :: thesis: verum