let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 > ((2 / 3) * $1) * (sqrt $1);
assume A1: for n being Element of NAT st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ; :: thesis: for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (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 > ((2 / 3) * n) * (sqrt n) ; :: thesis: S₁[n + 1]
2 * n >= 2 * 1 by A3, XREAL_1:64;
then 2 * n > 1 by XXREAL_0:2;
then A5: (2 * n) - 1 > 0 by XREAL_1:50;
3 * n >= 3 * 1 by A3, XREAL_1:64;
then 3 * n > 1 by XXREAL_0:2;
then 1 - (3 * n) < 0 by XREAL_1:49;
then ((1 + (n - (4 * n))) + ((4 * (n ^2)) - (4 * (n ^2)))) + (4 * (n |^ 3)) < 0 + (4 * (n |^ 3)) by XREAL_1:8;
then (((4 * (n |^ (2 + 1))) - (4 * (n ^2))) + n) + (((4 * (n ^2)) - (4 * n)) + 1) < 4 * (n |^ 3) ;
then (((4 * ((n |^ 2) * n)) - (4 * (n * n))) + n) + (((4 * (n ^2)) - (4 * n)) + 1) < 4 * (n |^ 3) by NEWTON:6;
then ((((4 * (n |^ 2)) - (4 * n)) + 1) * n) + ((((4 * (n ^2)) - (4 * n)) + 1) * 1) < 4 * (n |^ 3) ;
then ((((4 * (n ^2)) - (4 * n)) + 1) * n) + ((((4 * (n ^2)) - (4 * n)) + 1) * 1) < 4 * (n |^ 3) by NEWTON:81;
then (((4 * (n ^2)) - (4 * n)) + 1) * (n + 1) < 4 * (n |^ (2 + 1)) ;
then (((4 * (n ^2)) - (4 * n)) + 1) * (n + 1) < 4 * ((n |^ 2) * n) by NEWTON:6;
then (((4 * (n ^2)) - (4 * n)) + 1) * (n + 1) < (4 * (n |^ 2)) * n ;
then (((2 * n) - 1) ^2) * (n + 1) < (4 * (n ^2)) * n by NEWTON:81;
then (n + 1) / n < ((2 * n) ^2) / (((2 * n) - 1) ^2) by A3, A5, XREAL_1:106;
then (n + 1) / n < ((2 * n) / ((2 * n) - 1)) ^2 by XCMPLX_1:76;
then sqrt ((n + 1) / n) < sqrt (((2 * n) / ((2 * n) - 1)) ^2) by SQUARE_1:27;
then sqrt ((n + 1) / n) < (2 * n) / ((2 * n) - 1) by A5, SQUARE_1:22;
then A6: (sqrt (n + 1)) / (sqrt n) < (2 * n) / ((2 * n) - 1) by SQUARE_1:30;
sqrt n > 0 by A3, SQUARE_1:25;
then (1 / 3) * ((sqrt (n + 1)) * ((2 * n) - 1)) < (1 / 3) * ((2 * n) * (sqrt n)) by A5, A6, XREAL_1:68, XREAL_1:102;
then (Partial_Sums s) . n > (((2 / 3) * (n + 1)) * (sqrt (n + 1))) - (sqrt (n + 1)) by A4, XXREAL_0:2;
then A7: ((Partial_Sums s) . n) + (sqrt (n + 1)) > ((((2 / 3) * (n + 1)) * (sqrt (n + 1))) - (sqrt (n + 1))) + (sqrt (n + 1)) by XREAL_1:8;
A8: n in NAT by ORDINAL1:def 12;
n + 1 >= 1 + 1 by A3, XREAL_1:7;
then n + 1 >= 1 by XXREAL_0:2;
then ((Partial_Sums s) . n) + (s . (n + 1)) > ((2 / 3) * (n + 1)) * (sqrt (n + 1)) by A1, A7;
hence S₁[n + 1] by A8, 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 A9: S₁[1] by SQUARE_1:18;
for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A9, A2);
hence for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) ; :: thesis: verum