modelico

Description: Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014)

		Ref	Expression
	Assertion	modelico	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in [0, B)$

Step	Hyp	Ref	Expression
1		modcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$
2		modge0	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to 0 \leq A \mod B$
3		modlt	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B < B$
4		0re	$⊢ 0 \in ℝ$
5		rpxr	$⊢ B \in ℝ^{+} \to B \in ℝ^{*}$
6	5	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℝ^{*}$
7		elico2	$⊢ (0 \in ℝ \land B \in ℝ^{*}) \to (A \mod B \in [0, B) \leftrightarrow (A \mod B \in ℝ \land 0 \leq A \mod B \land A \mod B < B))$
8	4 6 7	sylancr	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B \in [0, B) \leftrightarrow (A \mod B \in ℝ \land 0 \leq A \mod B \land A \mod B < B))$
9	1 2 3 8	mpbir3and	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in [0, B)$

Metamath Proof Explorer