set f = seq_logn ;
let e be Real; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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; :: thesis: 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 ; :: thesis: ( n >= N1 implies (n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) )
assume A9: n >= N1 ; :: thesis: (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)) ; :: thesis: 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)) ; :: thesis: 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)) ; :: thesis: verum