This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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