let k be Nat; ( number_e < k implies ex N being Nat st
for n being Nat st N <= n holds
2 to_power k <= n / (log (2,n)) )
assume K1:
number_e < k
; ex N being Nat st
for n being Nat st N <= n holds
2 to_power k <= n / (log (2,n))
set N = 2 to_power ((2 * k) + 1);
k * 1 <= 2 * k
by XREAL_1:64;
then X1:
k + 0 < (2 * k) + 1
by XREAL_1:8;
(2 * k) + 1 <= 2 to_power ((2 * k) + 1)
by LMC31X;
then
k < 2 to_power ((2 * k) + 1)
by X1, XXREAL_0:2;
then DD:
number_e < 2 to_power ((2 * k) + 1)
by K1, XXREAL_0:2;
take
2 to_power ((2 * k) + 1)
; for n being Nat st 2 to_power ((2 * k) + 1) <= n holds
2 to_power k <= n / (log (2,n))
let n be Nat; ( 2 to_power ((2 * k) + 1) <= n implies 2 to_power k <= n / (log (2,n)) )
assume
2 to_power ((2 * k) + 1) <= n
; 2 to_power k <= n / (log (2,n))
then B0:
(2 to_power ((2 * k) + 1)) / (log (2,(2 to_power ((2 * k) + 1)))) <= n / (log (2,n))
by LMC31H1, DD;
X0:
0 < 2 to_power ((2 * k) + 1)
by POWER:34;
then X1:
(2 * k) + 1 = log (2,(2 to_power ((2 * k) + 1)))
by POWER:def 3;
reconsider m = log (2,(2 to_power ((2 * k) + 1))) as Nat by X0, POWER:def 3;
X3:
2 to_power k <= (2 to_power m) / m
by LMC31G, X1;
2 to_power m = 2 to_power ((2 * k) + 1)
by POWER:def 3, X0;
hence
2 to_power k <= n / (log (2,n))
by B0, XXREAL_0:2, X3; verum