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	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\wedge R\in {\mathbb{N}}_0\right)\to \left(R=N\mathrm{mod}D\leftrightarrow \left(R<D\wedge D\parallel \left(N-R\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		divalgmod	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\right)\to \left(R=N\mathrm{mod}D\leftrightarrow \left(R\in {\mathbb{N}}_0\wedge \left(R<D\wedge D\parallel \left(N-R\right)\right)\right)\right)$$
2	1	baibd	$$⊢\left(\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\right)\wedge R\in {\mathbb{N}}_0\right)\to \left(R=N\mathrm{mod}D\leftrightarrow \left(R<D\wedge D\parallel \left(N-R\right)\right)\right)$$
3	2	3impa	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\wedge R\in {\mathbb{N}}_0\right)\to \left(R=N\mathrm{mod}D\leftrightarrow \left(R<D\wedge D\parallel \left(N-R\right)\right)\right)$$