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:8;
then log 2,1 < log 2,(e + 1) by POWER:65;
then A5: log 2,(1 + e) > 0 by POWER:59;
then (log 2,(1 + e)) * (1 / 16) > (log 2,(1 + e)) * 0 by XREAL_1:70;
then consider N being Element of NAT such that
A6: for n being Element of NAT st n >= N holds
abs (((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

set N1 = max 2,N;
A7: max 2,N >= 2 by XXREAL_0:25;
A8: max 2,N >= N by XXREAL_0:25;

now

take N1 = max 2,N; :: 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:39;
A11: n >= 2 by A7, A9, XXREAL_0:2;
then log 2,2 <= log 2,n by PRE_FF:12;
then A12: 1 <= log 2,n by POWER:60;
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:44;
then 1 / (n to_power 1) < 1 / (n to_power e) by A10, XREAL_1:90;
then 1 / n < 1 / (n to_power e) by POWER:30;
then A14: (log 2,n) / n < (log 2,n) * (1 / (n to_power e)) by A12, XREAL_1:70;
n >= N by A8, A9, XXREAL_0:2;
then abs (((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:70;
then 1 / ((log 2,n) / n) > 1 / ((log 2,(1 + e)) / 16) by A15, XREAL_1:90;
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:70;
then (log 2,(1 + e)) * (n / (log 2,n)) > 16 by A5, XCMPLX_1:88;
then ((log 2,(1 + e)) * (n / (log 2,n))) * (log 2,n) > 16 * (log 2,n) by A12, XREAL_1:70;
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:88;
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:11;
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