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)
proof
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;
hence contradiction by AS, N2POWINPOLY; :: thesis: verum