prmunb

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

		Ref	Expression
	Assertion	prmunb	$⊢ N \in ℕ \to \exists p \in ℙ N < p$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
2		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
3		elnnuz	$⊢ N! \in ℕ \leftrightarrow N! \in ℤ_{\geq 1}$
4		eluzp1p1	$⊢ N! \in ℤ_{\geq 1} \to N! + 1 \in ℤ_{\geq (1 + 1)}$
5		df-2	$⊢ 2 = 1 + 1$
6	5	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
7	4 6	eleqtrrdi	$⊢ N! \in ℤ_{\geq 1} \to N! + 1 \in ℤ_{\geq 2}$
8	3 7	sylbi	$⊢ N! \in ℕ \to N! + 1 \in ℤ_{\geq 2}$
9		exprmfct	$⊢ N! + 1 \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (N! + 1)$
10	2 8 9	3syl	$⊢ N \in ℕ_{0} \to \exists p \in ℙ p ∥ (N! + 1)$
11		prmz	$⊢ p \in ℙ \to p \in ℤ$
12		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
13		eluz	$⊢ (p \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq p} \leftrightarrow p \leq N)$
14	11 12 13	syl2an	$⊢ (p \in ℙ \land N \in ℕ_{0}) \to (N \in ℤ_{\geq p} \leftrightarrow p \leq N)$
15		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
16		eluz2b2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (p \in ℕ \land 1 < p)$
17	15 16	sylib	$⊢ p \in ℙ \to (p \in ℕ \land 1 < p)$
18	17	adantr	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to (p \in ℕ \land 1 < p)$
19	18	simpld	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to p \in ℕ$
20	19	nnnn0d	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to p \in ℕ_{0}$
21		eluznn0	$⊢ (p \in ℕ_{0} \land N \in ℤ_{\geq p}) \to N \in ℕ_{0}$
22	20 21	sylancom	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to N \in ℕ_{0}$
23		nnz	$⊢ N! \in ℕ \to N! \in ℤ$
24	22 2 23	3syl	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to N! \in ℤ$
25	18	simprd	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to 1 < p$
26		dvdsfac	$⊢ (p \in ℕ \land N \in ℤ_{\geq p}) \to p ∥ N!$
27	19 26	sylancom	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to p ∥ N!$
28		ndvdsp1	$⊢ (N! \in ℤ \land p \in ℕ \land 1 < p) \to (p ∥ N! \to \neg p ∥ (N! + 1))$
29	28	imp	$⊢ ((N! \in ℤ \land p \in ℕ \land 1 < p) \land p ∥ N!) \to \neg p ∥ (N! + 1)$
30	24 19 25 27 29	syl31anc	$⊢ (p \in ℙ \land N \in ℤ_{\geq p}) \to \neg p ∥ (N! + 1)$
31	30	ex	$⊢ p \in ℙ \to (N \in ℤ_{\geq p} \to \neg p ∥ (N! + 1))$
32	31	adantr	$⊢ (p \in ℙ \land N \in ℕ_{0}) \to (N \in ℤ_{\geq p} \to \neg p ∥ (N! + 1))$
33	14 32	sylbird	$⊢ (p \in ℙ \land N \in ℕ_{0}) \to (p \leq N \to \neg p ∥ (N! + 1))$
34	33	con2d	$⊢ (p \in ℙ \land N \in ℕ_{0}) \to (p ∥ (N! + 1) \to \neg p \leq N)$
35	34	ancoms	$⊢ (N \in ℕ_{0} \land p \in ℙ) \to (p ∥ (N! + 1) \to \neg p \leq N)$
36		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
37	11	zred	$⊢ p \in ℙ \to p \in ℝ$
38		ltnle	$⊢ (N \in ℝ \land p \in ℝ) \to (N < p \leftrightarrow \neg p \leq N)$
39	36 37 38	syl2an	$⊢ (N \in ℕ_{0} \land p \in ℙ) \to (N < p \leftrightarrow \neg p \leq N)$
40	35 39	sylibrd	$⊢ (N \in ℕ_{0} \land p \in ℙ) \to (p ∥ (N! + 1) \to N < p)$
41	40	reximdva	$⊢ N \in ℕ_{0} \to (\exists p \in ℙ p ∥ (N! + 1) \to \exists p \in ℙ N < p)$
42	10 41	mpd	$⊢ N \in ℕ_{0} \to \exists p \in ℙ N < p$
43	1 42	syl	$⊢ N \in ℕ \to \exists p \in ℙ N < p$

Metamath Proof Explorer

Theorem prmunb

Proof