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

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) )

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

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

k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n)))

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 )

( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & 1 < k )

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

( 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

then LPNN2:
0 < N
;
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 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

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

( N <= n & 0 < n - (x / 4) ) ; :: thesis: verum

end;

then consider n being Element of NAT such that 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 ) ) )end;

hence
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 )
;

end;

case AC1:
x / 4 < N
; :: thesis: ex n being Element of NAT st

( N <= n & 0 < n - (x / 4) )

( 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;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

case AC2:
N <= x / 4
; :: thesis: ex n being Element of NAT st

( 0 < n - (x / 4) & N <= n )

( 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;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

( N <= n & 0 < n - (x / 4) ) ; :: thesis: verum

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

ASC22:
for k being Nat st 1 <= k holds
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;then 2 to_power n <= 0 * (n to_power x) by XC1;

hence contradiction by POWER:34; :: thesis: verum

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

proof

HCL1:
for k being Nat st 1 <= k holds
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;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

k * n <= ((log (2,c)) + (x * (log (2,k)))) + (x * (log (2,n)))

proof

consider Z being Element of NAT such that
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;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

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

( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k ) ; :: thesis: verum

end;

ex k being Nat st 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 ) ) )end;

hence
ex k being 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)) )
;

end;

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 )

( 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;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

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 )

( ((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;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

( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k ) ; :: thesis: verum

( Z <= k & ((log (2,c)) + (x * (log (2,n)))) / (n - (x / 4)) <= k & 1 < k )

proof

then consider k being Nat such that
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;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

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