Theorem prmunb

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

	Ref	Expression
Assertion	prmunb	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝑁 < 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
2		faccl	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
3		elnnuz	⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ ↔ ( ! ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
4		eluzp1p1	⊢ ( ( ! ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ! ‘ 𝑁 ) + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
5		df-2	⊢ 2 = ( 1 + 1 )
6	5	fveq2i	⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
7	4 6	eleqtrrdi	⊢ ( ( ! ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ! ‘ 𝑁 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
8	3 7	sylbi	⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ( ! ‘ 𝑁 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
9		exprmfct	⊢ ( ( ( ! ‘ 𝑁 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) )
10	2 8 9	3syl	⊢ ( 𝑁 ∈ ℕ0 → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) )
11		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
12		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
13		eluz	⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ↔ 𝑝 ≤ 𝑁 ) )
14	11 12 13	syl2an	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ↔ 𝑝 ≤ 𝑁 ) )
15		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
16		eluz2b2	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
17	15 16	sylib	⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
18	17	adantr	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
19	18	simpld	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑝 ∈ ℕ )
20	19	nnnn0d	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑝 ∈ ℕ0 )
21		eluznn0	⊢ ( ( 𝑝 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑁 ∈ ℕ0 )
22	20 21	sylancom	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑁 ∈ ℕ0 )
23		nnz	⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℤ )
24	22 2 23	3syl	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → ( ! ‘ 𝑁 ) ∈ ℤ )
25	18	simprd	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 1 < 𝑝 )
26		dvdsfac	⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑝 ∥ ( ! ‘ 𝑁 ) )
27	19 26	sylancom	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑝 ∥ ( ! ‘ 𝑁 ) )
28		ndvdsp1	⊢ ( ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) → ( 𝑝 ∥ ( ! ‘ 𝑁 ) → ¬ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) ) )
29	28	imp	⊢ ( ( ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) ∧ 𝑝 ∥ ( ! ‘ 𝑁 ) ) → ¬ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) )
30	24 19 25 27 29	syl31anc	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) ) → ¬ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) )
31	30	ex	⊢ ( 𝑝 ∈ ℙ → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) → ¬ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) ) )
32	31	adantr	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑝 ) → ¬ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) ) )
33	14 32	sylbird	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑝 ≤ 𝑁 → ¬ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) ) )
34	33	con2d	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) → ¬ 𝑝 ≤ 𝑁 ) )
35	34	ancoms	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) → ¬ 𝑝 ≤ 𝑁 ) )
36		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
37	11	zred	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
38		ltnle	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( 𝑁 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑁 ) )
39	36 37 38	syl2an	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑝 ∈ ℙ ) → ( 𝑁 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑁 ) )
40	35 39	sylibrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) → 𝑁 < 𝑝 ) )
41	40	reximdva	⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ! ‘ 𝑁 ) + 1 ) → ∃ 𝑝 ∈ ℙ 𝑁 < 𝑝 ) )
42	10 41	mpd	⊢ ( 𝑁 ∈ ℕ0 → ∃ 𝑝 ∈ ℙ 𝑁 < 𝑝 )
43	1 42	syl	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝑁 < 𝑝 )