Metamath Proof Explorer

Theorem bpos

Description: Bertrand's postulate: there is a prime between N and 2 N for every positive integer N . This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Assertion bpos 
|- ( N e. NN -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )

Proof

Step Hyp Ref Expression
1 bpos1 
 |-  ( ( N e. NN /\ N <_ ; 6 4 ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
2 eqid 
 |-  ( n e. NN |-> ( ( ( ( sqrt ` 2 ) x. ( ( x e. RR+ |-> ( ( log ` x ) / x ) ) ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( ( x e. RR+ |-> ( ( log ` x ) / x ) ) ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) ) = ( n e. NN |-> ( ( ( ( sqrt ` 2 ) x. ( ( x e. RR+ |-> ( ( log ` x ) / x ) ) ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( ( x e. RR+ |-> ( ( log ` x ) / x ) ) ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) )
3 eqid 
 |-  ( x e. RR+ |-> ( ( log ` x ) / x ) ) = ( x e. RR+ |-> ( ( log ` x ) / x ) )
4 simpll 
 |-  ( ( ( N e. NN /\ ; 6 4 < N ) /\ -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) -> N e. NN )
5 simplr 
 |-  ( ( ( N e. NN /\ ; 6 4 < N ) /\ -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) -> ; 6 4 < N )
6 simpr 
 |-  ( ( ( N e. NN /\ ; 6 4 < N ) /\ -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
7 2 3 4 5 6 bposlem9 
 |-  ( ( ( N e. NN /\ ; 6 4 < N ) /\ -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
8 7 pm2.18da 
 |-  ( ( N e. NN /\ ; 6 4 < N ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
9 nnre 
 |-  ( N e. NN -> N e. RR )
10 6nn0 
 |-  6 e. NN0
11 4nn0 
 |-  4 e. NN0
12 10 11 deccl 
 |-  ; 6 4 e. NN0
13 12 nn0rei 
 |-  ; 6 4 e. RR
14 lelttric 
 |-  ( ( N e. RR /\ ; 6 4 e. RR ) -> ( N <_ ; 6 4 \/ ; 6 4 < N ) )
15 9 13 14 sylancl 
 |-  ( N e. NN -> ( N <_ ; 6 4 \/ ; 6 4 < N ) )
16 1 8 15 mpjaodan 
 |-  ( N e. NN -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )