reconsider k = [/number_e\] + 1 as Integer ;

LLC2: number_e <= [/number_e\] by INT_1:def 7;

then LC2: number_e < k by XREAL_1:145;

then LC3: 2 < k by XXREAL_0:2, TAYLOR_1:11;

k in NAT by INT_1:3, LLC2, TAYLOR_1:11;

then reconsider k = k as Nat ;

consider N being Nat such that

LC4: for n being Nat st N <= n holds

2 to_power k <= n / (log (2,n)) by LMC31H, LC2;

reconsider N = N as Element of NAT by ORDINAL1:def 12;

take N ; :: thesis: for n being Nat st N <= n holds

4 < n / (log (2,n))

let n be Nat; :: thesis: ( N <= n implies 4 < n / (log (2,n)) )

assume N <= n ; :: thesis: 4 < n / (log (2,n))

then LC5: 2 to_power k <= n / (log (2,n)) by LC4;

4 < 2 to_power k by POWER:60, POWER:39, LC3;

hence 4 < n / (log (2,n)) by LC5, XXREAL_0:2; :: thesis: verum

LLC2: number_e <= [/number_e\] by INT_1:def 7;

then LC2: number_e < k by XREAL_1:145;

then LC3: 2 < k by XXREAL_0:2, TAYLOR_1:11;

k in NAT by INT_1:3, LLC2, TAYLOR_1:11;

then reconsider k = k as Nat ;

consider N being Nat such that

LC4: for n being Nat st N <= n holds

2 to_power k <= n / (log (2,n)) by LMC31H, LC2;

reconsider N = N as Element of NAT by ORDINAL1:def 12;

take N ; :: thesis: for n being Nat st N <= n holds

4 < n / (log (2,n))

let n be Nat; :: thesis: ( N <= n implies 4 < n / (log (2,n)) )

assume N <= n ; :: thesis: 4 < n / (log (2,n))

then LC5: 2 to_power k <= n / (log (2,n)) by LC4;

4 < 2 to_power k by POWER:60, POWER:39, LC3;

hence 4 < n / (log (2,n)) by LC5, XXREAL_0:2; :: thesis: verum