| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovex 7464 | . . . . . 6
⊢ (𝑁 mod 𝐷) ∈ V | 
| 2 | 1 | snid 4662 | . . . . 5
⊢ (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)} | 
| 3 |  | eleq1 2829 | . . . . 5
⊢ (𝑅 = (𝑁 mod 𝐷) → (𝑅 ∈ {(𝑁 mod 𝐷)} ↔ (𝑁 mod 𝐷) ∈ {(𝑁 mod 𝐷)})) | 
| 4 | 2, 3 | mpbiri 258 | . . . 4
⊢ (𝑅 = (𝑁 mod 𝐷) → 𝑅 ∈ {(𝑁 mod 𝐷)}) | 
| 5 |  | elsni 4643 | . . . 4
⊢ (𝑅 ∈ {(𝑁 mod 𝐷)} → 𝑅 = (𝑁 mod 𝐷)) | 
| 6 | 4, 5 | impbii 209 | . . 3
⊢ (𝑅 = (𝑁 mod 𝐷) ↔ 𝑅 ∈ {(𝑁 mod 𝐷)}) | 
| 7 |  | zre 12617 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 8 |  | nnrp 13046 | . . . . . . . . 9
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ+) | 
| 9 |  | modlt 13920 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝑁 mod 𝐷) < 𝐷) | 
| 10 | 7, 8, 9 | syl2an 596 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) < 𝐷) | 
| 11 |  | nnre 12273 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ) | 
| 12 |  | nnne0 12300 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ≠ 0) | 
| 13 |  | redivcl 11986 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0) → (𝑁 / 𝐷) ∈ ℝ) | 
| 14 | 7, 11, 12, 13 | syl3an 1161 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℝ) | 
| 15 | 14 | 3anidm23 1423 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℝ) | 
| 16 | 15 | flcld 13838 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℤ) | 
| 17 |  | nnz 12634 | . . . . . . . . . 10
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℤ) | 
| 18 | 17 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℤ) | 
| 19 |  | zmodcl 13931 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈
ℕ0) | 
| 20 | 19 | nn0zd 12639 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℤ) | 
| 21 |  | zsubcl 12659 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 𝐷) ∈ ℤ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) | 
| 22 | 20, 21 | syldan 591 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) | 
| 23 |  | nncn 12274 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℂ) | 
| 24 | 23 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℂ) | 
| 25 | 16 | zcnd 12723 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℂ) | 
| 26 | 24, 25 | mulcomd 11282 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = ((⌊‘(𝑁 / 𝐷)) · 𝐷)) | 
| 27 |  | modval 13911 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) | 
| 28 | 7, 8, 27 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷))))) | 
| 29 | 19 | nn0cnd 12589 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℂ) | 
| 30 |  | zmulcl 12666 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ ℤ ∧
(⌊‘(𝑁 / 𝐷)) ∈ ℤ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) | 
| 31 | 17, 16, 30 | syl2an2 686 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℤ) | 
| 32 | 31 | zcnd 12723 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) ∈ ℂ) | 
| 33 |  | zcn 12618 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℂ) | 
| 35 | 29, 32, 34 | subexsub 11681 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 mod 𝐷) = (𝑁 − (𝐷 · (⌊‘(𝑁 / 𝐷)))) ↔ (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷)))) | 
| 36 | 28, 35 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 · (⌊‘(𝑁 / 𝐷))) = (𝑁 − (𝑁 mod 𝐷))) | 
| 37 | 26, 36 | eqtr3d 2779 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) | 
| 38 |  | dvds0lem 16304 | . . . . . . . . 9
⊢
((((⌊‘(𝑁
/ 𝐷)) ∈ ℤ ∧
𝐷 ∈ ℤ ∧
(𝑁 − (𝑁 mod 𝐷)) ∈ ℤ) ∧
((⌊‘(𝑁 / 𝐷)) · 𝐷) = (𝑁 − (𝑁 mod 𝐷))) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) | 
| 39 | 16, 18, 22, 37, 38 | syl31anc 1375 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) | 
| 40 |  | divalg2 16442 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) | 
| 41 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑧 < 𝐷 ↔ (𝑁 mod 𝐷) < 𝐷)) | 
| 42 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝑁 − 𝑧) = (𝑁 − (𝑁 mod 𝐷))) | 
| 43 | 42 | breq2d 5155 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑁 mod 𝐷) → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷)))) | 
| 44 | 41, 43 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = (𝑁 mod 𝐷) → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ ((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))))) | 
| 45 | 44 | riota2 7413 | . . . . . . . . 9
⊢ (((𝑁 mod 𝐷) ∈ ℕ0 ∧
∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) | 
| 46 | 19, 40, 45 | syl2anc 584 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (((𝑁 mod 𝐷) < 𝐷 ∧ 𝐷 ∥ (𝑁 − (𝑁 mod 𝐷))) ↔ (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷))) | 
| 47 | 10, 39, 46 | mpbi2and 712 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(℩𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))) = (𝑁 mod 𝐷)) | 
| 48 | 47 | eqcomd 2743 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))) | 
| 49 | 48 | sneqd 4638 | . . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) | 
| 50 |  | snriota 7421 | . . . . . 6
⊢
(∃!𝑧 ∈
ℕ0 (𝑧 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) → {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) | 
| 51 | 40, 50 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {𝑧 ∈ ℕ0
∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} = {(℩𝑧 ∈ ℕ0 (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)))}) | 
| 52 | 49, 51 | eqtr4d 2780 | . . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → {(𝑁 mod 𝐷)} = {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))}) | 
| 53 | 52 | eleq2d 2827 | . . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 ∈ {(𝑁 mod 𝐷)} ↔ 𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) | 
| 54 | 6, 53 | bitrid 283 | . 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ 𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))})) | 
| 55 |  | breq1 5146 | . . . 4
⊢ (𝑧 = 𝑅 → (𝑧 < 𝐷 ↔ 𝑅 < 𝐷)) | 
| 56 |  | oveq2 7439 | . . . . 5
⊢ (𝑧 = 𝑅 → (𝑁 − 𝑧) = (𝑁 − 𝑅)) | 
| 57 | 56 | breq2d 5155 | . . . 4
⊢ (𝑧 = 𝑅 → (𝐷 ∥ (𝑁 − 𝑧) ↔ 𝐷 ∥ (𝑁 − 𝑅))) | 
| 58 | 55, 57 | anbi12d 632 | . . 3
⊢ (𝑧 = 𝑅 → ((𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧)) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | 
| 59 | 58 | elrab 3692 | . 2
⊢ (𝑅 ∈ {𝑧 ∈ ℕ0 ∣ (𝑧 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑧))} ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | 
| 60 | 54, 59 | bitrdi 287 | 1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))) |