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 )
proof
per cases ( 0 < r0 or not 0 < r0 ) ;
suppose A1: 0 < r0 ; :: thesis: ex r being Real st
( 0 < r & r0 <= r )

take r0 ; :: thesis: ( 0 < r0 & r0 <= r0 )
thus ( 0 < r0 & r0 <= r0 ) by A1; :: thesis: verum
end;
suppose A2: not 0 < r0 ; :: thesis: ex r being Real st
( 0 < r & r0 <= r )

take 1 ; :: thesis: ( 0 < 1 & r0 <= 1 )
thus ( 0 < 1 & r0 <= 1 ) by A2; :: thesis: verum
end;
end;
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 ;
then reconsider k = [/(max ((log (2,r)),number_e))\] + 1 as Nat ;
A0: ( log (2,r) < k & number_e < k ) by ;
2 to_power (log (2,r)) < 2 to_power k by ;
then A1: r < 2 to_power k by ;
consider N being Nat such that
A2: for n being Nat st N <= n holds
2 to_power k <= n / (log (2,n)) by ;
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 ;
hence r0 < n / (log (2,n)) by ; :: thesis: verum