let r0 be Real; ex N being Nat st
for n being Nat st N <= n holds
r0 < n / (log (2,n))
ex r being Real st
( 0 < r & r0 <= r )
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 ASYMPT_2:13, A0;
reconsider N = N as Element of NAT by ORDINAL1:def 12;
take
N
; for n being Nat st N <= n holds
r0 < n / (log (2,n))
thus
for n being Nat st N <= n holds
r0 < n / (log (2,n))
verum