Theorem flpmodeq

Description: Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		modvalr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B=A-⌊\frac{A}{B}⌋B$$
2	1	eqcomd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-⌊\frac{A}{B}⌋B=A\mathrm{mod}B$$
3		recn	$$⊢A\in ℝ\to A\in ℂ$$
4	3	adantr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℂ$$
5		rerpdivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$
6		flcl	$$⊢\frac{A}{B}\in ℝ\to ⌊\frac{A}{B}⌋\in \mathbb{Z}$$
7	6	zcnd	$$⊢\frac{A}{B}\in ℝ\to ⌊\frac{A}{B}⌋\in ℂ$$
8	5 7	syl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in ℂ$$
9		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
10	9	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℂ$$
11	8 10	mulcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋B\in ℂ$$
12		modcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B\in ℝ$$
13	12	recnd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B\in ℂ$$
14	4 11 13	subaddd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(A-⌊\frac{A}{B}⌋B=A\mathrm{mod}B\leftrightarrow ⌊\frac{A}{B}⌋B+\left(A\mathrm{mod}B\right)=A\right)$$
15	2 14	mpbid	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋B+\left(A\mathrm{mod}B\right)=A$$