let x be Nat; :: thesis: ( 1 < x implies for N, c being Nat ex n being Nat st
( N <= n & not 2 to_power n <= c * (n to_power x) ) )
assume AS1: 1 < x ; :: thesis: for N, c being Nat ex n being Nat st
( N <= n & not 2 to_power n <= c * (n to_power x) )
assume ASC: ex N, c being Nat st
for n being Nat st N <= n holds
2 to_power n <= c * (n to_power x) ; :: thesis: contradiction
consider N being Nat such that
ASC1: ex c being Nat st
for n being Nat st N <= n holds
2 to_power n <= c * (n to_power x) by ASC;
N <> 0
proof
assume N = 0 ; :: thesis: contradiction
then consider c being Nat such that
LNT: for n being Nat st 0 <= n holds
2 to_power n <= c * (n to_power x) by ASC1;
2 to_power 0 <= c * (0 to_power x) by LNT;
then 2 to_power 0 <= c * 0 by POWER:42, AS1;
hence contradiction by POWER:24; :: thesis: verum
end;
then LPNN2: 0 < N ;
consider c being Nat such that
ASC2: for n being Nat st N <= n holds
2 to_power n <= c * (n to_power x) by ASC1;
ex n being Element of NAT st
( N <= n & 0 < n - (x / 4) )
proof
now :: thesis: ( ( x / 4 < N & ex n being Element of NAT st
( N <= n & 0 < n - (x / 4) ) ) or ( N <= x / 4 & ex n being Element of NAT st
( 0 < n - (x / 4) & N <= n ) ) )
per cases ( x / 4 < N or N <= x / 4 ) ;
case AC1: x / 4 < N ; :: thesis: ex n being Element of NAT st
( N <= n & 0 < n - (x / 4) )
reconsider n = N + 1 as Element of NAT ;
take n = n; :: thesis: ( N <= n & 0 < n - (x / 4) )
thus N <= n by INT_1:6; :: thesis: 0 < n - (x / 4)
then x / 4 < n by AC1, XXREAL_0:2;
hence 0 < n - (x / 4) by XREAL_1:50; :: thesis: verum
end;
case AC2: N <= x / 4 ; :: thesis: ex n being Element of NAT st
( 0 < n - (x / 4) & N <= n )
reconsider n = [/(x / 4)\] + 1 as Integer ;
AC33: x / 4 <= [/(x / 4)\] by INT_1:def 7;
then AC3: (x / 4) + 0 < [/(x / 4)\] + 1 by XREAL_1:8;
reconsider n = n as Element of NAT by INT_1:3, AC33;
take n = n; :: thesis: ( 0 < n - (x / 4) & N <= n )
thus 0 < n - (x / 4) by AC3, XREAL_1:50; :: thesis: N <= n
thus N <= n by AC3, AC2, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
( N <= n & 0 < n - (x / 4) ) ; :: thesis: verum
end;
then consider n being Element of NAT such that
ASC3: ( N <= n & 0 < n - (x / 4) ) ;
XC1: 2 to_power n <= c * (n to_power x) by ASC2, ASC3;
ZZ1: ( 0 < n & 1 < x ) by AS1, ASC3;
TEZ1: 0 < c
proof
assume not 0 < c ; :: thesis: contradiction
then 2 to_power n <= 0 * (n to_power x) by XC1;
hence contradiction by POWER:34; :: thesis: verum
end;
ASC22: for k being Nat st 1 <= k holds
2 to_power (k * n) <= c * ((k * n) to_power x)
proof
let k be Nat; :: thesis: ( 1 <= k implies 2 to_power (k * n) <= c * ((k * n) to_power x) )
assume 1 <= k ; :: thesis: 2 to_power (k * n) <= c * ((k * n) to_power x)
then 1 * N <= k * n by ASC3, XREAL_1:66;
hence 2 to_power (k * n) <= c * ((k * n) to_power x) by ASC2; :: thesis: verum
end;
HCL1: for k being Nat st 1 <= k holds
k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n)))
proof
let k be Nat; :: thesis: ( 1 <= k implies k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n))) )
assume ASK: 1 <= k ; :: thesis: k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n)))
then L1: 2 to_power (k * n) <= c * ((k * n) to_power x) by ASC22;
L3: 0 < (k * n) to_power x by POWER:34, LPNN2, ASC3, ASK;
0 < 2 to_power (k * n) by POWER:34;
then log (2,(2 to_power (k * n))) <= log (2,(c * ((k * n) to_power x))) by L1, CPOWER57;
then (k * n) * (log (2,2)) <= log (2,(c * ((k * n) to_power x))) by POWER:55;
then (k * n) * 1 <= log (2,(c * ((k * n) to_power x))) by POWER:52;
then k * n <= (log (2,c)) + (log (2,((k * n) to_power x))) by POWER:53, TEZ1, L3;
then k * n <= (log (2,c)) + (x * (log (2,(k * n)))) by POWER:55, LPNN2, ASC3, ASK;
then k * n <= (log (2,c)) + (x * ((log (2,k)) + (log (2,n)))) by POWER:53, ASK, ZZ1;
hence k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n))) ; :: thesis: verum
end;
consider Z being Element of NAT such that
HCL2: for k being Nat st Z <= k holds
4 < k / (log (2,k)) by LMC31HC;
HEXK: ex k being Nat st
( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k )
proof
now :: thesis: ( ( ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < Z & ex k being Element of NAT st
( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < k ) ) or ( Z <= ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) & ex k being Element of NAT st
( ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & Z <= k ) ) )
per cases ( ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < Z or Z <= ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) ) ;
case AC1: ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < Z ; :: thesis: ex k being Element of NAT st
( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < k )
reconsider k = Z + 1 as Element of NAT ;
take k = k; :: thesis: ( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < k )
thus Z <= k by INT_1:6; :: thesis: ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < k
hence ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) < k by AC1, XXREAL_0:2; :: thesis: verum
end;
case AC2: Z <= ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) ; :: thesis: ex k being Element of NAT st
( ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & Z <= k )
reconsider k = [/(((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)))\] + 1 as Integer ;
AC3P: ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= [/(((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)))\] by INT_1:def 7;
then AC3: (((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4))) + 0 <= [/(((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)))\] + 1 by XREAL_1:8;
reconsider k = k as Element of NAT by AC3P, INT_1:3, AC2;
take k = k; :: thesis: ( ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & Z <= k )
thus ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k by AC3; :: thesis: Z <= k
thus Z <= k by AC3, AC2, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ex k being Nat st
( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k ) ; :: thesis: verum
end;
ex k being Nat st
( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & 1 < k )
proof
consider k being Nat such that
HEXK2: ( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k ) by HEXK;
reconsider a = k + 2 as Nat ;
take a ; :: thesis: ( Z <= a & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= a & 1 < a )
CC1: 0 + 2 <= k + 2 by XREAL_1:6;
k <= a by NAT_1:11;
hence ( Z <= a & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= a & 1 < a ) by CC1, XXREAL_0:2, HEXK2; :: thesis: verum
end;
then consider k being Nat such that
HCL3: ( Z <= k & 1 < k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k ) ;
FF0: (((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4))) * (n - (x / 4)) <= k * (n - (x / 4)) by HCL3, ASC3, XREAL_1:64;
HCL4: 4 < k / (log (2,k)) by HCL2, HCL3;
HCL7: k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n))) by HCL1, HCL3;
HCL8: 0 < log (2,k) by ENTROPY1:4, HCL3;
then 4 * (log (2,k)) < (k / (log (2,k))) * (log (2,k)) by HCL4, XREAL_1:68;
then 4 * (log (2,k)) < (k * (log (2,k))) / (log (2,k)) by XCMPLX_1:74;
then 4 * (log (2,k)) < k * ((log (2,k)) / (log (2,k))) by XCMPLX_1:74;
then 4 * (log (2,k)) < k * 1 by XCMPLX_1:60, HCL8;
then ((log (2,k)) * 4) * x < k * x by XREAL_1:68, AS1;
then (((log (2,k)) * x) * 4) / 4 < (k * x) / 4 by XREAL_1:74;
then (k * n) - ((k * x) / 4) < (((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n)))) - (x * (log (2,k))) by HCL7, XREAL_1:15;
hence contradiction by FF0, XCMPLX_1:87, ASC3; :: thesis: verum