for k being Nat st number_e < k holds
ex N being Nat st
for n being Nat st N <= n holds
2 to_power k <= n / (log (2,n))