Step | Hyp | Ref
| Expression |
1 | | eluz2nn 9477 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
2 | | eleq1 2220 |
. . . 4
⊢ (𝑥 = 1 → (𝑥 ∈ (ℤ≥‘2)
↔ 1 ∈ (ℤ≥‘2))) |
3 | 2 | imbi1d 230 |
. . 3
⊢ (𝑥 = 1 → ((𝑥 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑥) ↔ (1 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥))) |
4 | | eleq1 2220 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (ℤ≥‘2)
↔ 𝑦 ∈
(ℤ≥‘2))) |
5 | | breq2 3969 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦)) |
6 | 5 | rexbidv 2458 |
. . . 4
⊢ (𝑥 = 𝑦 → (∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑦)) |
7 | 4, 6 | imbi12d 233 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑥) ↔ (𝑦 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑦))) |
8 | | eleq1 2220 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑥 ∈ (ℤ≥‘2)
↔ 𝑧 ∈
(ℤ≥‘2))) |
9 | | breq2 3969 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧)) |
10 | 9 | rexbidv 2458 |
. . . 4
⊢ (𝑥 = 𝑧 → (∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑧)) |
11 | 8, 10 | imbi12d 233 |
. . 3
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑥) ↔ (𝑧 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑧))) |
12 | | eleq1 2220 |
. . . 4
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 ∈ (ℤ≥‘2)
↔ (𝑦 · 𝑧) ∈
(ℤ≥‘2))) |
13 | | breq2 3969 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ (𝑦 · 𝑧))) |
14 | 13 | rexbidv 2458 |
. . . 4
⊢ (𝑥 = (𝑦 · 𝑧) → (∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃𝑝 ∈ ℙ 𝑝 ∥ (𝑦 · 𝑧))) |
15 | 12, 14 | imbi12d 233 |
. . 3
⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑥 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑥) ↔ ((𝑦 · 𝑧) ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ (𝑦 · 𝑧)))) |
16 | | eleq1 2220 |
. . . 4
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (ℤ≥‘2)
↔ 𝑁 ∈
(ℤ≥‘2))) |
17 | | breq2 3969 |
. . . . 5
⊢ (𝑥 = 𝑁 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑁)) |
18 | 17 | rexbidv 2458 |
. . . 4
⊢ (𝑥 = 𝑁 → (∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁)) |
19 | 16, 18 | imbi12d 233 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑥) ↔ (𝑁 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑁))) |
20 | | 1m1e0 8902 |
. . . . 5
⊢ (1
− 1) = 0 |
21 | | uz2m1nn 9516 |
. . . . 5
⊢ (1 ∈
(ℤ≥‘2) → (1 − 1) ∈
ℕ) |
22 | 20, 21 | eqeltrrid 2245 |
. . . 4
⊢ (1 ∈
(ℤ≥‘2) → 0 ∈ ℕ) |
23 | | 0nnn 8860 |
. . . . 5
⊢ ¬ 0
∈ ℕ |
24 | 23 | pm2.21i 636 |
. . . 4
⊢ (0 ∈
ℕ → ∃𝑝
∈ ℙ 𝑝 ∥
𝑥) |
25 | 22, 24 | syl 14 |
. . 3
⊢ (1 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥) |
26 | | prmz 11988 |
. . . . . 6
⊢ (𝑥 ∈ ℙ → 𝑥 ∈
ℤ) |
27 | | iddvds 11700 |
. . . . . 6
⊢ (𝑥 ∈ ℤ → 𝑥 ∥ 𝑥) |
28 | 26, 27 | syl 14 |
. . . . 5
⊢ (𝑥 ∈ ℙ → 𝑥 ∥ 𝑥) |
29 | | breq1 3968 |
. . . . . 6
⊢ (𝑝 = 𝑥 → (𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥)) |
30 | 29 | rspcev 2816 |
. . . . 5
⊢ ((𝑥 ∈ ℙ ∧ 𝑥 ∥ 𝑥) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥) |
31 | 28, 30 | mpdan 418 |
. . . 4
⊢ (𝑥 ∈ ℙ →
∃𝑝 ∈ ℙ
𝑝 ∥ 𝑥) |
32 | 31 | a1d 22 |
. . 3
⊢ (𝑥 ∈ ℙ → (𝑥 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑥)) |
33 | | simpl 108 |
. . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑦 ∈
(ℤ≥‘2)) |
34 | | eluzelz 9448 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
35 | 34 | ad2antrr 480 |
. . . . . . . . 9
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑦 ∈
ℤ) |
36 | | eluzelz 9448 |
. . . . . . . . . 10
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
37 | 36 | ad2antlr 481 |
. . . . . . . . 9
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑧 ∈
ℤ) |
38 | | dvdsmul1 11709 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑦 ∥ (𝑦 · 𝑧)) |
39 | 35, 37, 38 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑦 ∥ (𝑦 · 𝑧)) |
40 | | prmz 11988 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
41 | 40 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ 𝑝 ∈
ℤ) |
42 | 35, 37 | zmulcld 9292 |
. . . . . . . . 9
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ (𝑦 · 𝑧) ∈
ℤ) |
43 | | dvdstr 11724 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ (𝑦 · 𝑧) ∈ ℤ) → ((𝑝 ∥ 𝑦 ∧ 𝑦 ∥ (𝑦 · 𝑧)) → 𝑝 ∥ (𝑦 · 𝑧))) |
44 | 41, 35, 42, 43 | syl3anc 1220 |
. . . . . . . 8
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ ((𝑝 ∥ 𝑦 ∧ 𝑦 ∥ (𝑦 · 𝑧)) → 𝑝 ∥ (𝑦 · 𝑧))) |
45 | 39, 44 | mpan2d 425 |
. . . . . . 7
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑝 ∈ ℙ)
→ (𝑝 ∥ 𝑦 → 𝑝 ∥ (𝑦 · 𝑧))) |
46 | 45 | reximdva 2559 |
. . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (∃𝑝 ∈
ℙ 𝑝 ∥ 𝑦 → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝑦 · 𝑧))) |
47 | 33, 46 | embantd 56 |
. . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝑦 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑦) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝑦 · 𝑧))) |
48 | 47 | a1dd 48 |
. . . 4
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝑦 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑦) → ((𝑦 · 𝑧) ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ (𝑦 · 𝑧)))) |
49 | 48 | adantrd 277 |
. . 3
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (((𝑦 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑦) ∧ (𝑧 ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ 𝑧)) → ((𝑦 · 𝑧) ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥ (𝑦 · 𝑧)))) |
50 | 3, 7, 11, 15, 19, 25, 32, 49 | prmind 11998 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑁 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁)) |
51 | 1, 50 | mpcom 36 |
1
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |