Metamath Proof Explorer

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 ⊢N∈ℕ→∃p∈ℙN<p∧∀z∈N+1..^pz∉ℙ

Proof

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