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 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