modcl

Description: Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008)

		Ref	Expression
	Assertion	modcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$

Step	Hyp	Ref	Expression
1		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
2		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
3	2	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℝ$
4		refldivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℝ$
5	3 4	remulcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \in ℝ$
6		resubcl	$⊢ (A \in ℝ \land B ⌊\frac{A}{B}⌋ \in ℝ) \to A - B ⌊\frac{A}{B}⌋ \in ℝ$
7	5 6	syldan	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A - B ⌊\frac{A}{B}⌋ \in ℝ$
8	1 7	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$

Metamath Proof Explorer