let x be Nat; ( 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
; 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
; ex c being Nat st
for n being Nat st N <= n holds
n to_power x <= c * (x to_power n)
take
c
; for n being Nat st N <= n holds
n to_power x <= c * (x to_power n)
let n be Nat; ( N <= n implies n to_power x <= c * (x to_power n) )
assume AS2:
N <= n
; 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; verum