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