Theorem modvalr

Description: The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018)

	Ref	Expression
Assertion	modvalr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B=A-⌊\frac{A}{B}⌋B$$

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		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
3	2	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℂ$$
4		rerpdivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$
5		reflcl	$$⊢\frac{A}{B}\in ℝ\to ⌊\frac{A}{B}⌋\in ℝ$$
6	5	recnd	$$⊢\frac{A}{B}\in ℝ\to ⌊\frac{A}{B}⌋\in ℂ$$
7	4 6	syl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in ℂ$$
8	3 7	mulcomd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B⌊\frac{A}{B}⌋=⌊\frac{A}{B}⌋B$$
9	8	oveq2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-B⌊\frac{A}{B}⌋=A-⌊\frac{A}{B}⌋B$$
10	1 9	eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B=A-⌊\frac{A}{B}⌋B$$