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