let n be Nat; :: thesis: ( n >= 1 implies ex p being Prime st
( n < p & p <= 2 * n ) )
assume A1: n >= 1 ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
AA: n in NAT by ORDINAL1:def 12;

per cases ( n < 4000 or n >= 4000 ) ;

suppose n < 4000 ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )

then n < 4001 by XXREAL_0:2;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A1, AA, Lm7; :: thesis: verum

end;

suppose A2: n >= 4000 ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )

set m = (2 * n) choose n;
set X1 = { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count ((2 * n) choose n) > 0 ) } ;
set X2 = { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } ;
set X3 = { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count ((2 * n) choose n) > 0 ) } ;
assume A3: for p being Prime holds
( not n < p or not p <= 2 * n ) ; :: thesis: contradiction

now :: thesis: not { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count ((2 * n) choose n) > 0 ) } <> {}

assume { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count ((2 * n) choose n) > 0 ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count ((2 * n) choose n) > 0 ) } by XBOOLE_0:def 1;
ex p being prime Element of NAT st
( p |^ (p |-count ((2 * n) choose n)) = x & n < p & p <= 2 * n & p |-count ((2 * n) choose n) > 0 ) by A4;
hence contradiction by A3; :: thesis: verum

end;

then A5: (2 * n) choose n = ((Product (Sgm { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count ((2 * n) choose n) > 0 ) } )) * (Product (Sgm { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } ))) * 1 by AA, A2, Lm10, FINSEQ_3:43, RVSUM_1:94, XXREAL_0:2;
A6: (4 |^ n) / (2 * n) <= (2 * n) choose n by Th6;
set X = { p where p is prime Element of NAT : p <= (2 * n) / 3 } ;
A7: n >= 3 by A2, XXREAL_0:2;
then n / 3 >= 3 / 3 by XREAL_1:72;
then (n / 3) * 2 >= 1 * 2 by XREAL_1:64;
then A8: Product (Sgm { p where p is prime Element of NAT : p <= (2 * n) / 3 } ) <= 4 to_power (((2 * n) / 3) - 1) by Th45;
set mm = [/((2 * n) / 3)\];
reconsider mm = [/((2 * n) / 3)\] as Element of NAT by INT_1:53;
set XX = Seg mm;

A9: now :: thesis: not {} in { p where p is prime Element of NAT : p <= (2 * n) / 3 }

assume {} in { p where p is prime Element of NAT : p <= (2 * n) / 3 } ; :: thesis: contradiction
then ex p being prime Element of NAT st
( p = {} & p <= (2 * n) / 3 ) ;
hence contradiction ; :: thesis: verum

end;

(- 1) + ((2 * n) / 3) < 0 + ((2 * n) / 3) by XREAL_1:6;
then A10: 4 to_power (((2 * n) / 3) - 1) < 4 to_power ((2 * n) / 3) by POWER:39;

now :: thesis: for x being object st x in { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } holds
x in { p where p is prime Element of NAT : p <= (2 * n) / 3 }

let x be object ; :: thesis: ( x in { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } implies x in { p where p is prime Element of NAT : p <= (2 * n) / 3 } )
assume x in { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } ; :: thesis: x in { p where p is prime Element of NAT : p <= (2 * n) / 3 }
then consider p being prime Element of NAT such that
A11: p |^ (p |-count ((2 * n) choose n)) = x and
A12: sqrt (2 * n) < p and
A13: p <= (2 * n) / 3 and
A14: p |-count ((2 * n) choose n) > 0 ;
p |-count ((2 * n) choose n) <= 1 by AA, A7, A12, A13, Lm9;
then p |-count ((2 * n) choose n) < 1 + 1 by NAT_1:13;
then p |-count ((2 * n) choose n) = 1 by A14, NAT_1:23;
then p = x by A11;
hence x in { p where p is prime Element of NAT : p <= (2 * n) / 3 } by A13; :: thesis: verum

end;

then A15: { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } c= { p where p is prime Element of NAT : p <= (2 * n) / 3 } ;

now :: thesis: for x being object st x in { p where p is prime Element of NAT : p <= (2 * n) / 3 } holds
x in Seg mm

let x be object ; :: thesis: ( x in { p where p is prime Element of NAT : p <= (2 * n) / 3 } implies x in Seg mm )
assume x in { p where p is prime Element of NAT : p <= (2 * n) / 3 } ; :: thesis: x in Seg mm
then consider p being prime Element of NAT such that
A16: p = x and
A17: p <= (2 * n) / 3 ;
A18: 1 <= p by INT_2:def 4;
(2 * n) / 3 <= [/((2 * n) / 3)\] by INT_1:def 7;
then p <= [/((2 * n) / 3)\] by A17, XXREAL_0:2;
hence x in Seg mm by A16, A18, FINSEQ_1:1; :: thesis: verum

end;

then A19: { p where p is prime Element of NAT : p <= (2 * n) / 3 } c= Seg mm ;
then { p where p is prime Element of NAT : p <= (2 * n) / 3 } c= NAT by XBOOLE_1:1;
then Product (Sgm { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } ) <= Product (Sgm { p where p is prime Element of NAT : p <= (2 * n) / 3 } ) by A19, A9, A15, Th42;
then A20: Product (Sgm { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) } ) <= 4 to_power (((2 * n) / 3) - 1) by A8, XXREAL_0:2;
n >= 3 by A2, XXREAL_0:2;
then Product (Sgm { (p |^ (p |-count ((2 * n) choose n))) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count ((2 * n) choose n) > 0 ) } ) <= (2 * n) to_power (sqrt (2 * n)) by AA, Lm11;
then (2 * n) choose n <= ((2 * n) to_power (sqrt (2 * n))) * (4 to_power (((2 * n) / 3) - 1)) by A20, A5, XREAL_1:66;
then A21: (4 |^ n) / (2 * n) <= ((2 * n) to_power (sqrt (2 * n))) * (4 to_power (((2 * n) / 3) - 1)) by A6, XXREAL_0:2;
A22: 4 to_power ((2 * n) / 3) > 0 by POWER:34;
(2 * n) to_power (sqrt (2 * n)) > 0 by A2, POWER:34;
then (4 to_power (((2 * n) / 3) - 1)) * ((2 * n) to_power (sqrt (2 * n))) < (4 to_power ((2 * n) / 3)) * ((2 * n) to_power (sqrt (2 * n))) by A10, XREAL_1:68;
then (4 |^ n) / (2 * n) <= ((2 * n) to_power (sqrt (2 * n))) * (4 to_power ((2 * n) / 3)) by A21, XXREAL_0:2;
then ((4 |^ n) / (2 * n)) * (2 * n) <= (((2 * n) to_power (sqrt (2 * n))) * (4 to_power ((2 * n) / 3))) * (2 * n) by XREAL_1:64;
then ( 4 |^ n = 4 to_power ((3 * n) / 3) & 4 |^ n <= (((2 * n) to_power (sqrt (2 * n))) * (2 * n)) * (4 to_power ((2 * n) / 3)) ) by A2, POWER:41, XCMPLX_1:87;
then (4 to_power ((3 * n) / 3)) / (4 to_power ((2 * n) / 3)) <= ((((2 * n) to_power (sqrt (2 * n))) * (2 * n)) * (4 to_power ((2 * n) / 3))) / (4 to_power ((2 * n) / 3)) by A22, XREAL_1:72;
then (4 to_power ((3 * n) / 3)) / (4 to_power ((2 * n) / 3)) <= ((2 * n) to_power (sqrt (2 * n))) * (2 * n) by A22, XCMPLX_1:89;
then 4 to_power (((3 * n) / 3) - ((2 * n) / 3)) <= ((2 * n) to_power (sqrt (2 * n))) * (2 * n) by POWER:29;
then 4 to_power (n / 3) <= ((2 * n) to_power (sqrt (2 * n))) * ((2 * n) to_power 1) by POWER:25;
then 4 to_power (n / 3) <= (2 * n) to_power ((sqrt (2 * n)) + 1) by A2, POWER:27;
then A23: ( 4 to_power (n / 3) < (2 * n) to_power ((sqrt (2 * n)) + 1) or 4 to_power (n / 3) = (2 * n) to_power ((sqrt (2 * n)) + 1) ) by XXREAL_0:1;
4 to_power (n / 3) > 0 by POWER:34;
then (4 to_power (n / 3)) to_power 3 <= ((2 * n) to_power ((sqrt (2 * n)) + 1)) to_power 3 by A23, POWER:37;
then 4 to_power ((n / 3) * 3) <= ((2 * n) to_power ((sqrt (2 * n)) + 1)) to_power 3 by POWER:33;
then A24: 4 to_power n <= (2 * n) to_power (((sqrt (2 * n)) + 1) * 3) by A2, POWER:33;
reconsider 2n = 2 * n as Real ;
A25: (6 -root (2 * n)) to_power 6 = (6 -root 2n) |^ 6 by POWER:41
.= 2n by COMPTRIG:4 ;
2 to_power 2 = 2 |^ 2 by POWER:41
.= Product <*2,2*> by FINSEQ_2:61
.= 2 * 2 by RVSUM_1:99 ;
then A26: ( 2 to_power (2 * n) > 0 & 4 to_power n = 2 to_power (2 * n) ) by POWER:33, POWER:34;
set n1 = [\(6 -root (2 * n))/];
(6 -root (2 * n)) - 1 < [\(6 -root (2 * n))/] by INT_1:def 6;
then A27: ((6 -root (2 * n)) - 1) + 1 < [\(6 -root (2 * n))/] + 1 by XREAL_1:6;
6 -root (2 * n) > 6 -root 0 by A2, POWER:17;
then A28: 6 -root (2 * n) > 0 by POWER:5;
then reconsider n1 = [\(6 -root (2 * n))/] as Element of NAT by INT_1:53;
n1 <= 6 -root (2 * n) by INT_1:def 6;
then ( n1 < 6 -root (2 * n) or n1 = 6 -root (2 * n) ) by XXREAL_0:1;
then A29: 2 to_power n1 <= 2 to_power (6 -root (2 * n)) by POWER:39;
n1 + 1 <= 2 |^ n1 by NEWTON:85;
then n1 + 1 <= 2 to_power n1 by POWER:41;
then n1 + 1 <= 2 to_power (6 -root (2 * n)) by A29, XXREAL_0:2;
then ( n1 + 1 < 2 to_power (6 -root (2 * n)) or n1 + 1 = 2 to_power (6 -root (2 * n)) ) by XXREAL_0:1;
then A30: (n1 + 1) to_power 6 <= (2 to_power (6 -root (2 * n))) to_power 6 by POWER:37;
(6 -root (2 * n)) to_power 6 < (n1 + 1) to_power 6 by A27, A28, POWER:37;
then 2 * n < (2 to_power (6 -root (2 * n))) to_power 6 by A30, A25, XXREAL_0:2;
then A31: 2 * n < 2 to_power ((6 -root (2 * n)) * 6) by POWER:33;
sqrt (2 * n) > 0 by A2, SQUARE_1:25;
then (2 * n) to_power (((sqrt (2 * n)) + 1) * 3) < (2 to_power ((6 -root (2 * n)) * 6)) to_power (((sqrt (2 * n)) + 1) * 3) by A2, A31, POWER:37;
then 4 to_power n < (2 to_power ((6 -root (2 * n)) * 6)) to_power (((sqrt (2 * n)) + 1) * 3) by A24, XXREAL_0:2;
then 4 to_power n < 2 to_power (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) by POWER:33;
then log (2,(2 to_power (2 * n))) < log (2,(2 to_power (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)))) by A26, POWER:57;
then (2 * n) * (log (2,2)) < log (2,(2 to_power (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)))) by POWER:55;
then (2 * n) * (log (2,2)) < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * (log (2,2)) by POWER:55;
then (2 * n) * 1 < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * (log (2,2)) by POWER:52;
then A32: 2 * n < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * 1 by POWER:52;
42 < n by A2, XXREAL_0:2;
then 42 * 2 < n * 2 by XREAL_1:68;
then 81 < 2 * n by XXREAL_0:2;
then A33: sqrt 81 < sqrt (2 * n) by SQUARE_1:27;
81 = 9 ^2 ;
then sqrt 81 = 9 by SQUARE_1:22;
then 9 * 2 < (sqrt (2 * n)) * 2 by A33, XREAL_1:68;
then 18 + (18 * (sqrt (2 * n))) < (2 * (sqrt (2 * n))) + (18 * (sqrt (2 * n))) by XREAL_1:6;
then (18 + (18 * (sqrt (2 * n)))) * (6 -root (2 * n)) < (20 * (sqrt (2 * n))) * (6 -root (2 * n)) by A28, XREAL_1:68;
then 2 * n < 20 * ((sqrt (2 * n)) * (6 -root (2 * n))) by A32, XXREAL_0:2;
then 2 * n < 20 * ((2 -Root (2 * n)) * (6 -root (2 * n))) by PREPOWER:32;
then 2 * n < 20 * ((2 -root (2 * n)) * (6 -root (2 * n))) by POWER:def 1;
then 2 * n < 20 * (((2 * n) to_power (1 / 2)) * (6 -root (2 * n))) by POWER:45;
then 2 * n < 20 * (((2 * n) to_power (1 / 2)) * ((2 * n) to_power (1 / 6))) by POWER:45;
then A34: 2 * n < 20 * ((2 * n) to_power ((1 / 2) + (1 / 6))) by A2, POWER:27;
A35: (2 * n) to_power (2 / 3) <> 0 by A2, POWER:34;
(2 * n) to_power (2 / 3) > 0 by A2, POWER:34;
then (2 * n) / ((2 * n) to_power (2 / 3)) < (20 * ((2 * n) to_power (2 / 3))) / ((2 * n) to_power (2 / 3)) by A34, XREAL_1:74;
then (2 * n) / ((2 * n) to_power (2 / 3)) < 20 by A35, XCMPLX_1:89;
then ((2 * n) to_power 1) / ((2 * n) to_power (2 / 3)) < 20 by POWER:25;
then A36: (2 * n) to_power (1 - (2 / 3)) < 20 by A2, POWER:29;
(2 * n) to_power (1 / 3) > 0 by A2, POWER:34;
then ((2 * n) to_power (1 / 3)) to_power 3 < 20 to_power 3 by A36, POWER:37;
then (2 * n) to_power ((1 / 3) * 3) < 20 to_power 3 by A2, POWER:33;
then 2 * n < 20 to_power (2 + 1) by POWER:25;
then 2 * n < (20 to_power 2) * (20 to_power 1) by POWER:27;
then 2 * n < (20 to_power (1 + 1)) * 20 by POWER:25;
then 2 * n < ((20 to_power 1) * (20 to_power 1)) * 20 by POWER:27;
then 2 * n < ((20 to_power 1) * 20) * 20 by POWER:25;
then 2 * n < (20 * 20) * 20 by POWER:25;
then (2 * n) / 2 < 8000 / 2 by XREAL_1:74;
hence contradiction by A2; :: thesis: verum

end;

end;