Theorem moddifz

Description: The modulo operation differs from A by an integer multiple of B . (Contributed by Mario Carneiro, 15-Jul-2014)

	Ref	Expression
Assertion	moddifz	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A-\left(A\mathrm{mod}B\right)}{B}\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		moddiffl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A-\left(A\mathrm{mod}B\right)}{B}=⌊\frac{A}{B}⌋$$
2		rerpdivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$
3	2	flcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in \mathbb{Z}$$
4	1 3	eqeltrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A-\left(A\mathrm{mod}B\right)}{B}\in \mathbb{Z}$$