let k be Nat; 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
; for x being Nat st N0 + 2 <= x holds
x to_power k < 2 to_power x
now for x being Nat st N0 + 2 <= x holds
x to_power k < 2 to_power xlet x be
Nat;
( N0 + 2 <= x implies x to_power k < 2 to_power x )assume AS2:
N0 + 2
<= x
;
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;
verum end;
hence
for x being Nat st N0 + 2 <= x holds
x to_power k < 2 to_power x
; verum