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