Step | Hyp | Ref
| Expression |
1 | | ssrab2 3979 |
. . . . 5
⊢ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℙ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℙ) |
3 | | prmssnn 16129 |
. . . . 5
⊢ ℙ
⊆ ℕ |
4 | | nnssre 11732 |
. . . . 5
⊢ ℕ
⊆ ℝ |
5 | 3, 4 | sstri 3896 |
. . . 4
⊢ ℙ
⊆ ℝ |
6 | 2, 5 | sstrdi 3899 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ) |
7 | | fzofi 13445 |
. . . 4
⊢
(0..^𝑁) ∈
Fin |
8 | | breq1 5043 |
. . . . . . 7
⊢ (𝑝 = 𝑖 → (𝑝 < 𝑁 ↔ 𝑖 < 𝑁)) |
9 | 8 | elrab 3593 |
. . . . . 6
⊢ (𝑖 ∈ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ↔ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) |
10 | | prmnn 16127 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℙ → 𝑖 ∈
ℕ) |
11 | 10 | nnnn0d 12048 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℙ → 𝑖 ∈
ℕ0) |
12 | 11 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑖 ∈ ℕ0) |
13 | | eluzge3nn 12384 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
14 | 13 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑁 ∈ ℕ) |
15 | | simprr 773 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑖 < 𝑁) |
16 | | elfzo0 13181 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) |
17 | 12, 14, 15, 16 | syl3anbrc 1344 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑖 ∈ (0..^𝑁)) |
18 | 17 | ex 416 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑖 ∈ ℙ ∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^𝑁))) |
19 | 9, 18 | syl5bi 245 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → 𝑖 ∈ (0..^𝑁))) |
20 | 19 | ssrdv 3893 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ (0..^𝑁)) |
21 | | ssfi 8784 |
. . . 4
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑝 ∈ ℙ
∣ 𝑝 < 𝑁} ⊆ (0..^𝑁)) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin) |
22 | 7, 20, 21 | sylancr 590 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin) |
23 | | breq1 5043 |
. . . . 5
⊢ (𝑝 = 2 → (𝑝 < 𝑁 ↔ 2 < 𝑁)) |
24 | | 2prm 16145 |
. . . . . 6
⊢ 2 ∈
ℙ |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℙ) |
26 | | eluz2 12342 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤
𝑁)) |
27 | | df-3 11792 |
. . . . . . . . . 10
⊢ 3 = (2 +
1) |
28 | 27 | breq1i 5047 |
. . . . . . . . 9
⊢ (3 ≤
𝑁 ↔ (2 + 1) ≤ 𝑁) |
29 | | 2z 12107 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
30 | | zltp1le 12125 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁)) |
31 | 29, 30 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (2 <
𝑁 ↔ (2 + 1) ≤ 𝑁)) |
32 | 31 | biimprd 251 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((2 + 1)
≤ 𝑁 → 2 < 𝑁)) |
33 | 28, 32 | syl5bi 245 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → 2 < 𝑁)) |
34 | 33 | imp 410 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 2 < 𝑁) |
35 | 34 | 3adant1 1131 |
. . . . . 6
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 2 < 𝑁) |
36 | 26, 35 | sylbi 220 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 < 𝑁) |
37 | 23, 25, 36 | elrabd 3595 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁}) |
38 | 37 | ne0d 4234 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅) |
39 | | prmgaplem3.a |
. . . 4
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} |
40 | | sseq1 3912 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → (𝐴 ⊆ ℝ ↔ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ)) |
41 | | eleq1 2821 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → (𝐴 ∈ Fin ↔ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin)) |
42 | | neeq1 2997 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → (𝐴 ≠ ∅ ↔ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅)) |
43 | 40, 41, 42 | 3anbi123d 1437 |
. . . 4
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ↔ ({𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅))) |
44 | 39, 43 | ax-mp 5 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ↔ ({𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅)) |
45 | 6, 22, 38, 44 | syl3anbrc 1344 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅)) |
46 | | fimaxre 11674 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
47 | 45, 46 | syl 17 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |