Theorem divalgmodcl

Description: The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor. Variant of divalgmod . (Contributed by Stefan O'Rear, 17-Oct-2014) (Proof shortened by AV, 21-Aug-2021)

	Ref	Expression
Assertion	divalgmodcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		divalgmod	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) ) )
2	1	baibd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
3	2	3impa	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )