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

Step	Hyp	Ref	Expression
1		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
2		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
3	2	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℂ$
4		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \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	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℂ$
8	3 7	mulcomd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ = ⌊\frac{A}{B}⌋ B$
9	8	oveq2d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A - B ⌊\frac{A}{B}⌋ = A - ⌊\frac{A}{B}⌋ B$
10	1 9	eqtrd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - ⌊\frac{A}{B}⌋ B$

Metamath Proof Explorer