set f = seq_logn ;
let e be Real; ( 0 < e & e < 1 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) )
assume that
A1:
0 < e
and
A2:
e < 1
; ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))
set d = log (2,(1 + e));
set g = seq_n^ e;
set h = seq_logn /" (seq_n^ e);
A3:
seq_logn /" (seq_n^ e) is convergent
by A1, Lm11;
A4:
lim (seq_logn /" (seq_n^ e)) = 0
by A1, Lm11;
0 + 1 < e + 1
by A1, XREAL_1:6;
then
log (2,1) < log (2,(e + 1))
by POWER:57;
then A5:
log (2,(1 + e)) > 0
by POWER:51;
then
(log (2,(1 + e))) * (1 / 16) > (log (2,(1 + e))) * 0
by XREAL_1:68;
then consider N being Nat such that
A6:
for n being Nat st n >= N holds
|.(((seq_logn /" (seq_n^ e)) . n) - 0).| < (log (2,(1 + e))) / 16
by A3, A4, SEQ_2:def 7;
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))
proof
reconsider N1 =
max (2,
N) as
Element of
NAT by ORDINAL1:def 12;
A7:
N1 >= 2
by XXREAL_0:25;
A8:
N1 >= N
by XXREAL_0:25;
now ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))take N1 =
N1;
for n being Element of NAT st n >= N1 holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))let n be
Element of
NAT ;
( n >= N1 implies (n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) )assume A9:
n >= N1
;
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))then A10:
n to_power e > 0
by A7, POWER:34;
A11:
n >= 2
by A7, A9, XXREAL_0:2;
then
log (2,2)
<= log (2,
n)
by PRE_FF:10;
then A12:
1
<= log (2,
n)
by POWER:52;
A13:
(seq_logn /" (seq_n^ e)) . n =
(seq_logn . n) / ((seq_n^ e) . n)
by Lm4
.=
(log (2,n)) / ((seq_n^ e) . n)
by A7, A9, Def2
.=
(log (2,n)) / (n to_power e)
by A7, A9, Def3
;
n > 1
by A11, XXREAL_0:2;
then
n to_power 1
> n to_power e
by A2, POWER:39;
then
1
/ (n to_power 1) < 1
/ (n to_power e)
by A10, XREAL_1:88;
then
1
/ n < 1
/ (n to_power e)
by POWER:25;
then A14:
(log (2,n)) / n < (log (2,n)) * (1 / (n to_power e))
by A12, XREAL_1:68;
n >= N
by A8, A9, XXREAL_0:2;
then
|.(((seq_logn /" (seq_n^ e)) . n) - 0).| < (log (2,(1 + e))) / 16
by A6;
then
(seq_logn /" (seq_n^ e)) . n < (log (2,(1 + e))) / 16
by A12, A13, A10, ABSVALUE:def 1;
then A15:
(log (2,n)) / n < (log (2,(1 + e))) / 16
by A13, A14, XXREAL_0:2;
(log (2,n)) * (n ") > 0 * (n ")
by A7, A9, A12, XREAL_1:68;
then
1
/ ((log (2,n)) / n) > 1
/ ((log (2,(1 + e))) / 16)
by A15, XREAL_1:88;
then
n / (log (2,n)) > 1
/ ((log (2,(1 + e))) / 16)
by XCMPLX_1:57;
then
n / (log (2,n)) > 16
/ (log (2,(1 + e)))
by XCMPLX_1:57;
then
(log (2,(1 + e))) * (n / (log (2,n))) > (16 / (log (2,(1 + e)))) * (log (2,(1 + e)))
by A5, XREAL_1:68;
then
(log (2,(1 + e))) * (n / (log (2,n))) > 16
by A5, XCMPLX_1:87;
then
((log (2,(1 + e))) * (n / (log (2,n)))) * (log (2,n)) > 16
* (log (2,n))
by A12, XREAL_1:68;
then
(log (2,(1 + e))) * ((n / (log (2,n))) * (log (2,n))) > 16
* (log (2,n))
;
then
(log (2,(1 + e))) * n > (8 + 8) * (log (2,n))
by A12, XCMPLX_1:87;
then
((log (2,(1 + e))) * n) - (8 * (log (2,n))) > ((8 * (log (2,n))) + (8 * (log (2,n)))) - (8 * (log (2,n)))
by XREAL_1:9;
hence
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8
* (log (2,n))
;
verum end;
hence
ex
N being
Element of
NAT st
for
n being
Element of
NAT st
n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8
* (log (2,n))
;
verum
end;
hence
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))
; verum