Theorem prmgaplem3

Description: Lemma for prmgap . (Contributed by AV, 9-Aug-2020)

	Ref	Expression
Hypothesis	prmgaplem3.a	⊢ 𝐴 = { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 }
Assertion	prmgaplem3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		prmgaplem3.a	⊢ 𝐴 = { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 }
2		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ℙ
3	2	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ℙ )
4		prmssnn	⊢ ℙ ⊆ ℕ
5		nnssre	⊢ ℕ ⊆ ℝ
6	4 5	sstri	⊢ ℙ ⊆ ℝ
7	3 6	sstrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ℝ )
8		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
9		breq1	⊢ ( 𝑝 = 𝑖 → ( 𝑝 < 𝑁 ↔ 𝑖 < 𝑁 ) )
10	9	elrab	⊢ ( 𝑖 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ↔ ( 𝑖 ∈ ℙ ∧ 𝑖 < 𝑁 ) )
11		prmnn	⊢ ( 𝑖 ∈ ℙ → 𝑖 ∈ ℕ )
12	11	nnnn0d	⊢ ( 𝑖 ∈ ℙ → 𝑖 ∈ ℕ0 )
13	12	ad2antrl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑖 ∈ ℙ ∧ 𝑖 < 𝑁 ) ) → 𝑖 ∈ ℕ0 )
14		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
15	14	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑖 ∈ ℙ ∧ 𝑖 < 𝑁 ) ) → 𝑁 ∈ ℕ )
16		simprr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑖 ∈ ℙ ∧ 𝑖 < 𝑁 ) ) → 𝑖 < 𝑁 )
17		elfzo0	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) )
18	13 15 16 17	syl3anbrc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑖 ∈ ℙ ∧ 𝑖 < 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
19	18	ex	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑖 ∈ ℙ ∧ 𝑖 < 𝑁 ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
20	10 19	syl5bi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑖 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } → 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
21	20	ssrdv	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ( 0 ..^ 𝑁 ) )
22		ssfi	⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ( 0 ..^ 𝑁 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ∈ Fin )
23	8 21 22	sylancr	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ∈ Fin )
24		breq1	⊢ ( 𝑝 = 2 → ( 𝑝 < 𝑁 ↔ 2 < 𝑁 ) )
25		2prm	⊢ 2 ∈ ℙ
26	25	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℙ )
27		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) )
28		df-3	⊢ 3 = ( 2 + 1 )
29	28	breq1i	⊢ ( 3 ≤ 𝑁 ↔ ( 2 + 1 ) ≤ 𝑁 )
30		2z	⊢ 2 ∈ ℤ
31		zltp1le	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 < 𝑁 ↔ ( 2 + 1 ) ≤ 𝑁 ) )
32	30 31	mpan	⊢ ( 𝑁 ∈ ℤ → ( 2 < 𝑁 ↔ ( 2 + 1 ) ≤ 𝑁 ) )
33	32	biimprd	⊢ ( 𝑁 ∈ ℤ → ( ( 2 + 1 ) ≤ 𝑁 → 2 < 𝑁 ) )
34	29 33	syl5bi	⊢ ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 → 2 < 𝑁 ) )
35	34	imp	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 )
36	35	3adant1	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 )
37	27 36	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 < 𝑁 )
38	24 26 37	elrabd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } )
39	38	ne0d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ≠ ∅ )
40		sseq1	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } → ( 𝐴 ⊆ ℝ ↔ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ℝ ) )
41		eleq1	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } → ( 𝐴 ∈ Fin ↔ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ∈ Fin ) )
42		neeq1	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } → ( 𝐴 ≠ ∅ ↔ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ≠ ∅ ) )
43	40 41 42	3anbi123d	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } → ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ↔ ( { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ℝ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ≠ ∅ ) ) )
44	1 43	ax-mp	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ↔ ( { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ⊆ ℝ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 < 𝑁 } ≠ ∅ ) )
45	7 23 39 44	syl3anbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) )
46		fimaxre	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
47	45 46	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )