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 XXREAL_0:2, AS2;

then E1: x / (log (2,x)) < n / (log (2,n)) by P1;

1 + 1 <= x by AS1, NAT_1:13;

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 XXREAL_0:2, AS2;

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 XREAL_1:68, E1;

then (x / (log (2,x))) * (log (2,n)) < n by P3, XCMPLX_1:87;

then ((log (2,n)) * (x / (log (2,x)))) * (log (2,x)) < n * (log (2,x)) by XREAL_1:68, P2;

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 P2, XCMPLX_1:87;

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 POWER:def 3, AS2 ;

2 to_power (n * (log (2,x))) = (2 to_power (log (2,x))) to_power n by POWER:33

.= x to_power n by AS1, POWER:def 3 ;

hence n to_power x <= c * (x to_power n) by PP4, P5, POWER:39; :: thesis: verum

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 XXREAL_0:2, AS2;

then E1: x / (log (2,x)) < n / (log (2,n)) by P1;

1 + 1 <= x by AS1, NAT_1:13;

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 XXREAL_0:2, AS2;

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 XREAL_1:68, E1;

then (x / (log (2,x))) * (log (2,n)) < n by P3, XCMPLX_1:87;

then ((log (2,n)) * (x / (log (2,x)))) * (log (2,x)) < n * (log (2,x)) by XREAL_1:68, P2;

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 P2, XCMPLX_1:87;

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 POWER:def 3, AS2 ;

2 to_power (n * (log (2,x))) = (2 to_power (log (2,x))) to_power n by POWER:33

.= x to_power n by AS1, POWER:def 3 ;

hence n to_power x <= c * (x to_power n) by PP4, P5, POWER:39; :: thesis: verum