Theorem moddiffl

Description: Value of the modulo operation rewritten to give two ways of expressing the quotient when " A is divided by B using Euclidean division." Multiplying both sides by B , this implies that A mod B differs from A by an integer multiple of B . (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 6-Sep-2016)

	Ref	Expression
Assertion	moddiffl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A-\left(A\mathrm{mod}B\right)}{B}=⌊\frac{A}{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	1	oveq2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-\left(A\mathrm{mod}B\right)=A-\left(A-B⌊\frac{A}{B}⌋\right)$$
3		simpl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℝ$$
4	3	recnd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℂ$$
5		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
6	5	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℂ$$
7		rerpdivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$
8	7	flcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in \mathbb{Z}$$
9	8	zcnd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in ℂ$$
10	6 9	mulcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B⌊\frac{A}{B}⌋\in ℂ$$
11	4 10	nncand	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-\left(A-B⌊\frac{A}{B}⌋\right)=B⌊\frac{A}{B}⌋$$
12	2 11	eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-\left(A\mathrm{mod}B\right)=B⌊\frac{A}{B}⌋$$
13	12	oveq1d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A-\left(A\mathrm{mod}B\right)}{B}=\frac{B⌊\frac{A}{B}⌋}{B}$$
14		rpne0	$$⊢B\in {ℝ}^{+}\to B\ne 0$$
15	14	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\ne 0$$
16	9 6 15	divcan3d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{B⌊\frac{A}{B}⌋}{B}=⌊\frac{A}{B}⌋$$
17	13 16	eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A-\left(A\mathrm{mod}B\right)}{B}=⌊\frac{A}{B}⌋$$