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 )

assume A3: for p being Prime holds
( not n < p or not p <= 2 * n ) ; :: thesis: contradiction
set m = (2 * n) choose n;
A4: n >= 3 by A2, XXREAL_0:2;
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 ) } ;
n >= 3 by A2, XXREAL_0:2;
then A6: 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;
set X = { p where p is prime Element of NAT : p <= (2 * n) / 3 } ;
set mm = [/((2 * n) / 3)\];
reconsider mm = [/((2 * n) / 3)\] as Element of NAT by INT_1:80;
set XX = Seg mm;

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
A7: ( p = x & p <= (2 * n) / 3 ) ;
(2 * n) / 3 <= [/((2 * n) / 3)\] by INT_1:def 5;
then A8: p <= [/((2 * n) / 3)\] by A7, XXREAL_0:2;
1 <= p by INT_2:def 5;
hence x in Seg mm by A7, A8, FINSEQ_1:3; :: thesis: verum

end;

then { p where p is prime Element of NAT : p <= (2 * n) / 3 } c= Seg mm by TARSKI:def 3;
then A9: ( { p where p is prime Element of NAT : p <= (2 * n) / 3 } c= NAT & { p where p is prime Element of NAT : p <= (2 * n) / 3 } is finite ) by XBOOLE_1:1;

A10: 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;

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 & sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count ((2 * n) choose n) > 0 ) ;
p |-count ((2 * n) choose n) <= 1 by A4, A11, Lm9;
then p |-count ((2 * n) choose n) < 1 + 1 by NAT_1:13;
then p |-count ((2 * n) choose n) = 1 by A11, 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 A11; :: thesis: verum

end;

then { (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;
then A12: 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 A9, A10, Th43;
n / 3 >= 3 / 3 by A4, XREAL_1:74;
then (n / 3) * 2 >= 1 * 2 by XREAL_1:66;
then Product (Sgm { p where p is prime Element of NAT : p <= (2 * n) / 3 } ) <= 4 to_power (((2 * n) / 3) - 1) by Th46;
then A13: 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 A12, XXREAL_0:2;

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
A14: 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 A14;
hence contradiction by A3; :: thesis: verum

end;

then A15: (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;
A16: (2 * n) choose n <= ((2 * n) to_power (sqrt (2 * n))) * (4 to_power (((2 * n) / 3) - 1)) by A6, A13, A15, XREAL_1:68;
(4 |^ n) / (2 * n) <= (2 * n) choose n by Th6;
then A17: (4 |^ n) / (2 * n) <= ((2 * n) to_power (sqrt (2 * n))) * (4 to_power (((2 * n) / 3) - 1)) by A16, XXREAL_0:2;
A18: (2 * n) to_power (sqrt (2 * n)) > 0 by A2, POWER:39;
A19: 4 |^ n = 4 to_power ((3 * n) / 3) by POWER:46;
A20: 4 to_power ((2 * n) / 3) > 0 by POWER:39;
A21: 4 to_power (n / 3) > 0 by POWER:39;
(- 1) + ((2 * n) / 3) < 0 + ((2 * n) / 3) by XREAL_1:8;
then 4 to_power (((2 * n) / 3) - 1) < 4 to_power ((2 * n) / 3) by POWER:44;
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 A18, XREAL_1:70;
then (4 |^ n) / (2 * n) <= ((2 * n) to_power (sqrt (2 * n))) * (4 to_power ((2 * n) / 3)) by A17, 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 <= (((2 * n) to_power (sqrt (2 * n))) * (2 * n)) * (4 to_power ((2 * n) / 3)) by A2, 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 A19, A20, 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 A20, 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 ( 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;
then (4 to_power (n / 3)) to_power 3 <= ((2 * n) to_power ((sqrt (2 * n)) + 1)) to_power 3 by A21, POWER:42;
then 4 to_power ((n / 3) * 3) <= ((2 * n) to_power ((sqrt (2 * n)) + 1)) to_power 3 by POWER:38;
then A22: 4 to_power n <= (2 * n) to_power (((sqrt (2 * n)) + 1) * 3) by A2, POWER:38;
set n1 = [\(6 -root (2 * n))/];
(6 -root (2 * n)) - 1 < [\(6 -root (2 * n))/] by INT_1:def 4;
then A23: ((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 A24: 6 -root (2 * n) > 0 by POWER:6;
then reconsider n1 = [\(6 -root (2 * n))/] as Element of NAT by INT_1:80;
n1 + 1 <= 2 |^ n1 by NEWTON:104;
then A25: n1 + 1 <= 2 to_power n1 by POWER:46;
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 2 to_power n1 <= 2 to_power (6 -root (2 * n)) by POWER:44;
then n1 + 1 <= 2 to_power (6 -root (2 * n)) by A25, 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 A26: (n1 + 1) to_power 6 <= (2 to_power (6 -root (2 * n))) to_power 6 by POWER:42;
sqrt (2 * n) > 0 by A2, SQUARE_1:93;
then A27: ((sqrt (2 * n)) + 1) * 3 > 0 * 3 ;
reconsider 2n = 2 * n as real number ;
A28: (6 -root (2 * n)) to_power 6 = (6 -root 2n) |^ 6 by POWER:46
.= 2n by COMPTRIG:17 ;
(6 -root (2 * n)) to_power 6 < (n1 + 1) to_power 6 by A23, A24, POWER:42;
then 2 * n < (2 to_power (6 -root (2 * n))) to_power 6 by A26, A28, XXREAL_0:2;
then 2 * n < 2 to_power ((6 -root (2 * n)) * 6) by POWER:38;
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, A27, POWER:42;
then 4 to_power n < (2 to_power ((6 -root (2 * n)) * 6)) to_power (((sqrt (2 * n)) + 1) * 3) by A22, XXREAL_0:2;
then A29: 4 to_power n < 2 to_power (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) by POWER:38;
81 = 9 ^2 ;
then A30: sqrt 81 = 9 by SQUARE_1:89;
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 sqrt 81 < sqrt (2 * n) by SQUARE_1:95;
then 9 * 2 < (sqrt (2 * n)) * 2 by A30, XREAL_1:70;
then 18 + (18 * (sqrt (2 * n))) < (2 * (sqrt (2 * n))) + (18 * (sqrt (2 * n))) by XREAL_1:8;
then A31: (18 + (18 * (sqrt (2 * n)))) * (6 -root (2 * n)) < (20 * (sqrt (2 * n))) * (6 -root (2 * n)) by A24, XREAL_1:70;
A32: 2 to_power (2 * n) > 0 by POWER:39;
A33: (2 * n) to_power (2 / 3) > 0 by A2, POWER:39;
A34: (2 * n) to_power (2 / 3) <> 0 by A2, POWER:39;
A35: (2 * n) to_power (1 / 3) > 0 by A2, POWER:39;
2 to_power 2 = 2 |^ 2 by POWER:46
.= Product <*2,2*> by FINSEQ_2:75
.= 2 * 2 by RVSUM_1:129 ;
then 4 to_power n = 2 to_power (2 * n) 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 A29, A32, 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 2 * n < (((6 -root (2 * n)) * 6) * (((sqrt (2 * n)) + 1) * 3)) * 1 by POWER:60;
then 2 * n < 20 * ((sqrt (2 * n)) * (6 -root (2 * n))) by A31, 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 2 * n < 20 * ((2 * n) to_power ((1 / 2) + (1 / 6))) by A2, POWER:32;
then (2 * n) / ((2 * n) to_power (2 / 3)) < (20 * ((2 * n) to_power (2 / 3))) / ((2 * n) to_power (2 / 3)) by A33, XREAL_1:76;
then (2 * n) / ((2 * n) to_power (2 / 3)) < 20 by A34, XCMPLX_1:90;
then ((2 * n) to_power 1) / ((2 * n) to_power (2 / 3)) < 20 by POWER:30;
then (2 * n) to_power (1 - (2 / 3)) < 20 by A2, POWER:34;
then ((2 * n) to_power (1 / 3)) to_power 3 < 20 to_power 3 by A35, 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;