| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | divalglem8.1 | . . . 4
⊢ 𝑁 ∈ ℤ | 
| 2 |  | divalglem8.2 | . . . 4
⊢ 𝐷 ∈ ℤ | 
| 3 |  | divalglem8.3 | . . . 4
⊢ 𝐷 ≠ 0 | 
| 4 |  | divalglem8.4 | . . . 4
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} | 
| 5 |  | eqid 2737 | . . . 4
⊢ inf(𝑆, ℝ, < ) = inf(𝑆, ℝ, <
) | 
| 6 | 1, 2, 3, 4, 5 | divalglem9 16438 | . . 3
⊢
∃!𝑥 ∈
𝑆 𝑥 < (abs‘𝐷) | 
| 7 |  | elnn0z 12626 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0
↔ (𝑥 ∈ ℤ
∧ 0 ≤ 𝑥)) | 
| 8 | 7 | anbi2i 623 | . . . . . . . . 9
⊢ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ↔ (𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥))) | 
| 9 |  | an12 645 | . . . . . . . . . 10
⊢ ((𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥)) ↔ (𝑥 ∈ ℤ ∧ (𝑥 < (abs‘𝐷) ∧ 0 ≤ 𝑥))) | 
| 10 |  | ancom 460 | . . . . . . . . . . 11
⊢ ((𝑥 < (abs‘𝐷) ∧ 0 ≤ 𝑥) ↔ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷))) | 
| 11 | 10 | anbi2i 623 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ (𝑥 < (abs‘𝐷) ∧ 0 ≤ 𝑥)) ↔ (𝑥 ∈ ℤ ∧ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)))) | 
| 12 | 9, 11 | bitri 275 | . . . . . . . . 9
⊢ ((𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥)) ↔ (𝑥 ∈ ℤ ∧ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)))) | 
| 13 | 8, 12 | bitri 275 | . . . . . . . 8
⊢ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ↔ (𝑥 ∈ ℤ ∧ (0 ≤
𝑥 ∧ 𝑥 < (abs‘𝐷)))) | 
| 14 | 13 | anbi1i 624 | . . . . . . 7
⊢ (((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((𝑥 ∈ ℤ ∧ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷))) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 15 |  | anass 468 | . . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ (0 ≤
𝑥 ∧ 𝑥 < (abs‘𝐷))) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (𝑥 ∈ ℤ ∧ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 16 | 14, 15 | bitri 275 | . . . . . 6
⊢ (((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (𝑥 ∈ ℤ ∧ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 17 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑥 → ((𝑞 · 𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑥)) | 
| 18 | 17 | eqeq2d 2748 | . . . . . . . . . 10
⊢ (𝑟 = 𝑥 → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 19 | 18 | rexbidv 3179 | . . . . . . . . 9
⊢ (𝑟 = 𝑥 → (∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 20 | 1, 2, 3, 4 | divalglem4 16433 | . . . . . . . . 9
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑟)} | 
| 21 | 19, 20 | elrab2 3695 | . . . . . . . 8
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 22 | 21 | anbi2i 623 | . . . . . . 7
⊢ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ 𝑆) ↔ (𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 23 |  | ancom 460 | . . . . . . 7
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ (𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ 𝑆)) | 
| 24 |  | anass 468 | . . . . . . 7
⊢ (((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 25 | 22, 23, 24 | 3bitr4i 303 | . . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 26 |  | df-3an 1089 | . . . . . . . . 9
⊢ ((0 ≤
𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 27 | 26 | rexbii 3094 | . . . . . . . 8
⊢
(∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃𝑞 ∈ ℤ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 28 |  | r19.42v 3191 | . . . . . . . 8
⊢
(∃𝑞 ∈
ℤ ((0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 29 | 27, 28 | bitri 275 | . . . . . . 7
⊢
(∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 30 | 29 | anbi2i 623 | . . . . . 6
⊢ ((𝑥 ∈ ℤ ∧
∃𝑞 ∈ ℤ (0
≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) ↔ (𝑥 ∈ ℤ ∧ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 31 | 16, 25, 30 | 3bitr4i 303 | . . . . 5
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ (𝑥 ∈ ℤ ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 32 | 31 | eubii 2585 | . . . 4
⊢
(∃!𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ ∃!𝑥(𝑥 ∈ ℤ ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 33 |  | df-reu 3381 | . . . 4
⊢
(∃!𝑥 ∈
𝑆 𝑥 < (abs‘𝐷) ↔ ∃!𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷))) | 
| 34 |  | df-reu 3381 | . . . 4
⊢
(∃!𝑥 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃!𝑥(𝑥 ∈ ℤ ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) | 
| 35 | 32, 33, 34 | 3bitr4i 303 | . . 3
⊢
(∃!𝑥 ∈
𝑆 𝑥 < (abs‘𝐷) ↔ ∃!𝑥 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) | 
| 36 | 6, 35 | mpbi 230 | . 2
⊢
∃!𝑥 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) | 
| 37 |  | breq2 5147 | . . . . 5
⊢ (𝑥 = 𝑟 → (0 ≤ 𝑥 ↔ 0 ≤ 𝑟)) | 
| 38 |  | breq1 5146 | . . . . 5
⊢ (𝑥 = 𝑟 → (𝑥 < (abs‘𝐷) ↔ 𝑟 < (abs‘𝐷))) | 
| 39 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = 𝑟 → ((𝑞 · 𝐷) + 𝑥) = ((𝑞 · 𝐷) + 𝑟)) | 
| 40 | 39 | eqeq2d 2748 | . . . . 5
⊢ (𝑥 = 𝑟 → (𝑁 = ((𝑞 · 𝐷) + 𝑥) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | 
| 41 | 37, 38, 40 | 3anbi123d 1438 | . . . 4
⊢ (𝑥 = 𝑟 → ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) | 
| 42 | 41 | rexbidv 3179 | . . 3
⊢ (𝑥 = 𝑟 → (∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) | 
| 43 | 42 | cbvreuvw 3404 | . 2
⊢
(∃!𝑥 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | 
| 44 | 36, 43 | mpbi 230 | 1
⊢
∃!𝑟 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑟 ∧
𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) |