let r0 be Real; :: thesis: ex N being Element of NAT st

for n being Nat st N <= n holds

r0 < n / (log (2,n))

ex r being Real st

( 0 < r & r0 <= r )

AS: ( 0 < r & r0 <= r ) ;

set a0 = max ((log (2,r)),number_e);

A01: ( log (2,r) <= max ((log (2,r)),number_e) & number_e <= max ((log (2,r)),number_e) ) by XXREAL_0:25;

set k = [/(max ((log (2,r)),number_e))\] + 1;

max ((log (2,r)),number_e) < [/(max ((log (2,r)),number_e))\] + 1 by INT_1:32;

then [/(max ((log (2,r)),number_e))\] + 1 in NAT by INT_1:3, TAYLOR_1:11, A01;

then reconsider k = [/(max ((log (2,r)),number_e))\] + 1 as Nat ;

A0: ( log (2,r) < k & number_e < k ) by A01, XXREAL_0:2, INT_1:32;

2 to_power (log (2,r)) < 2 to_power k by A0, POWER:39;

then A1: r < 2 to_power k by AS, POWER:def 3;

consider N being Nat such that

A2: for n being Nat st N <= n holds

2 to_power k <= n / (log (2,n)) by LMC31H, A0;

reconsider N = N as Element of NAT by ORDINAL1:def 12;

take N ; :: thesis: for n being Nat st N <= n holds

r0 < n / (log (2,n))

let n be Nat; :: thesis: ( N <= n implies r0 < n / (log (2,n)) )

assume N <= n ; :: thesis: r0 < n / (log (2,n))

then 2 to_power k <= n / (log (2,n)) by A2;

then r < n / (log (2,n)) by A1, XXREAL_0:2;

hence r0 < n / (log (2,n)) by AS, XXREAL_0:2; :: thesis: verum

for n being Nat st N <= n holds

r0 < n / (log (2,n))

ex r being Real st

( 0 < r & r0 <= r )

proof
end;

then consider r being Real such that AS: ( 0 < r & r0 <= r ) ;

set a0 = max ((log (2,r)),number_e);

A01: ( log (2,r) <= max ((log (2,r)),number_e) & number_e <= max ((log (2,r)),number_e) ) by XXREAL_0:25;

set k = [/(max ((log (2,r)),number_e))\] + 1;

max ((log (2,r)),number_e) < [/(max ((log (2,r)),number_e))\] + 1 by INT_1:32;

then [/(max ((log (2,r)),number_e))\] + 1 in NAT by INT_1:3, TAYLOR_1:11, A01;

then reconsider k = [/(max ((log (2,r)),number_e))\] + 1 as Nat ;

A0: ( log (2,r) < k & number_e < k ) by A01, XXREAL_0:2, INT_1:32;

2 to_power (log (2,r)) < 2 to_power k by A0, POWER:39;

then A1: r < 2 to_power k by AS, POWER:def 3;

consider N being Nat such that

A2: for n being Nat st N <= n holds

2 to_power k <= n / (log (2,n)) by LMC31H, A0;

reconsider N = N as Element of NAT by ORDINAL1:def 12;

take N ; :: thesis: for n being Nat st N <= n holds

r0 < n / (log (2,n))

let n be Nat; :: thesis: ( N <= n implies r0 < n / (log (2,n)) )

assume N <= n ; :: thesis: r0 < n / (log (2,n))

then 2 to_power k <= n / (log (2,n)) by A2;

then r < n / (log (2,n)) by A1, XXREAL_0:2;

hence r0 < n / (log (2,n)) by AS, XXREAL_0:2; :: thesis: verum