Theorem 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	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ ∀ 𝑧 ∈ ( ( 𝑁 + 1 ) ..^ 𝑝 ) 𝑧 ∉ ℙ ) )

Proof

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