Step | Hyp | Ref
| Expression |
1 | | divalglem0.2 |
. . . . . 6
⊢ 𝐷 ∈ ℤ |
2 | | divalglem0.1 |
. . . . . . 7
⊢ 𝑁 ∈ ℤ |
3 | | nn0z 11729 |
. . . . . . 7
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℤ) |
4 | | zsubcl 11748 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑁 − 𝑧) ∈ ℤ) |
5 | 2, 3, 4 | sylancr 583 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0
→ (𝑁 − 𝑧) ∈
ℤ) |
6 | | divides 15360 |
. . . . . 6
⊢ ((𝐷 ∈ ℤ ∧ (𝑁 − 𝑧) ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑧) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑧))) |
7 | 1, 5, 6 | sylancr 583 |
. . . . 5
⊢ (𝑧 ∈ ℕ0
→ (𝐷 ∥ (𝑁 − 𝑧) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑧))) |
8 | | nn0cn 11630 |
. . . . . . . 8
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℂ) |
9 | | zmulcl 11755 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 · 𝐷) ∈ ℤ) |
10 | 1, 9 | mpan2 684 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℤ → (𝑞 · 𝐷) ∈ ℤ) |
11 | 10 | zcnd 11812 |
. . . . . . . 8
⊢ (𝑞 ∈ ℤ → (𝑞 · 𝐷) ∈ ℂ) |
12 | | zcn 11710 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
13 | 2, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑁 ∈ ℂ |
14 | | subadd 10605 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → ((𝑁 − 𝑧) = (𝑞 · 𝐷) ↔ (𝑧 + (𝑞 · 𝐷)) = 𝑁)) |
15 | 13, 14 | mp3an1 1578 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → ((𝑁 − 𝑧) = (𝑞 · 𝐷) ↔ (𝑧 + (𝑞 · 𝐷)) = 𝑁)) |
16 | | addcom 10542 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → (𝑧 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑧)) |
17 | 16 | eqeq1d 2828 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → ((𝑧 + (𝑞 · 𝐷)) = 𝑁 ↔ ((𝑞 · 𝐷) + 𝑧) = 𝑁)) |
18 | 15, 17 | bitrd 271 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → ((𝑁 − 𝑧) = (𝑞 · 𝐷) ↔ ((𝑞 · 𝐷) + 𝑧) = 𝑁)) |
19 | 8, 11, 18 | syl2an 591 |
. . . . . . 7
⊢ ((𝑧 ∈ ℕ0
∧ 𝑞 ∈ ℤ)
→ ((𝑁 − 𝑧) = (𝑞 · 𝐷) ↔ ((𝑞 · 𝐷) + 𝑧) = 𝑁)) |
20 | | eqcom 2833 |
. . . . . . 7
⊢ ((𝑁 − 𝑧) = (𝑞 · 𝐷) ↔ (𝑞 · 𝐷) = (𝑁 − 𝑧)) |
21 | | eqcom 2833 |
. . . . . . 7
⊢ (((𝑞 · 𝐷) + 𝑧) = 𝑁 ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑧)) |
22 | 19, 20, 21 | 3bitr3g 305 |
. . . . . 6
⊢ ((𝑧 ∈ ℕ0
∧ 𝑞 ∈ ℤ)
→ ((𝑞 · 𝐷) = (𝑁 − 𝑧) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
23 | 22 | rexbidva 3260 |
. . . . 5
⊢ (𝑧 ∈ ℕ0
→ (∃𝑞 ∈
ℤ (𝑞 · 𝐷) = (𝑁 − 𝑧) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
24 | 7, 23 | bitrd 271 |
. . . 4
⊢ (𝑧 ∈ ℕ0
→ (𝐷 ∥ (𝑁 − 𝑧) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
25 | 24 | pm5.32i 572 |
. . 3
⊢ ((𝑧 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ (𝑧 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
26 | | oveq2 6914 |
. . . . 5
⊢ (𝑟 = 𝑧 → (𝑁 − 𝑟) = (𝑁 − 𝑧)) |
27 | 26 | breq2d 4886 |
. . . 4
⊢ (𝑟 = 𝑧 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝑧))) |
28 | | divalglem2.4 |
. . . 4
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} |
29 | 27, 28 | elrab2 3590 |
. . 3
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑧))) |
30 | | oveq2 6914 |
. . . . . 6
⊢ (𝑟 = 𝑧 → ((𝑞 · 𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑧)) |
31 | 30 | eqeq2d 2836 |
. . . . 5
⊢ (𝑟 = 𝑧 → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
32 | 31 | rexbidv 3263 |
. . . 4
⊢ (𝑟 = 𝑧 → (∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
33 | 32 | elrab 3586 |
. . 3
⊢ (𝑧 ∈ {𝑟 ∈ ℕ0 ∣
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑟)} ↔ (𝑧 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑧))) |
34 | 25, 29, 33 | 3bitr4i 295 |
. 2
⊢ (𝑧 ∈ 𝑆 ↔ 𝑧 ∈ {𝑟 ∈ ℕ0 ∣
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑟)}) |
35 | 34 | eqriv 2823 |
1
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑟)} |