Step | Hyp | Ref
| Expression |
1 | | divalglem8.1 |
. . . 4
⊢ 𝑁 ∈ ℤ |
2 | | divalglem8.2 |
. . . 4
⊢ 𝐷 ∈ ℤ |
3 | | divalglem8.3 |
. . . 4
⊢ 𝐷 ≠ 0 |
4 | | divalglem8.4 |
. . . 4
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} |
5 | | eqid 2739 |
. . . 4
⊢ inf(𝑆, ℝ, < ) = inf(𝑆, ℝ, <
) |
6 | 1, 2, 3, 4, 5 | divalglem9 15858 |
. . 3
⊢
∃!𝑥 ∈
𝑆 𝑥 < (abs‘𝐷) |
7 | | elnn0z 12087 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0
↔ (𝑥 ∈ ℤ
∧ 0 ≤ 𝑥)) |
8 | 7 | anbi2i 626 |
. . . . . . . . 9
⊢ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ↔ (𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥))) |
9 | | an12 645 |
. . . . . . . . . 10
⊢ ((𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥)) ↔ (𝑥 ∈ ℤ ∧ (𝑥 < (abs‘𝐷) ∧ 0 ≤ 𝑥))) |
10 | | ancom 464 |
. . . . . . . . . . 11
⊢ ((𝑥 < (abs‘𝐷) ∧ 0 ≤ 𝑥) ↔ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷))) |
11 | 10 | anbi2i 626 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ (𝑥 < (abs‘𝐷) ∧ 0 ≤ 𝑥)) ↔ (𝑥 ∈ ℤ ∧ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)))) |
12 | 9, 11 | bitri 278 |
. . . . . . . . 9
⊢ ((𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℤ ∧ 0 ≤ 𝑥)) ↔ (𝑥 ∈ ℤ ∧ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)))) |
13 | 8, 12 | bitri 278 |
. . . . . . . 8
⊢ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ↔ (𝑥 ∈ ℤ ∧ (0 ≤
𝑥 ∧ 𝑥 < (abs‘𝐷)))) |
14 | 13 | anbi1i 627 |
. . . . . . 7
⊢ (((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((𝑥 ∈ ℤ ∧ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷))) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
15 | | anass 472 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ (0 ≤
𝑥 ∧ 𝑥 < (abs‘𝐷))) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (𝑥 ∈ ℤ ∧ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
16 | 14, 15 | bitri 278 |
. . . . . 6
⊢ (((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (𝑥 ∈ ℤ ∧ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
17 | | oveq2 7190 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑥 → ((𝑞 · 𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑥)) |
18 | 17 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑥 → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
19 | 18 | rexbidv 3208 |
. . . . . . . . 9
⊢ (𝑟 = 𝑥 → (∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
20 | 1, 2, 3, 4 | divalglem4 15853 |
. . . . . . . . 9
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑟)} |
21 | 19, 20 | elrab2 3596 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
22 | 21 | anbi2i 626 |
. . . . . . 7
⊢ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ 𝑆) ↔ (𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
23 | | ancom 464 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ (𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ 𝑆)) |
24 | | anass 472 |
. . . . . . 7
⊢ (((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (𝑥 < (abs‘𝐷) ∧ (𝑥 ∈ ℕ0 ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
25 | 22, 23, 24 | 3bitr4i 306 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ ((𝑥 < (abs‘𝐷) ∧ 𝑥 ∈ ℕ0) ∧
∃𝑞 ∈ ℤ
𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
26 | | df-3an 1090 |
. . . . . . . . 9
⊢ ((0 ≤
𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
27 | 26 | rexbii 3162 |
. . . . . . . 8
⊢
(∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃𝑞 ∈ ℤ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
28 | | r19.42v 3255 |
. . . . . . . 8
⊢
(∃𝑞 ∈
ℤ ((0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
29 | 27, 28 | bitri 278 |
. . . . . . 7
⊢
(∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
30 | 29 | anbi2i 626 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧
∃𝑞 ∈ ℤ (0
≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) ↔ (𝑥 ∈ ℤ ∧ ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
31 | 16, 25, 30 | 3bitr4i 306 |
. . . . 5
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ (𝑥 ∈ ℤ ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
32 | 31 | eubii 2587 |
. . . 4
⊢
(∃!𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷)) ↔ ∃!𝑥(𝑥 ∈ ℤ ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
33 | | df-reu 3061 |
. . . 4
⊢
(∃!𝑥 ∈
𝑆 𝑥 < (abs‘𝐷) ↔ ∃!𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 < (abs‘𝐷))) |
34 | | df-reu 3061 |
. . . 4
⊢
(∃!𝑥 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃!𝑥(𝑥 ∈ ℤ ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)))) |
35 | 32, 33, 34 | 3bitr4i 306 |
. . 3
⊢
(∃!𝑥 ∈
𝑆 𝑥 < (abs‘𝐷) ↔ ∃!𝑥 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥))) |
36 | 6, 35 | mpbi 233 |
. 2
⊢
∃!𝑥 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) |
37 | | breq2 5044 |
. . . . 5
⊢ (𝑥 = 𝑟 → (0 ≤ 𝑥 ↔ 0 ≤ 𝑟)) |
38 | | breq1 5043 |
. . . . 5
⊢ (𝑥 = 𝑟 → (𝑥 < (abs‘𝐷) ↔ 𝑟 < (abs‘𝐷))) |
39 | | oveq2 7190 |
. . . . . 6
⊢ (𝑥 = 𝑟 → ((𝑞 · 𝐷) + 𝑥) = ((𝑞 · 𝐷) + 𝑟)) |
40 | 39 | eqeq2d 2750 |
. . . . 5
⊢ (𝑥 = 𝑟 → (𝑁 = ((𝑞 · 𝐷) + 𝑥) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
41 | 37, 38, 40 | 3anbi123d 1437 |
. . . 4
⊢ (𝑥 = 𝑟 → ((0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
42 | 41 | rexbidv 3208 |
. . 3
⊢ (𝑥 = 𝑟 → (∃𝑞 ∈ ℤ (0 ≤ 𝑥 ∧ 𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
43 | 42 | cbvreuvw 3353 |
. 2
⊢
(∃!𝑥 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑥 ∧
𝑥 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑥)) ↔ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
44 | 36, 43 | mpbi 233 |
1
⊢
∃!𝑟 ∈
ℤ ∃𝑞 ∈
ℤ (0 ≤ 𝑟 ∧
𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) |