let x be Nat; ( 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
; 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)
; 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
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) )
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
ASC22:
for k being Nat st 1 <= k holds
2 to_power (k * n) <= c * ((k * n) to_power x)
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;
( 1 <= k implies k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n))) )
assume ASK:
1
<= k
;
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)))
;
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 ( ( ((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 AC2:
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 )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;
( ((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;
Z <= kthus
Z <= k
by AC3, AC2, XXREAL_0:2;
verum end; end; end;
hence
ex
k being
Nat st
(
Z <= k &
((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k )
;
verum
end;
ex k being Nat st
( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & 1 < k )
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; verum