Metamath Proof Explorer

Theorem prmunb

Description: The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012)

Ref Expression
Assertion prmunb 
|- ( N e. NN -> E. p e. Prime N < p )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
2 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
3 elnnuz 
 |-  ( ( ! ` N ) e. NN <-> ( ! ` N ) e. ( ZZ>= ` 1 ) )
4 eluzp1p1 
 |-  ( ( ! ` N ) e. ( ZZ>= ` 1 ) -> ( ( ! ` N ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
5 df-2 
 |-  2 = ( 1 + 1 )
6 5 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
7 4 6 eleqtrrdi 
 |-  ( ( ! ` N ) e. ( ZZ>= ` 1 ) -> ( ( ! ` N ) + 1 ) e. ( ZZ>= ` 2 ) )
8 3 7 sylbi 
 |-  ( ( ! ` N ) e. NN -> ( ( ! ` N ) + 1 ) e. ( ZZ>= ` 2 ) )
9 exprmfct 
 |-  ( ( ( ! ` N ) + 1 ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( ( ! ` N ) + 1 ) )
10 2 8 9 3syl 
 |-  ( N e. NN0 -> E. p e. Prime p || ( ( ! ` N ) + 1 ) )
11 prmz 
 |-  ( p e. Prime -> p e. ZZ )
12 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
13 eluz 
 |-  ( ( p e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` p ) <-> p <_ N ) )
14 11 12 13 syl2an 
 |-  ( ( p e. Prime /\ N e. NN0 ) -> ( N e. ( ZZ>= ` p ) <-> p <_ N ) )
15 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
16 eluz2b2 
 |-  ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
17 15 16 sylib 
 |-  ( p e. Prime -> ( p e. NN /\ 1 < p ) )
18 17 adantr 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> ( p e. NN /\ 1 < p ) )
19 18 simpld 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> p e. NN )
20 19 nnnn0d 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> p e. NN0 )
21 eluznn0 
 |-  ( ( p e. NN0 /\ N e. ( ZZ>= ` p ) ) -> N e. NN0 )
22 20 21 sylancom 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> N e. NN0 )
23 nnz 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. ZZ )
24 22 2 23 3syl 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> ( ! ` N ) e. ZZ )
25 18 simprd 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> 1 < p )
26 dvdsfac 
 |-  ( ( p e. NN /\ N e. ( ZZ>= ` p ) ) -> p || ( ! ` N ) )
27 19 26 sylancom 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> p || ( ! ` N ) )
28 ndvdsp1 
 |-  ( ( ( ! ` N ) e. ZZ /\ p e. NN /\ 1 < p ) -> ( p || ( ! ` N ) -> -. p || ( ( ! ` N ) + 1 ) ) )
29 28 imp 
 |-  ( ( ( ( ! ` N ) e. ZZ /\ p e. NN /\ 1 < p ) /\ p || ( ! ` N ) ) -> -. p || ( ( ! ` N ) + 1 ) )
30 24 19 25 27 29 syl31anc 
 |-  ( ( p e. Prime /\ N e. ( ZZ>= ` p ) ) -> -. p || ( ( ! ` N ) + 1 ) )
31 30 ex 
 |-  ( p e. Prime -> ( N e. ( ZZ>= ` p ) -> -. p || ( ( ! ` N ) + 1 ) ) )
32 31 adantr 
 |-  ( ( p e. Prime /\ N e. NN0 ) -> ( N e. ( ZZ>= ` p ) -> -. p || ( ( ! ` N ) + 1 ) ) )
33 14 32 sylbird 
 |-  ( ( p e. Prime /\ N e. NN0 ) -> ( p <_ N -> -. p || ( ( ! ` N ) + 1 ) ) )
34 33 con2d 
 |-  ( ( p e. Prime /\ N e. NN0 ) -> ( p || ( ( ! ` N ) + 1 ) -> -. p <_ N ) )
35 34 ancoms 
 |-  ( ( N e. NN0 /\ p e. Prime ) -> ( p || ( ( ! ` N ) + 1 ) -> -. p <_ N ) )
36 nn0re 
 |-  ( N e. NN0 -> N e. RR )
37 11 zred 
 |-  ( p e. Prime -> p e. RR )
38 ltnle 
 |-  ( ( N e. RR /\ p e. RR ) -> ( N < p <-> -. p <_ N ) )
39 36 37 38 syl2an 
 |-  ( ( N e. NN0 /\ p e. Prime ) -> ( N < p <-> -. p <_ N ) )
40 35 39 sylibrd 
 |-  ( ( N e. NN0 /\ p e. Prime ) -> ( p || ( ( ! ` N ) + 1 ) -> N < p ) )
41 40 reximdva 
 |-  ( N e. NN0 -> ( E. p e. Prime p || ( ( ! ` N ) + 1 ) -> E. p e. Prime N < p ) )
42 10 41 mpd 
 |-  ( N e. NN0 -> E. p e. Prime N < p )
43 1 42 syl 
 |-  ( N e. NN -> E. p e. Prime N < p )