Theorem prmgaplem4

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

	Ref	Expression
Hypothesis	prmgaplem4.a	⊢ 𝐴 = { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) }
Assertion	prmgaplem4	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		prmgaplem4.a	⊢ 𝐴 = { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) }
2		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ℙ
3	2	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ℙ )
4		prmssnn	⊢ ℙ ⊆ ℕ
5		nnssre	⊢ ℕ ⊆ ℝ
6	4 5	sstri	⊢ ℙ ⊆ ℝ
7	3 6	sstrdi	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ℝ )
8		fzfid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝑁 ... 𝑃 ) ∈ Fin )
9		breq2	⊢ ( 𝑝 = 𝑖 → ( 𝑁 < 𝑝 ↔ 𝑁 < 𝑖 ) )
10		breq1	⊢ ( 𝑝 = 𝑖 → ( 𝑝 ≤ 𝑃 ↔ 𝑖 ≤ 𝑃 ) )
11	9 10	anbi12d	⊢ ( 𝑝 = 𝑖 → ( ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) ↔ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) )
12	11	elrab	⊢ ( 𝑖 ∈ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ↔ ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) )
13		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
14		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
15	13 14	anim12i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) )
16	15	3adant3	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) )
17		prmz	⊢ ( 𝑖 ∈ ℙ → 𝑖 ∈ ℤ )
18	17	adantr	⊢ ( ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) → 𝑖 ∈ ℤ )
19	16 18	anim12i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) ∧ ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) ) → ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑖 ∈ ℤ ) )
20		df-3an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑖 ∈ ℤ ) )
21	19 20	sylibr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) ∧ ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) ) → ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ ) )
22		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
23	22	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ℝ )
24	6	sseli	⊢ ( 𝑖 ∈ ℙ → 𝑖 ∈ ℝ )
25		ltle	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑖 ∈ ℝ ) → ( 𝑁 < 𝑖 → 𝑁 ≤ 𝑖 ) )
26	23 24 25	syl2an	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑖 ∈ ℙ ) → ( 𝑁 < 𝑖 → 𝑁 ≤ 𝑖 ) )
27	26	anim1d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑖 ∈ ℙ ) → ( ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) → ( 𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) )
28	27	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 𝑖 ∈ ℙ → ( ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) → ( 𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) ) )
29	28	3adant3	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝑖 ∈ ℙ → ( ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) → ( 𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) ) )
30	29	imp32	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) ∧ ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) ) → ( 𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃 ) )
31		elfz2	⊢ ( 𝑖 ∈ ( 𝑁 ... 𝑃 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) )
32	21 30 31	sylanbrc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) ∧ ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) ) → 𝑖 ∈ ( 𝑁 ... 𝑃 ) )
33	32	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( ( 𝑖 ∈ ℙ ∧ ( 𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃 ) ) → 𝑖 ∈ ( 𝑁 ... 𝑃 ) ) )
34	12 33	biimtrid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝑖 ∈ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } → 𝑖 ∈ ( 𝑁 ... 𝑃 ) ) )
35	34	ssrdv	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ( 𝑁 ... 𝑃 ) )
36	8 35	ssfid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ∈ Fin )
37		breq2	⊢ ( 𝑝 = 𝑃 → ( 𝑁 < 𝑝 ↔ 𝑁 < 𝑃 ) )
38		breq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≤ 𝑃 ↔ 𝑃 ≤ 𝑃 ) )
39	37 38	anbi12d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) ↔ ( 𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃 ) ) )
40		simp2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → 𝑃 ∈ ℙ )
41		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
42	41	nnred	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
43	42	leidd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ≤ 𝑃 )
44	43	anim1ci	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃 ) )
45	44	3adant1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃 ) )
46	39 40 45	elrabd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → 𝑃 ∈ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } )
47	46	ne0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ≠ ∅ )
48		sseq1	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } → ( 𝐴 ⊆ ℝ ↔ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ℝ ) )
49		eleq1	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } → ( 𝐴 ∈ Fin ↔ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ∈ Fin ) )
50		neeq1	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } → ( 𝐴 ≠ ∅ ↔ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ≠ ∅ ) )
51	48 49 50	3anbi123d	⊢ ( 𝐴 = { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } → ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ↔ ( { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ℝ ∧ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ≠ ∅ ) ) )
52	1 51	ax-mp	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ↔ ( { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ⊆ ℝ ∧ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃 ) } ≠ ∅ ) )
53	7 36 47 52	syl3anbrc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) )
54		fiminre	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
55	53 54	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )