let x be Nat; :: thesis: ( 1 < x implies for N, c being Nat ex n being Nat st

( N <= n & not x to_power n <= c * (n to_power x) ) )

assume AS: 1 < x ; :: thesis: for N, c being Nat ex n being Nat st

( N <= n & not x to_power n <= c * (n to_power x) )

assume CNT: ex N, c being Nat st

for n being Nat st N <= n holds

x to_power n <= c * (n to_power x) ; :: thesis: contradiction

ex N, c being Nat st

for n being Nat st N <= n holds

2 to_power n <= c * (n to_power x)

( N <= n & not x to_power n <= c * (n to_power x) ) )

assume AS: 1 < x ; :: thesis: for N, c being Nat ex n being Nat st

( N <= n & not x to_power n <= c * (n to_power x) )

assume CNT: ex N, c being Nat st

for n being Nat st N <= n holds

x to_power n <= c * (n to_power x) ; :: thesis: contradiction

ex N, c being Nat st

for n being Nat st N <= n holds

2 to_power n <= c * (n to_power x)

proof

hence
contradiction
by AS, N2POWINPOLY; :: thesis: verum
consider N, c being Nat such that

CNT2: for n being Nat st N <= n holds

x to_power n <= c * (n to_power x) by CNT;

take N ; :: thesis: ex c being Nat st

for n being Nat st N <= n holds

2 to_power n <= c * (n to_power x)

take c ; :: thesis: for n being Nat st N <= n holds

2 to_power n <= c * (n to_power x)

let n be Nat; :: thesis: ( N <= n implies 2 to_power n <= c * (n to_power x) )

assume N <= n ; :: thesis: 2 to_power n <= c * (n to_power x)

then LCX1: x to_power n <= c * (n to_power x) by CNT2;

1 + 1 <= x by AS, INT_1:7;

then 2 to_power n <= x to_power n by LEMC01;

hence 2 to_power n <= c * (n to_power x) by LCX1, XXREAL_0:2; :: thesis: verum

end;CNT2: for n being Nat st N <= n holds

x to_power n <= c * (n to_power x) by CNT;

take N ; :: thesis: ex c being Nat st

for n being Nat st N <= n holds

2 to_power n <= c * (n to_power x)

take c ; :: thesis: for n being Nat st N <= n holds

2 to_power n <= c * (n to_power x)

let n be Nat; :: thesis: ( N <= n implies 2 to_power n <= c * (n to_power x) )

assume N <= n ; :: thesis: 2 to_power n <= c * (n to_power x)

then LCX1: x to_power n <= c * (n to_power x) by CNT2;

1 + 1 <= x by AS, INT_1:7;

then 2 to_power n <= x to_power n by LEMC01;

hence 2 to_power n <= c * (n to_power x) by LCX1, XXREAL_0:2; :: thesis: verum