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

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