Theorem modcl

Description: Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008)

	Ref	Expression
Assertion	modcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		modval	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B=A-B⌊\frac{A}{B}⌋$$
2		rpre	$$⊢B\in {ℝ}^{+}\to B\in ℝ$$
3	2	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℝ$$
4		refldivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in ℝ$$
5	3 4	remulcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B⌊\frac{A}{B}⌋\in ℝ$$
6		resubcl	$$⊢\left(A\in ℝ\wedge B⌊\frac{A}{B}⌋\in ℝ\right)\to A-B⌊\frac{A}{B}⌋\in ℝ$$
7	5 6	syldan	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-B⌊\frac{A}{B}⌋\in ℝ$$
8	1 7	eqeltrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B\in ℝ$$