Step | Hyp | Ref
| Expression |
1 | | zq 9585 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℚ) |
2 | 1 | adantr 274 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℚ) |
3 | | nnq 9592 |
. . . . . . . 8
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℚ) |
4 | 3 | adantl 275 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℚ) |
5 | | simpr 109 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℕ) |
6 | 5 | nngt0d 8922 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 0 <
𝐷) |
7 | 2, 4, 6 | modqcld 10284 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℚ) |
8 | | snidg 3612 |
. . . . . 6
⊢ ((𝑁 mod 𝐷) ∈ ℚ → (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)}) |
9 | 7, 8 | syl 14 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)}) |
10 | | eleq1 2233 |
. . . . 5
⊢ (𝑅 = (𝑁 mod 𝐷) → (𝑅 ∈ {(𝑁 mod 𝐷)} ↔ (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)})) |
11 | 9, 10 | syl5ibrcom 156 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) → 𝑅 ∈ {(𝑁 mod 𝐷)})) |
12 | | elsni 3601 |
. . . 4
⊢ (𝑅 ∈ {(𝑁 mod 𝐷)} → 𝑅 = (𝑁 mod 𝐷)) |
13 | 11, 12 | impbid1 141 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ 𝑅 ∈ {(𝑁 mod 𝐷)})) |
14 | | modqlt 10289 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 0 <
𝐷) → (𝑁 mod 𝐷) < 𝐷) |
15 | 2, 4, 6, 14 | syl3anc 1233 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) < 𝐷) |
16 | | znq 9583 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℚ) |
17 | 16 | flqcld 10233 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℤ) |
18 | | nnz 9231 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℤ) |
19 | 18 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℤ) |
20 | | zmodcl 10300 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈
ℕ0) |
21 | 20 | nn0zd 9332 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℤ) |
22 | | zsubcl 9253 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 𝐷) ∈ ℤ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) |
23 | 21, 22 | syldan 280 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) |
24 | | nncn 8886 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℂ) |
25 | 24 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℂ) |
26 | 17 | zcnd 9335 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℂ) |
27 | 25, 26 | mulcomd 7941 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = ((⌊‘(𝑁 / 𝐷)) · 𝐷)) |
28 | | modqval 10280 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 0 <
𝐷) → (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
29 | 2, 4, 6, 28 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) |
30 | 20 | nn0cnd 9190 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℂ) |
31 | | zmulcl 9265 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ ℤ ∧
(⌊‘(𝑁 / 𝐷)) ∈ ℤ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
32 | 18, 17, 31 | syl2an2 589 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) |
33 | 32 | zcnd 9335 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℂ) |
34 | | zcn 9217 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
35 | 34 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℂ) |
36 | 30, 33, 35 | subexsub 8291 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) ↔ (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷)))) |
37 | 29, 36 | mpbid 146 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷))) |
38 | 27, 37 | eqtr3d 2205 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) |
39 | | dvds0lem 11763 |
. . . . . . . . 9
⊢
((((⌊‘(𝑁
/ 𝐷)) ∈ ℤ ∧
𝐷 ∈ ℤ ∧
(𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) ∧
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) |
40 | 17, 19, 23, 38, 39 | syl31anc 1236 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) |
41 | | divalg2 11885 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) |
42 | | breq1 3992 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑧 < 𝐷 ↔ (𝑁 mod 𝐷) < 𝐷)) |
43 | | oveq2 5861 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑁 − 𝑧) = (𝑁 − (𝑁 mod 𝐷))) |
44 | 43 | breq2d 4001 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷)))) |
45 | 42, 44 | anbi12d 470 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑁 mod 𝐷) → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ ((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))))) |
46 | 45 | riota2 5831 |
. . . . . . . . 9
⊢ (((𝑁 mod 𝐷) ∈ ℕ0 ∧
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) |
47 | 20, 41, 46 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) |
48 | 15, 40, 47 | mpbi2and 938 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(℩𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷)) |
49 | 48 | eqcomd 2176 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))) |
50 | 49 | sneqd 3596 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
51 | | snriota 5838 |
. . . . . 6
⊢
(∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) → {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
52 | 41, 51 | syl 14 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {𝑧 ∈ ℕ0
∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) |
53 | 50, 52 | eqtr4d 2206 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))}) |
54 | 53 | eleq2d 2240 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 ∈ {(𝑁 mod 𝐷)} ↔ 𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) |
55 | 13, 54 | bitrd 187 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ 𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) |
56 | | breq1 3992 |
. . . 4
⊢ (𝑧 = 𝑅 → (𝑧 < 𝐷 ↔ 𝑅 < 𝐷)) |
57 | | oveq2 5861 |
. . . . 5
⊢ (𝑧 = 𝑅 → (𝑁 − 𝑧) = (𝑁 − 𝑅)) |
58 | 57 | breq2d 4001 |
. . . 4
⊢ (𝑧 = 𝑅 → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − 𝑅))) |
59 | 56, 58 | anbi12d 470 |
. . 3
⊢ (𝑧 = 𝑅 → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) |
60 | 59 | elrab 2886 |
. 2
⊢ (𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) |
61 | 55, 60 | bitrdi 195 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))) |