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∈ℕ0r<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∈ℕ0r<D∧D∥N−r
6 4 5 mpbid ⊢N∈ℤ∧D∈ℤ∧D≠0→∃!r∈ℕ0r<D∧D∥N−r
7 6 3expb ⊢N∈ℤ∧D∈ℤ∧D≠0→∃!r∈ℕ0r<D∧D∥N−r
8 3 7 sylan2 ⊢N∈ℤ∧D∈ℕ→∃!r∈ℕ0r<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∈ℕ0r<D∧D∥N−r↔∃!r∈ℕ0r<D∧D∥N−r
16 15 adantl ⊢N∈ℤ∧D∈ℕ→∃!r∈ℕ0r<D∧D∥N−r↔∃!r∈ℕ0r<D∧D∥N−r
17 8 16 mpbid ⊢N∈ℤ∧D∈ℕ→∃!r∈ℕ0r<D∧D∥N−r