let n be Element of NAT ; ( n >= 1 implies ex p being Prime st
( n < p & p <= 2 * n ) )
assume A1:
n >= 1
; ex p being Prime st
( n < p & p <= 2 * n )
per cases
( n < 4000 or n >= 4000 )
;
suppose A2:
n >= 4000
;
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 )
;
contradictionthen 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: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;
(- 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;
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 }
;
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 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;
verum end; end;