let e be positive Real; for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ) holds
( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
let f be Real_Sequence; ( ( for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ) implies ( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 ) )
assume A1:
for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e))
; ( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
set g = seq_n^ e;
set h = f /" (seq_n^ e);
A2:
now for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < plet p be
Real;
( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < p )reconsider p1 =
p as
Real ;
set i0 =
[/((7 / p1) to_power (1 / e))\];
set i1 =
[/((p1 to_power (- (2 / e))) + 1)\];
set N =
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2);
A3:
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2)
>= max (
[/((7 / p1) to_power (1 / e))\],
[/((p1 to_power (- (2 / e))) + 1)\])
by XXREAL_0:25;
A4:
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) is
Integer
A5:
(p to_power (- (2 / e))) + 1
> (p to_power (- (2 / e))) + 0
by XREAL_1:8;
[/((p1 to_power (- (2 / e))) + 1)\] >= (p to_power (- (2 / e))) + 1
by INT_1:def 7;
then A6:
[/((p1 to_power (- (2 / e))) + 1)\] > p to_power (- (2 / e))
by A5, XXREAL_0:2;
assume A7:
p > 0
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < pthen A8:
p1 to_power 2
> 0
by POWER:34;
max (
[/((7 / p1) to_power (1 / e))\],
[/((p1 to_power (- (2 / e))) + 1)\])
>= [/((p1 to_power (- (2 / e))) + 1)\]
by XXREAL_0:25;
then A9:
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2)
>= [/((p1 to_power (- (2 / e))) + 1)\]
by A3, XXREAL_0:2;
A10:
[/((7 / p1) to_power (1 / e))\] >= (7 / p) to_power (1 / e)
by INT_1:def 7;
max (
[/((7 / p1) to_power (1 / e))\],
[/((p1 to_power (- (2 / e))) + 1)\])
>= [/((7 / p1) to_power (1 / e))\]
by XXREAL_0:25;
then A11:
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2)
>= [/((7 / p1) to_power (1 / e))\]
by A3, XXREAL_0:2;
A12:
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2)
>= 2
by XXREAL_0:25;
A13:
p1 to_power (- (2 / e)) > 0
by A7, POWER:34;
A14:
7
* (p ") > 7
* 0
by A7, XREAL_1:68;
then A15:
(7 / p1) to_power (1 / e) > 0
by POWER:34;
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2)
in NAT
by A12, A4, INT_1:3;
then reconsider N =
max (
(max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) as
Nat ;
take N =
N;
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < plet n be
Nat;
( n >= N implies |.(((f /" (seq_n^ e)) . n) - 0).| < p )set c =
p1 * (n to_power e);
assume A16:
n >= N
;
|.(((f /" (seq_n^ e)) . n) - 0).| < pthen
n >= [/((7 / p1) to_power (1 / e))\]
by A11, XXREAL_0:2;
then
n >= (7 / p) to_power (1 / e)
by A10, XXREAL_0:2;
then
n to_power e >= ((7 / p) to_power (1 / e)) to_power e
by A15, Lm6;
then
n to_power e >= (7 / p1) to_power (e * (1 / e))
by A14, POWER:33;
then
n to_power e >= (7 / p) to_power 1
by XCMPLX_1:106;
then
n to_power e >= 7
/ p1
by POWER:25;
then
p * (n to_power e) >= (7 / p) * p
by A7, XREAL_1:64;
then
p * (n to_power e) >= 7
by A7, XCMPLX_1:87;
then
p * (n to_power e) > 6
by XXREAL_0:2;
then A17:
(p1 * (n to_power e)) ^2 < 2
to_power (p1 * (n to_power e))
by Lm9;
n >= [/((p1 to_power (- (2 / e))) + 1)\]
by A9, A16, XXREAL_0:2;
then
n > p to_power (- (2 / e))
by A6, XXREAL_0:2;
then
n to_power e > (p to_power (- (2 / e))) to_power e
by A13, POWER:37;
then
n to_power e > p1 to_power ((- (2 / e)) * e)
by A7, POWER:33;
then
n to_power e > p to_power (- ((2 / e) * e))
;
then
n to_power e > p to_power (- 2)
by XCMPLX_1:87;
then
(p to_power 2) * (n to_power e) > (p to_power 2) * (p to_power (- 2))
by A8, XREAL_1:68;
then
(p1 to_power 2) * (n to_power e) > p1 to_power (2 + (- 2))
by A7, POWER:27;
then
(p1 to_power 2) * (n to_power e) > 1
by POWER:24;
then
(p1 ^2) * (n to_power e) > 1
by POWER:46;
then A18:
1
/ (p * (p1 * (n to_power e))) < 1
/ 1
by XREAL_1:88;
2
to_power (p1 * (n to_power e)) > 0
by POWER:34;
then A19:
(2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p) < (2 to_power (p1 * (n to_power e))) * 1
by A18, XREAL_1:68;
A20:
n to_power e > 0
by A12, A16, POWER:34;
then
p * (n to_power e) > p * 0
by A7, XREAL_1:68;
then
p1 * (n to_power e) < (2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e))
by A17, XREAL_1:81;
then
n to_power e < ((2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e))) / p
by A7, XREAL_1:81;
then
n to_power e < (2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p)
by XCMPLX_1:78;
then
n to_power e < 2
to_power (p1 * (n to_power e))
by A19, XXREAL_0:2;
then
log (2,
(n to_power e))
< log (2,
(2 to_power (p1 * (n to_power e))))
by A20, POWER:57;
then
log (2,
(n to_power e))
< (p1 * (n to_power e)) * (log (2,2))
by POWER:55;
then
log (2,
(n to_power e))
< (p1 * (n to_power e)) * 1
by POWER:52;
then A21:
(log (2,(n to_power e))) / (n to_power e) < p
by A12, A16, POWER:34, XREAL_1:83;
n >= 2
by A12, A16, XXREAL_0:2;
then
n > 1
by XXREAL_0:2;
then
n to_power e > n to_power 0
by POWER:39;
then
n to_power e > 1
by POWER:24;
then
log (2,
(n to_power e))
> log (2,1)
by POWER:57;
then A22:
log (2,
(n to_power e))
> 0
by POWER:51;
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 12;
(f /" (seq_n^ e)) . n =
(f . n) / ((seq_n^ e) . nn)
by Lm4
.=
(log (2,(nn to_power e))) / ((seq_n^ e) . n)
by A1, A12, A16
.=
(log (2,(nn to_power e))) / (n to_power e)
by A12, A16, Def3
;
hence
|.(((f /" (seq_n^ e)) . n) - 0).| < p
by A20, A21, A22, ABSVALUE:def 1;
verum end;
hence
f /" (seq_n^ e) is convergent
by SEQ_2:def 6; lim (f /" (seq_n^ e)) = 0
hence
lim (f /" (seq_n^ e)) = 0
by A2, SEQ_2:def 7; verum