Proof of Theorem divalglemnn
Step | Hyp | Ref
| Expression |
1 | | zmodcl 9346 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈
ℕ0) |
2 | 1 | nn0zd 8467 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℤ) |
3 | | znq 8709 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 / 𝐷) ∈ ℚ) |
4 | 3 | flqcld 9279 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℤ) |
5 | 1 | nn0ge0d 8344 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 0 ≤
(𝑁 mod 𝐷)) |
6 | | zq 8711 |
. . . . 5
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℚ) |
7 | 6 | adantr 270 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℚ) |
8 | | nnq 8718 |
. . . . 5
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℚ) |
9 | 8 | adantl 271 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℚ) |
10 | | nngt0 8064 |
. . . . 5
⊢ (𝐷 ∈ ℕ → 0 <
𝐷) |
11 | 10 | adantl 271 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 0 <
𝐷) |
12 | | modqlt 9335 |
. . . 4
⊢ ((𝑁 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 0 <
𝐷) → (𝑁 mod 𝐷) < 𝐷) |
13 | 7, 9, 11, 12 | syl3anc 1169 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) < 𝐷) |
14 | | nnre 8046 |
. . . . 5
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ) |
15 | 14 | adantl 271 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℝ) |
16 | | 0red 7120 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 0 ∈
ℝ) |
17 | 16, 15, 11 | ltled 7228 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 0 ≤
𝐷) |
18 | 15, 17 | absidd 10053 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(abs‘𝐷) = 𝐷) |
19 | 13, 18 | breqtrrd 3811 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) < (abs‘𝐷)) |
20 | 1 | nn0cnd 8343 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) ∈ ℂ) |
21 | 4 | zcnd 8470 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(⌊‘(𝑁 / 𝐷)) ∈
ℂ) |
22 | | simpr 108 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℕ) |
23 | 22 | nncnd 8053 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈
ℂ) |
24 | 21, 23 | mulcld 7139 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
((⌊‘(𝑁 / 𝐷)) · 𝐷) ∈ ℂ) |
25 | | modqvalr 9327 |
. . . . . 6
⊢ ((𝑁 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 0 <
𝐷) → (𝑁 mod 𝐷) = (𝑁 − ((⌊‘(𝑁 / 𝐷)) · 𝐷))) |
26 | 7, 9, 11, 25 | syl3anc 1169 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑁 mod 𝐷) = (𝑁 − ((⌊‘(𝑁 / 𝐷)) · 𝐷))) |
27 | 26 | oveq1d 5547 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 mod 𝐷) + ((⌊‘(𝑁 / 𝐷)) · 𝐷)) = ((𝑁 − ((⌊‘(𝑁 / 𝐷)) · 𝐷)) + ((⌊‘(𝑁 / 𝐷)) · 𝐷))) |
28 | | simpl 107 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℤ) |
29 | 28 | zcnd 8470 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 ∈
ℂ) |
30 | 29, 24 | npcand 7423 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 − ((⌊‘(𝑁 / 𝐷)) · 𝐷)) + ((⌊‘(𝑁 / 𝐷)) · 𝐷)) = 𝑁) |
31 | 27, 30 | eqtr2d 2114 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 = ((𝑁 mod 𝐷) + ((⌊‘(𝑁 / 𝐷)) · 𝐷))) |
32 | 20, 24, 31 | comraddd 7265 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → 𝑁 = (((⌊‘(𝑁 / 𝐷)) · 𝐷) + (𝑁 mod 𝐷))) |
33 | | breq2 3789 |
. . . 4
⊢ (𝑟 = (𝑁 mod 𝐷) → (0 ≤ 𝑟 ↔ 0 ≤ (𝑁 mod 𝐷))) |
34 | | breq1 3788 |
. . . 4
⊢ (𝑟 = (𝑁 mod 𝐷) → (𝑟 < (abs‘𝐷) ↔ (𝑁 mod 𝐷) < (abs‘𝐷))) |
35 | | oveq2 5540 |
. . . . 5
⊢ (𝑟 = (𝑁 mod 𝐷) → ((𝑞 · 𝐷) + 𝑟) = ((𝑞 · 𝐷) + (𝑁 mod 𝐷))) |
36 | 35 | eqeq2d 2092 |
. . . 4
⊢ (𝑟 = (𝑁 mod 𝐷) → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + (𝑁 mod 𝐷)))) |
37 | 33, 34, 36 | 3anbi123d 1243 |
. . 3
⊢ (𝑟 = (𝑁 mod 𝐷) → ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ (𝑁 mod 𝐷) ∧ (𝑁 mod 𝐷) < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + (𝑁 mod 𝐷))))) |
38 | | oveq1 5539 |
. . . . . 6
⊢ (𝑞 = (⌊‘(𝑁 / 𝐷)) → (𝑞 · 𝐷) = ((⌊‘(𝑁 / 𝐷)) · 𝐷)) |
39 | 38 | oveq1d 5547 |
. . . . 5
⊢ (𝑞 = (⌊‘(𝑁 / 𝐷)) → ((𝑞 · 𝐷) + (𝑁 mod 𝐷)) = (((⌊‘(𝑁 / 𝐷)) · 𝐷) + (𝑁 mod 𝐷))) |
40 | 39 | eqeq2d 2092 |
. . . 4
⊢ (𝑞 = (⌊‘(𝑁 / 𝐷)) → (𝑁 = ((𝑞 · 𝐷) + (𝑁 mod 𝐷)) ↔ 𝑁 = (((⌊‘(𝑁 / 𝐷)) · 𝐷) + (𝑁 mod 𝐷)))) |
41 | 40 | 3anbi3d 1249 |
. . 3
⊢ (𝑞 = (⌊‘(𝑁 / 𝐷)) → ((0 ≤ (𝑁 mod 𝐷) ∧ (𝑁 mod 𝐷) < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + (𝑁 mod 𝐷))) ↔ (0 ≤ (𝑁 mod 𝐷) ∧ (𝑁 mod 𝐷) < (abs‘𝐷) ∧ 𝑁 = (((⌊‘(𝑁 / 𝐷)) · 𝐷) + (𝑁 mod 𝐷))))) |
42 | 37, 41 | rspc2ev 2715 |
. 2
⊢ (((𝑁 mod 𝐷) ∈ ℤ ∧ (⌊‘(𝑁 / 𝐷)) ∈ ℤ ∧ (0 ≤ (𝑁 mod 𝐷) ∧ (𝑁 mod 𝐷) < (abs‘𝐷) ∧ 𝑁 = (((⌊‘(𝑁 / 𝐷)) · 𝐷) + (𝑁 mod 𝐷)))) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
43 | 2, 4, 5, 19, 32, 42 | syl113anc 1181 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃𝑟 ∈ ℤ
∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |