prmgaplem6

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

		Ref	Expression
	Assertion	prmgaplem6	$⊢ N \in ℕ \to \exists p \in ℙ (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ)$

Proof

Step	Hyp	Ref	Expression
1		prmunb	$⊢ N \in ℕ \to \exists n \in ℙ N < n$
2		eqid	$⊢ \{q \in ℙ \| (N < q \land q \leq n)\} = \{q \in ℙ \| (N < q \land q \leq n)\}$
3	2	prmgaplem4	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to \exists p \in \{q \in ℙ \| (N < q \land q \leq n)\} \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z$
4		breq2	$⊢ q = p \to (N < q \leftrightarrow N < p)$
5		breq1	$⊢ q = p \to (q \leq n \leftrightarrow p \leq n)$
6	4 5	anbi12d	$⊢ q = p \to ((N < q \land q \leq n) \leftrightarrow (N < p \land p \leq n))$
7	6	elrab	$⊢ p \in \{q \in ℙ \| (N < q \land q \leq n)\} \leftrightarrow (p \in ℙ \land (N < p \land p \leq n))$
8		simplrl	$⊢ (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \land \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z) \to p \in ℙ$
9		simprrl	$⊢ ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to N < p$
10	9	adantr	$⊢ (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \land \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z) \to N < p$
11		breq2	$⊢ q = z \to (N < q \leftrightarrow N < z)$
12		breq1	$⊢ q = z \to (q \leq n \leftrightarrow z \leq n)$
13	11 12	anbi12d	$⊢ q = z \to ((N < q \land q \leq n) \leftrightarrow (N < z \land z \leq n))$
14		simpll	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z \in (N + 1 ..^p)) \to z \in ℙ$
15		elfzo2	$⊢ z \in (N + 1 ..^p) \leftrightarrow (z \in ℤ_{\geq (N + 1)} \land p \in ℤ \land z < p)$
16		eluz2	$⊢ z \in ℤ_{\geq (N + 1)} \leftrightarrow (N + 1 \in ℤ \land z \in ℤ \land N + 1 \leq z)$
17		nnz	$⊢ N \in ℕ \to N \in ℤ$
18		prmz	$⊢ z \in ℙ \to z \in ℤ$
19		zltp1le	$⊢ (N \in ℤ \land z \in ℤ) \to (N < z \leftrightarrow N + 1 \leq z)$
20	17 18 19	syl2an	$⊢ (N \in ℕ \land z \in ℙ) \to (N < z \leftrightarrow N + 1 \leq z)$
21	20	exbiri	$⊢ N \in ℕ \to (z \in ℙ \to (N + 1 \leq z \to N < z))$
22	21	3ad2ant1	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to (z \in ℙ \to (N + 1 \leq z \to N < z))$
23	22	adantr	$⊢ ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to (z \in ℙ \to (N + 1 \leq z \to N < z))$
24	23	impcom	$⊢ (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (N + 1 \leq z \to N < z)$
25	24	com12	$⊢ N + 1 \leq z \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to N < z)$
26	25	adantr	$⊢ (N + 1 \leq z \land p \in ℤ) \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to N < z)$
27	26	adantr	$⊢ ((N + 1 \leq z \land p \in ℤ) \land z < p) \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to N < z)$
28	27	imp	$⊢ (((N + 1 \leq z \land p \in ℤ) \land z < p) \land (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))))) \to N < z$
29		prmnn	$⊢ z \in ℙ \to z \in ℕ$
30	29	nnred	$⊢ z \in ℙ \to z \in ℝ$
31	30	ad2antrl	$⊢ (n \in ℙ \land (z \in ℙ \land p \in ℙ)) \to z \in ℝ$
32		prmnn	$⊢ p \in ℙ \to p \in ℕ$
33	32	nnred	$⊢ p \in ℙ \to p \in ℝ$
34	33	adantl	$⊢ (z \in ℙ \land p \in ℙ) \to p \in ℝ$
35	34	adantl	$⊢ (n \in ℙ \land (z \in ℙ \land p \in ℙ)) \to p \in ℝ$
36		prmnn	$⊢ n \in ℙ \to n \in ℕ$
37	36	nnred	$⊢ n \in ℙ \to n \in ℝ$
38	37	adantr	$⊢ (n \in ℙ \land (z \in ℙ \land p \in ℙ)) \to n \in ℝ$
39		ltleletr	$⊢ (z \in ℝ \land p \in ℝ \land n \in ℝ) \to ((z < p \land p \leq n) \to z \leq n)$
40	31 35 38 39	syl3anc	$⊢ (n \in ℙ \land (z \in ℙ \land p \in ℙ)) \to ((z < p \land p \leq n) \to z \leq n)$
41	40	exp4b	$⊢ n \in ℙ \to ((z \in ℙ \land p \in ℙ) \to (z < p \to (p \leq n \to z \leq n)))$
42	41	3ad2ant2	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to ((z \in ℙ \land p \in ℙ) \to (z < p \to (p \leq n \to z \leq n)))$
43	42	expdcom	$⊢ z \in ℙ \to (p \in ℙ \to ((N \in ℕ \land n \in ℙ \land N < n) \to (z < p \to (p \leq n \to z \leq n))))$
44	43	com45	$⊢ z \in ℙ \to (p \in ℙ \to ((N \in ℕ \land n \in ℙ \land N < n) \to (p \leq n \to (z < p \to z \leq n))))$
45	44	com14	$⊢ p \leq n \to (p \in ℙ \to ((N \in ℕ \land n \in ℙ \land N < n) \to (z \in ℙ \to (z < p \to z \leq n))))$
46	45	adantl	$⊢ (N < p \land p \leq n) \to (p \in ℙ \to ((N \in ℕ \land n \in ℙ \land N < n) \to (z \in ℙ \to (z < p \to z \leq n))))$
47	46	impcom	$⊢ (p \in ℙ \land (N < p \land p \leq n)) \to ((N \in ℕ \land n \in ℙ \land N < n) \to (z \in ℙ \to (z < p \to z \leq n)))$
48	47	impcom	$⊢ ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to (z \in ℙ \to (z < p \to z \leq n))$
49	48	impcom	$⊢ (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (z < p \to z \leq n)$
50	49	adantld	$⊢ (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (((N + 1 \leq z \land p \in ℤ) \land z < p) \to z \leq n)$
51	50	impcom	$⊢ (((N + 1 \leq z \land p \in ℤ) \land z < p) \land (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))))) \to z \leq n$
52	28 51	jca	$⊢ (((N + 1 \leq z \land p \in ℤ) \land z < p) \land (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))))) \to (N < z \land z \leq n)$
53	52	exp41	$⊢ N + 1 \leq z \to (p \in ℤ \to (z < p \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (N < z \land z \leq n))))$
54	53	3ad2ant3	$⊢ (N + 1 \in ℤ \land z \in ℤ \land N + 1 \leq z) \to (p \in ℤ \to (z < p \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (N < z \land z \leq n))))$
55	16 54	sylbi	$⊢ z \in ℤ_{\geq (N + 1)} \to (p \in ℤ \to (z < p \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (N < z \land z \leq n))))$
56	55	3imp	$⊢ (z \in ℤ_{\geq (N + 1)} \land p \in ℤ \land z < p) \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (N < z \land z \leq n))$
57	15 56	sylbi	$⊢ z \in (N + 1 ..^p) \to ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (N < z \land z \leq n))$
58	57	impcom	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z \in (N + 1 ..^p)) \to (N < z \land z \leq n)$
59	13 14 58	elrabd	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z \in (N + 1 ..^p)) \to z \in \{q \in ℙ \| (N < q \land q \leq n)\}$
60		elfzolt2	$⊢ z \in (N + 1 ..^p) \to z < p$
61	33	ad2antrl	$⊢ ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to p \in ℝ$
62		ltnle	$⊢ (z \in ℝ \land p \in ℝ) \to (z < p \leftrightarrow \neg p \leq z)$
63	62	biimpd	$⊢ (z \in ℝ \land p \in ℝ) \to (z < p \to \neg p \leq z)$
64	30 61 63	syl2an	$⊢ (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (z < p \to \neg p \leq z)$
65	64	imp	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z < p) \to \neg p \leq z$
66	65	pm2.21d	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z < p) \to (p \leq z \to z \notin ℙ)$
67	60 66	sylan2	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z \in (N + 1 ..^p)) \to (p \leq z \to z \notin ℙ)$
68	59 67	embantd	$⊢ ((z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \land z \in (N + 1 ..^p)) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to z \notin ℙ)$
69	68	ex	$⊢ (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to (z \in (N + 1 ..^p) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to z \notin ℙ))$
70	69	com23	$⊢ (z \in ℙ \land ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n)))) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to (z \in (N + 1 ..^p) \to z \notin ℙ))$
71	70	ex	$⊢ z \in ℙ \to (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to (z \in (N + 1 ..^p) \to z \notin ℙ)))$
72		df-nel	$⊢ z \notin ℙ \leftrightarrow \neg z \in ℙ$
73		2a1	$⊢ z \notin ℙ \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to (z \in (N + 1 ..^p) \to z \notin ℙ))$
74	73	a1d	$⊢ z \notin ℙ \to (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to (z \in (N + 1 ..^p) \to z \notin ℙ)))$
75	72 74	sylbir	$⊢ \neg z \in ℙ \to (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to (z \in (N + 1 ..^p) \to z \notin ℙ)))$
76	71 75	pm2.61i	$⊢ ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to ((z \in \{q \in ℙ \| (N < q \land q \leq n)\} \to p \leq z) \to (z \in (N + 1 ..^p) \to z \notin ℙ))$
77	76	ralimdv2	$⊢ ((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \to (\forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z \to \forall z \in (N + 1 ..^p) z \notin ℙ)$
78	77	imp	$⊢ (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \land \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z) \to \forall z \in (N + 1 ..^p) z \notin ℙ$
79	8 10 78	jca32	$⊢ (((N \in ℕ \land n \in ℙ \land N < n) \land (p \in ℙ \land (N < p \land p \leq n))) \land \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z) \to (p \in ℙ \land (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ))$
80	79	exp31	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to ((p \in ℙ \land (N < p \land p \leq n)) \to (\forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z \to (p \in ℙ \land (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ))))$
81	7 80	biimtrid	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to (p \in \{q \in ℙ \| (N < q \land q \leq n)\} \to (\forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z \to (p \in ℙ \land (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ))))$
82	81	impd	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to ((p \in \{q \in ℙ \| (N < q \land q \leq n)\} \land \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z) \to (p \in ℙ \land (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ)))$
83	82	reximdv2	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to (\exists p \in \{q \in ℙ \| (N < q \land q \leq n)\} \forall z \in \{q \in ℙ \| (N < q \land q \leq n)\} p \leq z \to \exists p \in ℙ (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ))$
84	3 83	mpd	$⊢ (N \in ℕ \land n \in ℙ \land N < n) \to \exists p \in ℙ (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ)$
85	84	rexlimdv3a	$⊢ N \in ℕ \to (\exists n \in ℙ N < n \to \exists p \in ℙ (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ))$
86	1 85	mpd	$⊢ N \in ℕ \to \exists p \in ℙ (N < p \land \forall z \in (N + 1 ..^p) z \notin ℙ)$

Metamath Proof Explorer

Theorem prmgaplem6

Proof