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) )
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)
defpred S1[ Nat] means (Partial_Sums s) . $1 > ((2 / 3) * $1) * (sqrt $1);
(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:83
;
then A2:
S1[1]
by SQUARE_1:83;
A3:
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 A4:
(
n >= 1 &
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) )
;
:: thesis: S1[n + 1]
then
3
* n >= 3
* 1
by XREAL_1:66;
then
3
* n > 1
by XXREAL_0:2;
then
1
- (3 * n) < 0
by XREAL_1:51;
then
((1 + (n - (4 * n))) + ((4 * (n ^2 )) - (4 * (n ^2 )))) + (4 * (n |^ 3)) < 0 + (4 * (n |^ 3))
by XREAL_1:10;
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:11;
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:100;
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:11;
then
(((4 * (n ^2 )) - (4 * n)) + 1) * (n + 1) < (4 * (n |^ 2)) * n
;
then A5:
(((2 * n) - 1) ^2 ) * (n + 1) < (4 * (n ^2 )) * n
by NEWTON:100;
A6:
2
* n >= 2
* 1
by A4, XREAL_1:66;
then
2
* n > 1
by XXREAL_0:2;
then A7:
(2 * n) - 1
> 0
by XREAL_1:52;
then
((2 * n) - 1) ^2 > 0
;
then
(n + 1) / n < ((2 * n) ^2 ) / (((2 * n) - 1) ^2 )
by A4, A5, XREAL_1:108;
then
(n + 1) / n < ((2 * n) / ((2 * n) - 1)) ^2
by XCMPLX_1:77;
then A8:
sqrt ((n + 1) / n) < sqrt (((2 * n) / ((2 * n) - 1)) ^2 )
by SQUARE_1:95;
(2 * n) / ((2 * n) - 1) > 0
by A6, A7;
then
sqrt ((n + 1) / n) < (2 * n) / ((2 * n) - 1)
by A8, SQUARE_1:89;
then A9:
(sqrt (n + 1)) / (sqrt n) < (2 * n) / ((2 * n) - 1)
by SQUARE_1:99;
sqrt n > 0
by A4, SQUARE_1:93;
then
(1 / 3) * ((sqrt (n + 1)) * ((2 * n) - 1)) < (1 / 3) * ((2 * n) * (sqrt n))
by A7, A9, XREAL_1:70, XREAL_1:104;
then
(Partial_Sums s) . n > (((2 / 3) * (n + 1)) * (sqrt (n + 1))) - (sqrt (n + 1))
by A4, XXREAL_0:2;
then A10:
((Partial_Sums s) . n) + (sqrt (n + 1)) > ((((2 / 3) * (n + 1)) * (sqrt (n + 1))) - (sqrt (n + 1))) + (sqrt (n + 1))
by XREAL_1:10;
A11:
n in NAT
by ORDINAL1:def 13;
n + 1
>= 1
+ 1
by A4, XREAL_1:9;
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, A10;
hence
S1[
n + 1]
by A11, SERIES_1:def 1;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A2, A3);
hence
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n)
; :: thesis: verum