let n be Element of 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 )

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

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 set 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 A2, Lm10, FINSEQ_3:49, RVSUM_1:124, 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:74;
then (n / 3) * 2 >= 1 * 2 by XREAL_1:66;
then A8: Product (Sgm { p where p is prime Element of NAT : p <= (2 * n) / 3 } ) <= 4 to_power (((2 * n) / 3) - 1) by Th46;
set mm = [/((2 * n) / 3)\];
reconsider mm = [/((2 * n) / 3)\] as Element of NAT by INT_1:80;
set XX = Seg mm;

A9: now

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:8;
then A10: 4 to_power (((2 * n) / 3) - 1) < 4 to_power ((2 * n) / 3) by POWER:44;

now

let x be set ; :: 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 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, NEWTON:10;
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 } by TARSKI:def 3;

now

let x be set ; :: 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 5;
(2 * n) / 3 <= [/((2 * n) / 3)\] by INT_1:def 5;
then p <= [/((2 * n) / 3)\] by A17, XXREAL_0:2;
hence x in Seg mm by A16, A18, FINSEQ_1:3; :: thesis: verum

end;

then A19: { p where p is prime Element of NAT : p <= (2 * n) / 3 } c= Seg mm by TARSKI:def 3;
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, Th43;
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 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:68;
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:39;
(2 * n) to_power (sqrt (2 * n)) > 0 by A2, POWER:39;
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:70;
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:66;
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:46, XCMPLX_1:88;
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:74;
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:90;
then 4 to_power (((3 * n) / 3) - ((2 * n) / 3)) <= ((2 * n) to_power (sqrt (2 * n))) * (2 * n) by POWER:34;
then 4 to_power (n / 3) <= ((2 * n) to_power (sqrt (2 * n))) * ((2 * n) to_power 1) by POWER:30;
then 4 to_power (n / 3) <= (2 * n) to_power ((sqrt (2 * n)) + 1) by A2, POWER:32;
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:39;
then (4 to_power (n / 3)) to_power 3 <= ((2 * n) to_power ((sqrt (2 * n)) + 1)) to_power 3 by A23, POWER:42;
then 4 to_power ((n / 3) * 3) <= ((2 * n) to_power ((sqrt (2 * n)) + 1)) to_power 3 by POWER:38;
then A24: 4 to_power n <= (2 * n) to_power (((sqrt (2 * n)) + 1) * 3) by A2, POWER:38;
reconsider 2n = 2 * n as real number ;
A25: (6 -root (2 * n)) to_power 6 = (6 -root 2n) |^ 6 by POWER:46
.= 2n by COMPTRIG:17 ;
2 to_power 2 = 2 |^ 2 by POWER:46
.= Product <*2,2*> by FINSEQ_2:75
.= 2 * 2 by RVSUM_1:129 ;
then A26: ( 2 to_power (2 * n) > 0 & 4 to_power n = 2 to_power (2 * n) ) by POWER:38, POWER:39;
set n1 = [\(6 -root (2 * n))/];
(6 -root (2 * n)) - 1 < [\(6 -root (2 * n))/] by INT_1:def 4;
then A27: ((6 -root (2 * n)) - 1) + 1 < [\(6 -root (2 * n))/] + 1 by XREAL_1:8;
6 -root (2 * n) > 6 -root 0 by A2, POWER:18;
then A28: 6 -root (2 * n) > 0 by POWER:6;
then reconsider n1 = [\(6 -root (2 * n))/] as Element of NAT by INT_1:80;
n1 <= 6 -root (2 * n) by INT_1:def 4;
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:44;
n1 + 1 <= 2 |^ n1 by NEWTON:104;
then n1 + 1 <= 2 to_power n1 by POWER:46;
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:42;
(6 -root (2 * n)) to_power 6 < (n1 + 1) to_power 6 by A27, A28, POWER:42;
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:38;
sqrt (2 * n) > 0 by A2, SQUARE_1:93;
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:42;
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:38;
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:65;
then (2 * n) * (log 2,2) < log 2,(2 to_power (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3))) by POWER:63;
then (2 * n) * (log 2,2) < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * (log 2,2) by POWER:63;
then (2 * n) * 1 < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * (log 2,2) by POWER:60;
then A32: 2 * n < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * 1 by POWER:60;
42 < n by A2, XXREAL_0:2;
then 42 * 2 < n * 2 by XREAL_1:70;
then 81 < 2 * n by XXREAL_0:2;
then A33: sqrt 81 < sqrt (2 * n) by SQUARE_1:95;
81 = 9 ^2 ;
then sqrt 81 = 9 by SQUARE_1:89;
then 9 * 2 < (sqrt (2 * n)) * 2 by A33, XREAL_1:70;
then 18 + (18 * (sqrt (2 * n))) < (2 * (sqrt (2 * n))) + (18 * (sqrt (2 * n))) by XREAL_1:8;
then (18 + (18 * (sqrt (2 * n)))) * (6 -root (2 * n)) < (20 * (sqrt (2 * n))) * (6 -root (2 * n)) by A28, XREAL_1:70;
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:41;
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:52;
then 2 * n < 20 * (((2 * n) to_power (1 / 2)) * ((2 * n) to_power (1 / 6))) by POWER:52;
then A34: 2 * n < 20 * ((2 * n) to_power ((1 / 2) + (1 / 6))) by A2, POWER:32;
A35: (2 * n) to_power (2 / 3) <> 0 by A2, POWER:39;
(2 * n) to_power (2 / 3) > 0 by A2, POWER:39;
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:76;
then (2 * n) / ((2 * n) to_power (2 / 3)) < 20 by A35, XCMPLX_1:90;
then ((2 * n) to_power 1) / ((2 * n) to_power (2 / 3)) < 20 by POWER:30;
then A36: (2 * n) to_power (1 - (2 / 3)) < 20 by A2, POWER:34;
(2 * n) to_power (1 / 3) > 0 by A2, POWER:39;
then ((2 * n) to_power (1 / 3)) to_power 3 < 20 to_power 3 by A36, POWER:42;
then (2 * n) to_power ((1 / 3) * 3) < 20 to_power 3 by A2, POWER:38;
then 2 * n < 20 to_power (2 + 1) by POWER:30;
then 2 * n < (20 to_power 2) * (20 to_power 1) by POWER:32;
then 2 * n < (20 to_power (1 + 1)) * 20 by POWER:30;
then 2 * n < ((20 to_power 1) * (20 to_power 1)) * 20 by POWER:32;
then 2 * n < ((20 to_power 1) * 20) * 20 by POWER:30;
then 2 * n < (20 * 20) * 20 by POWER:30;
then (2 * n) / 2 < 8000 / 2 by XREAL_1:76;
hence contradiction by A2; :: thesis: verum

end;

end;