Proof of Theorem divalgb
| Step | Hyp | Ref
| Expression |
| 1 | | df-3an 1089 |
. . . . . . . . 9
⊢ ((0 ≤
𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 2 | 1 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑞 ∈
ℤ (0 ≤ 𝑟 ∧
𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃𝑞 ∈ ℤ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 3 | | r19.42v 3191 |
. . . . . . . 8
⊢
(∃𝑞 ∈
ℤ ((0 ≤ 𝑟 ∧
𝑟 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 4 | 2, 3 | bitri 275 |
. . . . . . 7
⊢
(∃𝑞 ∈
ℤ (0 ≤ 𝑟 ∧
𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 5 | | zsubcl 12659 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝑁 − 𝑟) ∈ ℤ) |
| 6 | | divides 16292 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ ℤ ∧ (𝑁 − 𝑟) ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟))) |
| 7 | 5, 6 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ)) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟))) |
| 8 | 7 | 3impb 1115 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟))) |
| 9 | 8 | 3com12 1124 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟))) |
| 10 | | zcn 12618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 11 | | zcn 12618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℤ → 𝑟 ∈
ℂ) |
| 12 | | zmulcl 12666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 · 𝐷) ∈ ℤ) |
| 13 | 12 | zcnd 12723 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 · 𝐷) ∈ ℂ) |
| 14 | | subadd 11511 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℂ ∧ 𝑟 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ (𝑟 + (𝑞 · 𝐷)) = 𝑁)) |
| 15 | 10, 11, 13, 14 | syl3an 1161 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ (𝑟 + (𝑞 · 𝐷)) = 𝑁)) |
| 16 | | addcom 11447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → (𝑟 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑟)) |
| 17 | 11, 13, 16 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (𝑟 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑟)) |
| 18 | 17 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (𝑟 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑟)) |
| 19 | 18 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑟 + (𝑞 · 𝐷)) = 𝑁 ↔ ((𝑞 · 𝐷) + 𝑟) = 𝑁)) |
| 20 | 15, 19 | bitrd 279 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ ((𝑞 · 𝐷) + 𝑟) = 𝑁)) |
| 21 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ (𝑞 · 𝐷) = (𝑁 − 𝑟)) |
| 22 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑞 · 𝐷) + 𝑟) = 𝑁 ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) |
| 23 | 20, 21, 22 | 3bitr3g 313 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 24 | 23 | 3expia 1122 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
| 25 | 24 | expcomd 416 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∈ ℤ → (𝑞 ∈ ℤ → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))))) |
| 26 | 25 | 3impia 1118 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 ∈ ℤ → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
| 27 | 26 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ 𝑞 ∈ ℤ) → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 28 | 27 | rexbidva 3177 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ) →
(∃𝑞 ∈ ℤ
(𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 29 | 28 | 3com23 1127 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) →
(∃𝑞 ∈ ℤ
(𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 30 | 9, 29 | bitrd 279 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
| 31 | 30 | anbi2d 630 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (((0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
| 32 | 4, 31 | bitr4id 290 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) →
(∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
| 33 | | anass 468 |
. . . . . 6
⊢ (((0 ≤
𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
| 34 | 32, 33 | bitrdi 287 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) →
(∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 35 | 34 | 3expa 1119 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ 𝑟 ∈ ℤ) →
(∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 36 | 35 | reubidva 3396 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) →
(∃!𝑟 ∈ ℤ
∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℤ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 37 | | elnn0z 12626 |
. . . . . . 7
⊢ (𝑟 ∈ ℕ0
↔ (𝑟 ∈ ℤ
∧ 0 ≤ 𝑟)) |
| 38 | 37 | anbi1i 624 |
. . . . . 6
⊢ ((𝑟 ∈ ℕ0
∧ (𝑟 <
(abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ((𝑟 ∈ ℤ ∧ 0 ≤ 𝑟) ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
| 39 | | anass 468 |
. . . . . 6
⊢ (((𝑟 ∈ ℤ ∧ 0 ≤
𝑟) ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ (𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 40 | 38, 39 | bitri 275 |
. . . . 5
⊢ ((𝑟 ∈ ℕ0
∧ (𝑟 <
(abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ (𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 41 | 40 | eubii 2585 |
. . . 4
⊢
(∃!𝑟(𝑟 ∈ ℕ0
∧ (𝑟 <
(abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ∃!𝑟(𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 42 | | df-reu 3381 |
. . . 4
⊢
(∃!𝑟 ∈
ℕ0 (𝑟 <
(abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ ∃!𝑟(𝑟 ∈ ℕ0 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
| 43 | | df-reu 3381 |
. . . 4
⊢
(∃!𝑟 ∈
ℤ (0 ≤ 𝑟 ∧
(𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ∃!𝑟(𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))) |
| 44 | 41, 42, 43 | 3bitr4ri 304 |
. . 3
⊢
(∃!𝑟 ∈
ℤ (0 ≤ 𝑟 ∧
(𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) |
| 45 | 36, 44 | bitrdi 287 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) →
(∃!𝑟 ∈ ℤ
∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
| 46 | 45 | 3adant3 1133 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |