Theorem modvalp1

Description: The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Alexander van der Vekens, 14-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2	1	adantr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℂ$$
3		refldivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in ℝ$$
4	3	recnd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋\in ℂ$$
5		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
6	5	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℂ$$
7	4 6	mulcld	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to ⌊\frac{A}{B}⌋B\in ℂ$$
8	2 7 6	pnpcan2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A+B-\left(⌊\frac{A}{B}⌋B+B\right)=A-⌊\frac{A}{B}⌋B$$
9	4 6	adddirp1d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(⌊\frac{A}{B}⌋+1\right)B=⌊\frac{A}{B}⌋B+B$$
10	9	oveq2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A+B-\left(⌊\frac{A}{B}⌋+1\right)B=A+B-\left(⌊\frac{A}{B}⌋B+B\right)$$
11		modvalr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\mathrm{mod}B=A-⌊\frac{A}{B}⌋B$$
12	8 10 11	3eqtr4d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A+B-\left(⌊\frac{A}{B}⌋+1\right)B=A\mathrm{mod}B$$