let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ) implies for n being Nat st n >= 1 holds
(Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 < ((1 / 6) * ((4 * $1) + 3)) * (sqrt $1);
assume A1: for n being Nat st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ; :: thesis: for n being Nat st n >= 1 holds
(Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n)
A2: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
A3: n >= 1 and
A4: (Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) ; :: thesis: S₁[n + 1]
n + 1 >= 1 + 1 by A3, XREAL_1:7;
then n + 1 >= 1 by XXREAL_0:2;
then A5: s . (n + 1) = sqrt (n + 1) by A1;
0 + ((16 * (n ^2)) + (8 * n)) < 1 + ((16 * (n ^2)) + (8 * n)) by XREAL_1:8;
then ((16 * n) + 8) * n < 1 * (((16 * (n ^2)) + (8 * n)) + 1) ;
then ((4 * ((4 * n) + 1)) + 4) / (((4 * n) + 1) ^2) < 1 / n by A3, XREAL_1:106;
then ((4 * ((4 * n) + 1)) / (((4 * n) + 1) * ((4 * n) + 1))) + (4 / (((4 * n) + 1) ^2)) < 1 / n by XCMPLX_1:62;
then (4 / ((4 * n) + 1)) + (4 / (((4 * n) + 1) ^2)) < 1 / n by XCMPLX_1:91;
then 1 + ((4 / ((4 * n) + 1)) + (4 / (((4 * n) + 1) ^2))) < 1 + (1 / n) by XREAL_1:8;
then (1 + (4 / ((4 * n) + 1))) + (4 / (((4 * n) + 1) ^2)) < 1 + (1 / n) ;
then (1 + ((2 * 2) / ((4 * n) + 1))) + ((2 / ((4 * n) + 1)) ^2) < 1 + (1 / n) by XCMPLX_1:76;
then (1 + (2 * (2 / ((4 * n) + 1)))) + ((2 / ((4 * n) + 1)) ^2) < 1 + (1 / n) by XCMPLX_1:74;
then ((2 / ((4 * n) + 1)) + 1) ^2 < (1 + (n * 1)) / n by A3, XCMPLX_1:113;
then sqrt (((2 / ((4 * n) + 1)) + 1) ^2) < sqrt ((1 + n) / n) by SQUARE_1:27;
then (2 / ((4 * n) + 1)) + 1 < sqrt ((1 + n) / n) by SQUARE_1:22;
then (2 + (((4 * n) + 1) * 1)) / ((4 * n) + 1) < sqrt ((1 + n) / n) by XCMPLX_1:113;
then A6: ((4 * n) + 3) / ((4 * n) + 1) < (sqrt (1 + n)) / (sqrt n) by SQUARE_1:30;
sqrt n > 0 by A3, SQUARE_1:25;
then (1 / 6) * (((4 * n) + 3) * (sqrt n)) < (1 / 6) * ((sqrt (1 + n)) * ((4 * n) + 1)) by A6, XREAL_1:68, XREAL_1:102;
then (Partial_Sums s) . n < (((1 / 6) * (sqrt (1 + n))) * ((4 * n) + 7)) - (sqrt (1 + n)) by A4, XXREAL_0:2;
then A7: ((Partial_Sums s) . n) + (sqrt (1 + n)) < ((((1 / 6) * (sqrt (1 + n))) * ((4 * n) + 7)) - (sqrt (1 + n))) + (sqrt (1 + n)) by XREAL_1:8;
thus S₁[n + 1] by A5, A7, SERIES_1:def 1; :: thesis: 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
.= 0 + (s . 1) by A1
.= 1 by A1, SQUARE_1:18 ;
then A8: S₁[1] ;
for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A8, A2);
hence for n being Nat st n >= 1 holds
(Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) ; :: thesis: verum