let x be Nat; :: thesis: ( 1 < x implies ex N, c being Nat st
for n being Nat st N <= n holds
n to_power x <= c * (x to_power n) )

assume AS1: 1 < x ; :: thesis: ex N, c being Nat st
for n being Nat st N <= n holds
n to_power x <= c * (x to_power n)

consider N0 being Element of NAT such that
P1: for n being Nat st N0 <= n holds
x / (log (2,x)) < n / (log (2,n)) by LMC31;
set N = N0 + 2;
reconsider N = N0 + 2 as Nat ;
reconsider c = 1 as Element of NAT ;
take N ; :: thesis: ex c being Nat st
for n being Nat st N <= n holds
n to_power x <= c * (x to_power n)

take c ; :: thesis: for n being Nat st N <= n holds
n to_power x <= c * (x to_power n)

let n be Nat; :: thesis: ( N <= n implies n to_power x <= c * (x to_power n) )
assume AS2: N <= n ; :: thesis: n to_power x <= c * (x to_power n)
N0 <= N by NAT_1:12;
then N0 <= n by ;
then E1: x / (log (2,x)) < n / (log (2,n)) by P1;
1 + 1 <= x by ;
then log (2,2) <= log (2,x) by PRE_FF:10;
then P2: 0 < log (2,x) by POWER:52;
2 <= N by NAT_1:11;
then 2 <= n by ;
then log (2,2) <= log (2,n) by PRE_FF:10;
then P3: 0 < log (2,n) by POWER:52;
then (x / (log (2,x))) * (log (2,n)) < (n / (log (2,n))) * (log (2,n)) by ;
then (x / (log (2,x))) * (log (2,n)) < n by ;
then ((log (2,n)) * (x / (log (2,x)))) * (log (2,x)) < n * (log (2,x)) by ;
then (log (2,n)) * ((x / (log (2,x))) * (log (2,x))) < n * (log (2,x)) ;
then PP4: (log (2,n)) * x < n * (log (2,x)) by ;
P5: 2 to_power ((log (2,n)) * x) = (2 to_power (log (2,n))) to_power x by POWER:33
.= n to_power x by ;
2 to_power (n * (log (2,x))) = (2 to_power (log (2,x))) to_power n by POWER:33
.= x to_power n by ;
hence n to_power x <= c * (x to_power n) by ; :: thesis: verum