Metamath Proof Explorer

Theorem prmgaplem3

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

Ref Expression
Hypothesis prmgaplem3.a ⊢A=p∈ℙ|p<N
Assertion prmgaplem3 ⊢N∈ℤ≥3→∃x∈A∀y∈Ay≤x

Proof

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