Step | Hyp | Ref
| Expression |
1 | | zre 11258 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
2 | | nnrp 11718 |
. . . . . . . 8
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ+) |
3 | | modlt 12541 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝑁 mod 𝐷) < 𝐷) |
4 | 1, 2, 3 | syl2an 493 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) < 𝐷) |
5 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ) |
6 | | nnne0 10930 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℕ → 𝐷 ≠ 0) |
7 | | redivcl 10623 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0) → (𝑁 / 𝐷) ∈ ℝ) |
8 | 1, 5, 6, 7 | syl3an 1360 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℝ) |
9 | 8 | 3anidm23 1377 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℝ) |
10 | 9 | flcld 12461 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℤ) |
11 | | nnz 11276 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℤ) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℤ) |
13 | | zmodcl 12552 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈
ℕ0) |
14 | 13 | nn0zd 11356 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℤ) |
15 | | zsubcl 11296 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 𝐷) ∈ ℤ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) |
16 | 14, 15 | syldan 486 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) |
17 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℂ) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℂ) |
19 | 10 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℂ) |
20 | 18, 19 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = ((⌊‘(𝑁 / 𝐷)) · 𝐷)) |
21 | | modval 12532 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
22 | 1, 2, 21 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
23 | | zcn 11259 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℂ) |
25 | | zmulcl 11303 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ ℤ ∧
(⌊‘(𝑁 / 𝐷)) ∈ ℤ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
26 | 11, 10, 25 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ)) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
27 | 26 | anabss7 858 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
28 | 27 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℂ) |
29 | 13 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℂ) |
30 | | subsub23 10165 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℂ ∧ (𝑁 mod 𝐷) ∈ ℂ) → ((𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) = (𝑁 mod 𝐷) ↔ (𝑁 − (𝑁 mod 𝐷)) = (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
31 | 24, 28, 29, 30 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) = (𝑁 mod 𝐷) ↔ (𝑁 − (𝑁 mod 𝐷)) = (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
32 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ ((𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) = (𝑁 mod 𝐷) ↔ (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
33 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ ((𝑁 − (𝑁 mod 𝐷)) = (𝐷 · (⌊‘(𝑁 / 𝐷))) ↔ (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷))) |
34 | 31, 32, 33 | 3bitr3g 301 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) ↔ (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷)))) |
35 | 22, 34 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷))) |
36 | 20, 35 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) |
37 | | dvds0lem 14830 |
. . . . . . . 8
⊢
((((⌊‘(𝑁
/ 𝐷)) ∈ ℤ ∧
𝐷 ∈ ℤ ∧
(𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) ∧
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) |
38 | 10, 12, 16, 36, 37 | syl31anc 1321 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) |
39 | | divalg2 14966 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) |
40 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑧 < 𝐷 ↔ (𝑁 mod 𝐷) < 𝐷)) |
41 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑁 − 𝑧) = (𝑁 − (𝑁 mod 𝐷))) |
42 | 41 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷)))) |
43 | 40, 42 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑧 = (𝑁 mod 𝐷) → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ ((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))))) |
44 | 43 | riota2 6533 |
. . . . . . . 8
⊢ (((𝑁 mod 𝐷) ∈ ℕ0 ∧
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) |
45 | 13, 39, 44 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) |
46 | 4, 38, 45 | mpbi2and 958 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(℩𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷)) |
47 | 46 | eqcomd 2616 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))) |
48 | 47 | sneqd 4137 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
49 | | snriota 6540 |
. . . . 5
⊢
(∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) → {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
50 | 39, 49 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {𝑧 ∈ ℕ0
∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
51 | 48, 50 | eqtr4d 2647 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))}) |
52 | 51 | eleq2d 2673 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑟 ∈ {(𝑁 mod 𝐷)} ↔ 𝑟 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) |
53 | | velsn 4141 |
. 2
⊢ (𝑟 ∈ {(𝑁 mod 𝐷)} ↔ 𝑟 = (𝑁 mod 𝐷)) |
54 | | breq1 4586 |
. . . 4
⊢ (𝑧 = 𝑟 → (𝑧 < 𝐷 ↔ 𝑟 < 𝐷)) |
55 | | oveq2 6557 |
. . . . 5
⊢ (𝑧 = 𝑟 → (𝑁 − 𝑧) = (𝑁 − 𝑟)) |
56 | 55 | breq2d 4595 |
. . . 4
⊢ (𝑧 = 𝑟 → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − 𝑟))) |
57 | 54, 56 | anbi12d 743 |
. . 3
⊢ (𝑧 = 𝑟 → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
58 | 57 | elrab 3331 |
. 2
⊢ (𝑟 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} ↔ (𝑟 ∈ ℕ0 ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
59 | 52, 53, 58 | 3bitr3g 301 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑟 = (𝑁 mod 𝐷) ↔ (𝑟 ∈ ℕ0 ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |