Metamath Proof Explorer


Theorem divalg2

Description: The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion divalg2 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) )

Proof

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 ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) )