Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℤ ) |
2 |
|
nnne0 |
⊢ ( 𝐷 ∈ ℕ → 𝐷 ≠ 0 ) |
3 |
1 2
|
jca |
⊢ ( 𝐷 ∈ ℕ → ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) ) |
4 |
|
divalg |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) |
5 |
|
divalgb |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) |
6 |
4 5
|
mpbid |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) |
7 |
6
|
3expb |
⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) |
8 |
3 7
|
sylan2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) |
9 |
|
nnre |
⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ ) |
10 |
|
nnnn0 |
⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℕ0 ) |
11 |
10
|
nn0ge0d |
⊢ ( 𝐷 ∈ ℕ → 0 ≤ 𝐷 ) |
12 |
9 11
|
absidd |
⊢ ( 𝐷 ∈ ℕ → ( abs ‘ 𝐷 ) = 𝐷 ) |
13 |
12
|
breq2d |
⊢ ( 𝐷 ∈ ℕ → ( 𝑟 < ( abs ‘ 𝐷 ) ↔ 𝑟 < 𝐷 ) ) |
14 |
13
|
anbi1d |
⊢ ( 𝐷 ∈ ℕ → ( ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) |
15 |
14
|
reubidv |
⊢ ( 𝐷 ∈ ℕ → ( ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) |
16 |
15
|
adantl |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) |
17 |
8 16
|
mpbid |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) |