let s be Real_Sequence; ( ( 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 > ((2 / 3) * n) * (sqrt n) )
defpred S1[ Nat] means (Partial_Sums s) . $1 > ((2 / 3) * $1) * (sqrt $1);
assume A1:
for n being Nat st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 )
; for n being Nat st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n)
A2:
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 A3:
n >= 1
and A4:
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n)
;
S1[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;
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
S1[
n + 1]
by SERIES_1:def 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
.=
0 + (s . 1)
by A1
.=
1
by A1, SQUARE_1:18
;
then A8:
S1[1]
by SQUARE_1:18;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A8, A2);
hence
for n being Nat st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n)
; verum