prmgaplem5

Description: Lemma for prmgap : for each integer greater than 2 there is a smaller prime closest to this integer, i.e. there is a smaller prime and no other prime is between this prime and the integer. (Contributed by AV, 9-Aug-2020)

		Ref	Expression
	Assertion	prmgaplem5	$⊢ N \in ℤ_{\geq 3} \to \exists p \in ℙ (p < N \land \forall z \in (p + 1 ..^N) z \notin ℙ)$

Proof

Step	Hyp	Ref	Expression
1		elrabi	$⊢ r \in \{q \in ℙ \| q < N\} \to r \in ℙ$
2	1	ad2antlr	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land \forall z \in \{q \in ℙ \| q < N\} z \leq r) \to r \in ℙ$
3		breq1	$⊢ p = r \to (p < N \leftrightarrow r < N)$
4		oveq1	$⊢ p = r \to p + 1 = r + 1$
5	4	oveq1d	$⊢ p = r \to (p + 1 ..^N) = (r + 1 ..^N)$
6	5	raleqdv	$⊢ p = r \to (\forall z \in (p + 1 ..^N) z \notin ℙ \leftrightarrow \forall z \in (r + 1 ..^N) z \notin ℙ)$
7	3 6	anbi12d	$⊢ p = r \to ((p < N \land \forall z \in (p + 1 ..^N) z \notin ℙ) \leftrightarrow (r < N \land \forall z \in (r + 1 ..^N) z \notin ℙ))$
8	7	adantl	$⊢ (((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land \forall z \in \{q \in ℙ \| q < N\} z \leq r) \land p = r) \to ((p < N \land \forall z \in (p + 1 ..^N) z \notin ℙ) \leftrightarrow (r < N \land \forall z \in (r + 1 ..^N) z \notin ℙ))$
9		breq1	$⊢ q = r \to (q < N \leftrightarrow r < N)$
10	9	elrab	$⊢ r \in \{q \in ℙ \| q < N\} \leftrightarrow (r \in ℙ \land r < N)$
11	10	simprbi	$⊢ r \in \{q \in ℙ \| q < N\} \to r < N$
12	11	ad2antlr	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land \forall z \in \{q \in ℙ \| q < N\} z \leq r) \to r < N$
13		elfzo2	$⊢ z \in (r + 1 ..^N) \leftrightarrow (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)$
14		breq1	$⊢ q = z \to (q < N \leftrightarrow z < N)$
15		simpl	$⊢ (z \in ℙ \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to z \in ℙ$
16		simpr3	$⊢ (z \in ℙ \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to z < N$
17	14 15 16	elrabd	$⊢ (z \in ℙ \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to z \in \{q \in ℙ \| q < N\}$
18	17	adantrl	$⊢ (z \in ℙ \land ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N))) \to z \in \{q \in ℙ \| q < N\}$
19		eluz2	$⊢ z \in ℤ_{\geq (r + 1)} \leftrightarrow (r + 1 \in ℤ \land z \in ℤ \land r + 1 \leq z)$
20		prmz	$⊢ r \in ℙ \to r \in ℤ$
21		zltp1le	$⊢ (r \in ℤ \land z \in ℤ) \to (r < z \leftrightarrow r + 1 \leq z)$
22	20 21	sylan	$⊢ (r \in ℙ \land z \in ℤ) \to (r < z \leftrightarrow r + 1 \leq z)$
23		prmnn	$⊢ r \in ℙ \to r \in ℕ$
24	23	nnred	$⊢ r \in ℙ \to r \in ℝ$
25		zre	$⊢ z \in ℤ \to z \in ℝ$
26		ltnle	$⊢ (r \in ℝ \land z \in ℝ) \to (r < z \leftrightarrow \neg z \leq r)$
27	26	biimpd	$⊢ (r \in ℝ \land z \in ℝ) \to (r < z \to \neg z \leq r)$
28	24 25 27	syl2an	$⊢ (r \in ℙ \land z \in ℤ) \to (r < z \to \neg z \leq r)$
29		pm2.21	$⊢ \neg z \leq r \to (z \leq r \to z \notin ℙ)$
30	28 29	syl6	$⊢ (r \in ℙ \land z \in ℤ) \to (r < z \to (z \leq r \to z \notin ℙ))$
31	22 30	sylbird	$⊢ (r \in ℙ \land z \in ℤ) \to (r + 1 \leq z \to (z \leq r \to z \notin ℙ))$
32	31	expcom	$⊢ z \in ℤ \to (r \in ℙ \to (r + 1 \leq z \to (z \leq r \to z \notin ℙ)))$
33	32	com23	$⊢ z \in ℤ \to (r + 1 \leq z \to (r \in ℙ \to (z \leq r \to z \notin ℙ)))$
34	33	a1i	$⊢ r + 1 \in ℤ \to (z \in ℤ \to (r + 1 \leq z \to (r \in ℙ \to (z \leq r \to z \notin ℙ))))$
35	34	3imp	$⊢ (r + 1 \in ℤ \land z \in ℤ \land r + 1 \leq z) \to (r \in ℙ \to (z \leq r \to z \notin ℙ))$
36	19 35	sylbi	$⊢ z \in ℤ_{\geq (r + 1)} \to (r \in ℙ \to (z \leq r \to z \notin ℙ))$
37	36	3ad2ant1	$⊢ (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N) \to (r \in ℙ \to (z \leq r \to z \notin ℙ))$
38	1 37	syl5com	$⊢ r \in \{q \in ℙ \| q < N\} \to ((z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N) \to (z \leq r \to z \notin ℙ))$
39	38	adantl	$⊢ (N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \to ((z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N) \to (z \leq r \to z \notin ℙ))$
40	39	imp	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to (z \leq r \to z \notin ℙ)$
41	40	adantl	$⊢ (z \in ℙ \land ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N))) \to (z \leq r \to z \notin ℙ)$
42	18 41	embantd	$⊢ (z \in ℙ \land ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N))) \to ((z \in \{q \in ℙ \| q < N\} \to z \leq r) \to z \notin ℙ)$
43	42	ex	$⊢ z \in ℙ \to (((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to ((z \in \{q \in ℙ \| q < N\} \to z \leq r) \to z \notin ℙ))$
44		df-nel	$⊢ z \notin ℙ \leftrightarrow \neg z \in ℙ$
45		2a1	$⊢ z \notin ℙ \to (((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to ((z \in \{q \in ℙ \| q < N\} \to z \leq r) \to z \notin ℙ))$
46	44 45	sylbir	$⊢ \neg z \in ℙ \to (((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to ((z \in \{q \in ℙ \| q < N\} \to z \leq r) \to z \notin ℙ))$
47	43 46	pm2.61i	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N)) \to ((z \in \{q \in ℙ \| q < N\} \to z \leq r) \to z \notin ℙ)$
48	47	impancom	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in \{q \in ℙ \| q < N\} \to z \leq r)) \to ((z \in ℤ_{\geq (r + 1)} \land N \in ℤ \land z < N) \to z \notin ℙ)$
49	13 48	biimtrid	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land (z \in \{q \in ℙ \| q < N\} \to z \leq r)) \to (z \in (r + 1 ..^N) \to z \notin ℙ)$
50	49	ex	$⊢ (N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \to ((z \in \{q \in ℙ \| q < N\} \to z \leq r) \to (z \in (r + 1 ..^N) \to z \notin ℙ))$
51	50	ralimdv2	$⊢ (N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \to (\forall z \in \{q \in ℙ \| q < N\} z \leq r \to \forall z \in (r + 1 ..^N) z \notin ℙ)$
52	51	imp	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land \forall z \in \{q \in ℙ \| q < N\} z \leq r) \to \forall z \in (r + 1 ..^N) z \notin ℙ$
53	12 52	jca	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land \forall z \in \{q \in ℙ \| q < N\} z \leq r) \to (r < N \land \forall z \in (r + 1 ..^N) z \notin ℙ)$
54	2 8 53	rspcedvd	$⊢ ((N \in ℤ_{\geq 3} \land r \in \{q \in ℙ \| q < N\}) \land \forall z \in \{q \in ℙ \| q < N\} z \leq r) \to \exists p \in ℙ (p < N \land \forall z \in (p + 1 ..^N) z \notin ℙ)$
55		eqid	$⊢ \{q \in ℙ \| q < N\} = \{q \in ℙ \| q < N\}$
56	55	prmgaplem3	$⊢ N \in ℤ_{\geq 3} \to \exists r \in \{q \in ℙ \| q < N\} \forall z \in \{q \in ℙ \| q < N\} z \leq r$
57	54 56	r19.29a	$⊢ N \in ℤ_{\geq 3} \to \exists p \in ℙ (p < N \land \forall z \in (p + 1 ..^N) z \notin ℙ)$

Metamath Proof Explorer

Theorem prmgaplem5

Proof