Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . 5
⊢ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℙ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℙ) |
3 | | prmssnn 15390 |
. . . . 5
⊢ ℙ
⊆ ℕ |
4 | | nnssre 11024 |
. . . . 5
⊢ ℕ
⊆ ℝ |
5 | 3, 4 | sstri 3612 |
. . . 4
⊢ ℙ
⊆ ℝ |
6 | 2, 5 | syl6ss 3615 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ) |
7 | | fzofi 12773 |
. . . 4
⊢
(0..^𝑁) ∈
Fin |
8 | | breq1 4656 |
. . . . . . 7
⊢ (𝑝 = 𝑖 → (𝑝 < 𝑁 ↔ 𝑖 < 𝑁)) |
9 | 8 | elrab 3363 |
. . . . . 6
⊢ (𝑖 ∈ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ↔ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) |
10 | | prmnn 15388 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℙ → 𝑖 ∈
ℕ) |
11 | 10 | nnnn0d 11351 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℙ → 𝑖 ∈
ℕ0) |
12 | 11 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑖 ∈ ℕ0) |
13 | | eluzge3nn 11730 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑁 ∈ ℕ) |
15 | | simprr 796 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑖 < 𝑁) |
16 | | elfzo0 12508 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) |
17 | 12, 14, 15, 16 | syl3anbrc 1246 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑖 ∈ ℙ ∧ 𝑖 < 𝑁)) → 𝑖 ∈ (0..^𝑁)) |
18 | 17 | ex 450 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑖 ∈ ℙ ∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^𝑁))) |
19 | 9, 18 | syl5bi 232 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → 𝑖 ∈ (0..^𝑁))) |
20 | 19 | ssrdv 3609 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ (0..^𝑁)) |
21 | | ssfi 8180 |
. . . 4
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑝 ∈ ℙ
∣ 𝑝 < 𝑁} ⊆ (0..^𝑁)) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin) |
22 | 7, 20, 21 | sylancr 695 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin) |
23 | | 2prm 15405 |
. . . . . 6
⊢ 2 ∈
ℙ |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℙ) |
25 | | eluz2 11693 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤
𝑁)) |
26 | | df-3 11080 |
. . . . . . . . . 10
⊢ 3 = (2 +
1) |
27 | 26 | breq1i 4660 |
. . . . . . . . 9
⊢ (3 ≤
𝑁 ↔ (2 + 1) ≤ 𝑁) |
28 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
29 | | zltp1le 11427 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁)) |
30 | 28, 29 | mpan 706 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (2 <
𝑁 ↔ (2 + 1) ≤ 𝑁)) |
31 | 30 | biimprd 238 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((2 + 1)
≤ 𝑁 → 2 < 𝑁)) |
32 | 27, 31 | syl5bi 232 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → 2 < 𝑁)) |
33 | 32 | imp 445 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 2 < 𝑁) |
34 | 33 | 3adant1 1079 |
. . . . . 6
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 2 < 𝑁) |
35 | 25, 34 | sylbi 207 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 < 𝑁) |
36 | | breq1 4656 |
. . . . . 6
⊢ (𝑝 = 2 → (𝑝 < 𝑁 ↔ 2 < 𝑁)) |
37 | 36 | elrab 3363 |
. . . . 5
⊢ (2 ∈
{𝑝 ∈ ℙ ∣
𝑝 < 𝑁} ↔ (2 ∈ ℙ ∧ 2 <
𝑁)) |
38 | 24, 35, 37 | sylanbrc 698 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁}) |
39 | | ne0i 3921 |
. . . 4
⊢ (2 ∈
{𝑝 ∈ ℙ ∣
𝑝 < 𝑁} → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅) |
40 | 38, 39 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅) |
41 | | prmgaplem3.a |
. . . 4
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} |
42 | | sseq1 3626 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → (𝐴 ⊆ ℝ ↔ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ)) |
43 | | eleq1 2689 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → (𝐴 ∈ Fin ↔ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin)) |
44 | | neeq1 2856 |
. . . . 5
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → (𝐴 ≠ ∅ ↔ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅)) |
45 | 42, 43, 44 | 3anbi123d 1399 |
. . . 4
⊢ (𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} → ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ↔ ({𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅))) |
46 | 41, 45 | ax-mp 5 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ↔ ({𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⊆ ℝ ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ≠ ∅)) |
47 | 6, 22, 40, 46 | syl3anbrc 1246 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅)) |
48 | | fimaxre 10968 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
49 | 47, 48 | syl 17 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |