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 f = seq_logn ;
set g = seq_n^ e;
set h = seq_logn /" (seq_n^ e);
A3: ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) by A1, Lm16;
set d = log 2,(1 + e);
0 + 1 < e + 1 by A1, XREAL_1:8;
then log 2,1 < log 2,(e + 1) by POWER:65;
then A4: 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
A5: 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, 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;
A6: ( max 2,N >= 2 & 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 A7: n >= N1 ; :: thesis: (n * (log 2,(1 + e))) - (8 * (log 2,n)) > 8 * (log 2,n)
then A8: ( n >= 2 & n >= N ) by A6, XXREAL_0:2;
then A9: abs (((seq_logn /" (seq_n^ e)) . n) - 0 ) < (log 2,(1 + e)) / 16 by A5;
log 2,2 <= log 2,n by A8, PRE_FF:12;
then A10: 1 <= log 2,n by POWER:60;
A11: (seq_logn /" (seq_n^ e)) . n = (seq_logn . n) / ((seq_n^ e) . n) by Lm4
.= (log 2,n) / ((seq_n^ e) . n) by A6, A7, Def2
.= (log 2,n) / (n to_power e) by A6, A7, Def3 ;
A12: n to_power e > 0 by A6, A7, POWER:39;
then (n to_power e) " > 0 ;
then (log 2,n) * ((n to_power e) " ) > 0 * ((n to_power e) " ) by A10, XREAL_1:70;
then (seq_logn /" (seq_n^ e)) . n > 0 by A11;
then A13: (seq_logn /" (seq_n^ e)) . n < (log 2,(1 + e)) / 16 by A9, ABSVALUE:def 1;
n > 1 by A8, 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 A12, XREAL_1:90;
then 1 / n < 1 / (n to_power e) by POWER:30;
then (log 2,n) * (1 / n) < (log 2,n) * (1 / (n to_power e)) by A10, XREAL_1:70;
then (log 2,n) / n < (log 2,n) * (1 / (n to_power e)) ;
then (log 2,n) / n < (seq_logn /" (seq_n^ e)) . n by A11;
then A14: (log 2,n) / n < (log 2,(1 + e)) / 16 by A13, XXREAL_0:2;
n " > 0 by A6, A7;
then (log 2,n) * (n " ) > 0 * (n " ) by A10, XREAL_1:70;
then (log 2,n) / n > 0 ;
then 1 / ((log 2,n) / n) > 1 / ((log 2,(1 + e)) / 16) by A14, 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 A4, XREAL_1:70;
then (log 2,(1 + e)) * (n / (log 2,n)) > 16 by A4, XCMPLX_1:88;
then ((log 2,(1 + e)) * (n / (log 2,n))) * (log 2,n) > 16 * (log 2,n) by A10, 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 A10, 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