let k be Nat; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
x to_power k < 2 to_power x
consider N0 being Nat such that
P1: for x being Nat st N0 <= x holds
k < x / (log (2,x)) by LMC31;
set N = N0 + 2;
take N0 + 2 ; :: thesis: for x being Nat st N0 + 2 <= x holds
x to_power k < 2 to_power x

now :: thesis: for x being Nat st N0 + 2 <= x holds
x to_power k < 2 to_power x

let x be Nat; :: thesis: ( N0 + 2 <= x implies x to_power k < 2 to_power x )
assume AS2: N0 + 2 <= x ; :: thesis: x to_power k < 2 to_power x
N0 <= N0 + 2 by NAT_1:12;
then N0 <= x by XXREAL_0:2, AS2;
then E1: k < x / (log (2,x)) by P1;
2 <= N0 + 2 by NAT_1:11;
then 2 <= x by XXREAL_0:2, AS2;
then log (2,2) <= log (2,x) by PRE_FF:10;
then P3: 0 < log (2,x) by POWER:52;
then k * (log (2,x)) < (x / (log (2,x))) * (log (2,x)) by XREAL_1:68, E1;
then P4: k * (log (2,x)) < x by P3, XCMPLX_1:87;
2 to_power ((log (2,x)) * k) = (2 to_power (log (2,x))) to_power k by POWER:33
.= x to_power k by AS2, POWER:def 3 ;
hence x to_power k < 2 to_power x by P4, POWER:39; :: thesis: verum

end;

hence for x being Nat st N0 + 2 <= x holds
x to_power k < 2 to_power x ; :: thesis: verum