This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A + B - (⌊\frac{A}{B}⌋ + 1) B = A \mod B$

Proof

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