Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . 5
⊢ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ ℙ |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ ℙ) |
3 | | prmssnn 15390 |
. . . . 5
⊢ ℙ
⊆ ℕ |
4 | | nnssre 11024 |
. . . . 5
⊢ ℕ
⊆ ℝ |
5 | 3, 4 | sstri 3612 |
. . . 4
⊢ ℙ
⊆ ℝ |
6 | 2, 5 | syl6ss 3615 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ ℝ) |
7 | | fzfid 12772 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑁...𝑃) ∈ Fin) |
8 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑝 = 𝑖 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑖)) |
9 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑝 = 𝑖 → (𝑝 ≤ 𝑃 ↔ 𝑖 ≤ 𝑃)) |
10 | 8, 9 | anbi12d 747 |
. . . . . . 7
⊢ (𝑝 = 𝑖 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃) ↔ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃))) |
11 | 10 | elrab 3363 |
. . . . . 6
⊢ (𝑖 ∈ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ↔ (𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃))) |
12 | | nnz 11399 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
13 | | prmz 15389 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
14 | 12, 13 | anim12i 590 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑁 ∈ ℤ ∧ 𝑃 ∈
ℤ)) |
15 | 14 | 3adant3 1081 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ)) |
16 | | prmz 15389 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℙ → 𝑖 ∈
ℤ) |
17 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃)) → 𝑖 ∈ ℤ) |
18 | 15, 17 | anim12i 590 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) ∧ (𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃))) → ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑖 ∈ ℤ)) |
19 | | df-3an 1039 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ) ↔ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑖 ∈
ℤ)) |
20 | 18, 19 | sylibr 224 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) ∧ (𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃))) → (𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
21 | | nnre 11027 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑁 ∈
ℝ) |
23 | 5 | sseli 3599 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℙ → 𝑖 ∈
ℝ) |
24 | | ltle 10126 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑁 < 𝑖 → 𝑁 ≤ 𝑖)) |
25 | 22, 23, 24 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑖 ∈ ℙ) → (𝑁 < 𝑖 → 𝑁 ≤ 𝑖)) |
26 | 25 | anim1d 588 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑖 ∈ ℙ) → ((𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃) → (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃))) |
27 | 26 | ex 450 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑖 ∈ ℙ → ((𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃) → (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃)))) |
28 | 27 | 3adant3 1081 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑖 ∈ ℙ → ((𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃) → (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃)))) |
29 | 28 | imp32 449 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) ∧ (𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃))) → (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃)) |
30 | | elfz2 12333 |
. . . . . . . 8
⊢ (𝑖 ∈ (𝑁...𝑃) ↔ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑃))) |
31 | 20, 29, 30 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) ∧ (𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃))) → 𝑖 ∈ (𝑁...𝑃)) |
32 | 31 | ex 450 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → ((𝑖 ∈ ℙ ∧ (𝑁 < 𝑖 ∧ 𝑖 ≤ 𝑃)) → 𝑖 ∈ (𝑁...𝑃))) |
33 | 11, 32 | syl5bi 232 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑖 ∈ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} → 𝑖 ∈ (𝑁...𝑃))) |
34 | 33 | ssrdv 3609 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ (𝑁...𝑃)) |
35 | | ssfi 8180 |
. . . 4
⊢ (((𝑁...𝑃) ∈ Fin ∧ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ (𝑁...𝑃)) → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ∈ Fin) |
36 | 7, 34, 35 | syl2anc 693 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ∈ Fin) |
37 | | simp2 1062 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → 𝑃 ∈ ℙ) |
38 | | prmnn 15388 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
39 | 38 | nnred 11035 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
40 | 39 | leidd 10594 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ≤ 𝑃) |
41 | 40 | anim1i 592 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑃 ≤ 𝑃 ∧ 𝑁 < 𝑃)) |
42 | 41 | ancomd 467 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃)) |
43 | 42 | 3adant1 1079 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃)) |
44 | | breq2 4657 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑃)) |
45 | | breq1 4656 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑝 ≤ 𝑃 ↔ 𝑃 ≤ 𝑃)) |
46 | 44, 45 | anbi12d 747 |
. . . . . 6
⊢ (𝑝 = 𝑃 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃) ↔ (𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃))) |
47 | 46 | elrab 3363 |
. . . . 5
⊢ (𝑃 ∈ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ↔ (𝑃 ∈ ℙ ∧ (𝑁 < 𝑃 ∧ 𝑃 ≤ 𝑃))) |
48 | 37, 43, 47 | sylanbrc 698 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → 𝑃 ∈ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)}) |
49 | | ne0i 3921 |
. . . 4
⊢ (𝑃 ∈ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ≠ ∅) |
50 | 48, 49 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ≠ ∅) |
51 | | prmgaplem4.a |
. . . 4
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} |
52 | | sseq1 3626 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} → (𝐴 ⊆ ℝ ↔ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ ℝ)) |
53 | | eleq1 2689 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} → (𝐴 ∈ Fin ↔ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ∈ Fin)) |
54 | | neeq1 2856 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} → (𝐴 ≠ ∅ ↔ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ≠ ∅)) |
55 | 52, 53, 54 | 3anbi123d 1399 |
. . . 4
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} → ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ↔ ({𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ ℝ ∧ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ≠ ∅))) |
56 | 51, 55 | ax-mp 5 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ↔ ({𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⊆ ℝ ∧ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ≠ ∅)) |
57 | 6, 36, 50, 56 | syl3anbrc 1246 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → (𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅)) |
58 | | fiminre 10972 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
59 | 57, 58 | syl 17 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |