Step | Hyp | Ref
| Expression |
1 | | simpl1 995 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → 𝑁 ∈ ℤ) |
2 | | simpl2 996 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → 𝐷 ∈ ℤ) |
3 | 2 | znegcld 9323 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → -𝐷 ∈ ℤ) |
4 | | simpr 109 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → 𝐷 < 0) |
5 | 2 | zred 9321 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → 𝐷 ∈ ℝ) |
6 | 5 | lt0neg1d 8421 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → (𝐷 < 0 ↔ 0 < -𝐷)) |
7 | 4, 6 | mpbid 146 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → 0 < -𝐷) |
8 | | elnnz 9209 |
. . . . 5
⊢ (-𝐷 ∈ ℕ ↔ (-𝐷 ∈ ℤ ∧ 0 <
-𝐷)) |
9 | 3, 7, 8 | sylanbrc 415 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → -𝐷 ∈ ℕ) |
10 | | divalglemnn 11864 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ -𝐷 ∈ ℕ) →
∃𝑟 ∈ ℤ
∃𝑘 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) |
11 | 1, 9, 10 | syl2anc 409 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → ∃𝑟 ∈ ℤ ∃𝑘 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) |
12 | | simplr 525 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝑘 ∈ ℤ) |
13 | 12 | znegcld 9323 |
. . . . . . 7
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → -𝑘 ∈ ℤ) |
14 | | simpr1 998 |
. . . . . . 7
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 0 ≤ 𝑟) |
15 | | simpr2 999 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝑟 < (abs‘-𝐷)) |
16 | | simpll2 1032 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) → 𝐷 ∈ ℤ) |
17 | 16 | ad2antrr 485 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝐷 ∈ ℤ) |
18 | 17 | zcnd 9322 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝐷 ∈ ℂ) |
19 | 18 | absnegd 11140 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → (abs‘-𝐷) = (abs‘𝐷)) |
20 | 15, 19 | breqtrd 4013 |
. . . . . . 7
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝑟 < (abs‘𝐷)) |
21 | | simpr3 1000 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝑁 = ((𝑘 · -𝐷) + 𝑟)) |
22 | 12 | zcnd 9322 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝑘 ∈ ℂ) |
23 | | mulneg12 8303 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (-𝑘 · 𝐷) = (𝑘 · -𝐷)) |
24 | 22, 18, 23 | syl2anc 409 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → (-𝑘 · 𝐷) = (𝑘 · -𝐷)) |
25 | 24 | oveq1d 5865 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → ((-𝑘 · 𝐷) + 𝑟) = ((𝑘 · -𝐷) + 𝑟)) |
26 | 21, 25 | eqtr4d 2206 |
. . . . . . 7
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → 𝑁 = ((-𝑘 · 𝐷) + 𝑟)) |
27 | | oveq1 5857 |
. . . . . . . . . . 11
⊢ (𝑞 = -𝑘 → (𝑞 · 𝐷) = (-𝑘 · 𝐷)) |
28 | 27 | oveq1d 5865 |
. . . . . . . . . 10
⊢ (𝑞 = -𝑘 → ((𝑞 · 𝐷) + 𝑟) = ((-𝑘 · 𝐷) + 𝑟)) |
29 | 28 | eqeq2d 2182 |
. . . . . . . . 9
⊢ (𝑞 = -𝑘 → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((-𝑘 · 𝐷) + 𝑟))) |
30 | 29 | 3anbi3d 1313 |
. . . . . . . 8
⊢ (𝑞 = -𝑘 → ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((-𝑘 · 𝐷) + 𝑟)))) |
31 | 30 | rspcev 2834 |
. . . . . . 7
⊢ ((-𝑘 ∈ ℤ ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((-𝑘 · 𝐷) + 𝑟))) → ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
32 | 13, 14, 20, 26, 31 | syl13anc 1235 |
. . . . . 6
⊢
((((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟))) → ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
33 | 32 | ex 114 |
. . . . 5
⊢
(((((𝑁 ∈
ℤ ∧ 𝐷 ∈
ℤ ∧ 𝐷 ≠ 0)
∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((0 ≤
𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟)) → ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
34 | 33 | rexlimdva 2587 |
. . . 4
⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) ∧ 𝑟 ∈ ℤ) → (∃𝑘 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟)) → ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
35 | 34 | reximdva 2572 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → (∃𝑟 ∈ ℤ ∃𝑘 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘-𝐷) ∧ 𝑁 = ((𝑘 · -𝐷) + 𝑟)) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))) |
36 | 11, 35 | mpd 13 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 < 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
37 | | simpr 109 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 = 0) → 𝐷 = 0) |
38 | | simpl3 997 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 = 0) → 𝐷 ≠ 0) |
39 | 37, 38 | pm2.21ddne 2423 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 𝐷 = 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
40 | | simpl1 995 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 0 < 𝐷) → 𝑁 ∈ ℤ) |
41 | | simpl2 996 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 0 < 𝐷) → 𝐷 ∈ ℤ) |
42 | | simpr 109 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 0 < 𝐷) → 0 < 𝐷) |
43 | | elnnz 9209 |
. . . 4
⊢ (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℤ ∧ 0 <
𝐷)) |
44 | 41, 42, 43 | sylanbrc 415 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 0 < 𝐷) → 𝐷 ∈ ℕ) |
45 | | divalglemnn 11864 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃𝑟 ∈ ℤ
∃𝑞 ∈ ℤ (0
≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
46 | 40, 44, 45 | syl2anc 409 |
. 2
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) ∧ 0 < 𝐷) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
47 | | ztri3or0 9241 |
. . 3
⊢ (𝐷 ∈ ℤ → (𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷)) |
48 | 47 | 3ad2ant2 1014 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷)) |
49 | 36, 39, 46, 48 | mpjao3dan 1302 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |