let k be Nat; :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: 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; :: thesis: ( 2 to_power ((2 * k) + 1) <= n implies 2 to_power k <= n / (log (2,n)) )
assume 2 to_power ((2 * k) + 1) <= n ; :: thesis: 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; :: thesis: verum