Step | Hyp | Ref
| Expression |
1 | | ovex 7055 |
. . . . . 6
⊢ (𝑁 mod 𝐷) ∈ V |
2 | 1 | snid 4512 |
. . . . 5
⊢ (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)} |
3 | | eleq1 2872 |
. . . . 5
⊢ (𝑅 = (𝑁 mod 𝐷) → (𝑅 ∈ {(𝑁 mod 𝐷)} ↔ (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)})) |
4 | 2, 3 | mpbiri 259 |
. . . 4
⊢ (𝑅 = (𝑁 mod 𝐷) → 𝑅 ∈ {(𝑁 mod 𝐷)}) |
5 | | elsni 4495 |
. . . 4
⊢ (𝑅 ∈ {(𝑁 mod 𝐷)} → 𝑅 = (𝑁 mod 𝐷)) |
6 | 4, 5 | impbii 210 |
. . 3
⊢ (𝑅 = (𝑁 mod 𝐷) ↔ 𝑅 ∈ {(𝑁 mod 𝐷)}) |
7 | | zre 11839 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
8 | | nnrp 12254 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ+) |
9 | | modlt 13102 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝑁 mod 𝐷) < 𝐷) |
10 | 7, 8, 9 | syl2an 595 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) < 𝐷) |
11 | | nnre 11499 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ) |
12 | | nnne0 11525 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ≠ 0) |
13 | | redivcl 11213 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0) → (𝑁 / 𝐷) ∈ ℝ) |
14 | 7, 11, 12, 13 | syl3an 1153 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℝ) |
15 | 14 | 3anidm23 1414 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℝ) |
16 | 15 | flcld 13022 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℤ) |
17 | | nnz 11858 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℤ) |
18 | 17 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℤ) |
19 | | zmodcl 13113 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈
ℕ0) |
20 | 19 | nn0zd 11939 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℤ) |
21 | | zsubcl 11878 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 𝐷) ∈ ℤ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) |
22 | 20, 21 | syldan 591 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) |
23 | | nncn 11500 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℂ) |
24 | 23 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℂ) |
25 | 16 | zcnd 11942 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℂ) |
26 | 24, 25 | mulcomd 10515 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = ((⌊‘(𝑁 / 𝐷)) · 𝐷)) |
27 | | modval 13093 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
28 | 7, 8, 27 | syl2an 595 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
29 | 19 | nn0cnd 11811 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℂ) |
30 | | zmulcl 11885 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ ℤ ∧
(⌊‘(𝑁 / 𝐷)) ∈ ℤ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
31 | 17, 16, 30 | syl2an2 682 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
32 | 31 | zcnd 11942 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℂ) |
33 | | zcn 11840 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
34 | 33 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℂ) |
35 | 29, 32, 34 | subexsub 10912 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) ↔ (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷)))) |
36 | 28, 35 | mpbid 233 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷))) |
37 | 26, 36 | eqtr3d 2835 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) |
38 | | dvds0lem 15457 |
. . . . . . . . 9
⊢
((((⌊‘(𝑁
/ 𝐷)) ∈ ℤ ∧
𝐷 ∈ ℤ ∧
(𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) ∧
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) |
39 | 16, 18, 22, 37, 38 | syl31anc 1366 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) |
40 | | divalg2 15593 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) |
41 | | breq1 4971 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑧 < 𝐷 ↔ (𝑁 mod 𝐷) < 𝐷)) |
42 | | oveq2 7031 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑁 − 𝑧) = (𝑁 − (𝑁 mod 𝐷))) |
43 | 42 | breq2d 4980 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷)))) |
44 | 41, 43 | anbi12d 630 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑁 mod 𝐷) → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ ((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))))) |
45 | 44 | riota2 7006 |
. . . . . . . . 9
⊢ (((𝑁 mod 𝐷) ∈ ℕ0 ∧
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) |
46 | 19, 40, 45 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) |
47 | 10, 39, 46 | mpbi2and 708 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(℩𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷)) |
48 | 47 | eqcomd 2803 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))) |
49 | 48 | sneqd 4490 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
50 | | snriota 7014 |
. . . . . 6
⊢
(∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) → {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
51 | 40, 50 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {𝑧 ∈ ℕ0
∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
52 | 49, 51 | eqtr4d 2836 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))}) |
53 | 52 | eleq2d 2870 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 ∈ {(𝑁 mod 𝐷)} ↔ 𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) |
54 | 6, 53 | syl5bb 284 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ 𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) |
55 | | breq1 4971 |
. . . 4
⊢ (𝑧 = 𝑅 → (𝑧 < 𝐷 ↔ 𝑅 < 𝐷)) |
56 | | oveq2 7031 |
. . . . 5
⊢ (𝑧 = 𝑅 → (𝑁 − 𝑧) = (𝑁 − 𝑅)) |
57 | 56 | breq2d 4980 |
. . . 4
⊢ (𝑧 = 𝑅 → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − 𝑅))) |
58 | 55, 57 | anbi12d 630 |
. . 3
⊢ (𝑧 = 𝑅 → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) |
59 | 58 | elrab 3621 |
. 2
⊢ (𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) |
60 | 54, 59 | syl6bb 288 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))) |