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 ⊢ N ∈ ℤ ∧ D ∈ ℕ → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r

Proof

Step Hyp Ref Expression
1 nnz ⊢ D ∈ ℕ → D ∈ ℤ
2 nnne0 ⊢ D ∈ ℕ → D ≠ 0
3 1 2 jca ⊢ D ∈ ℕ → D ∈ ℤ ∧ D ≠ 0
4 divalg ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r
5 divalgb ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r ↔ ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r
6 4 5 mpbid ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r
7 6 3expb ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r
8 3 7 sylan2 ⊢ N ∈ ℤ ∧ D ∈ ℕ → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r
9 nnre ⊢ D ∈ ℕ → D ∈ ℝ
10 nnnn0 ⊢ D ∈ ℕ → D ∈ ℕ 0
11 10 nn0ge0d ⊢ D ∈ ℕ → 0 ≤ D
12 9 11 absidd ⊢ D ∈ ℕ → D = D
13 12 breq2d ⊢ D ∈ ℕ → r < D ↔ r < D
14 13 anbi1d ⊢ D ∈ ℕ → r < D ∧ D ∥ N − r ↔ r < D ∧ D ∥ N − r
15 14 reubidv ⊢ D ∈ ℕ → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r ↔ ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r
16 15 adantl ⊢ N ∈ ℤ ∧ D ∈ ℕ → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r ↔ ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r
17 8 16 mpbid ⊢ N ∈ ℤ ∧ D ∈ ℕ → ∃! r ∈ ℕ 0 r < D ∧ D ∥ N − r