modge0

Description: The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008)

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

Step	Hyp	Ref	Expression
1		fldivle	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \leq \frac{A}{B}$
2		refldivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℝ$
3		simpl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \in ℝ$
4		rpregt0	$⊢ B \in ℝ^{+} \to (B \in ℝ \land 0 < B)$
5	4	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (B \in ℝ \land 0 < B)$
6		lemuldiv2	$⊢ (⌊\frac{A}{B}⌋ \in ℝ \land A \in ℝ \land (B \in ℝ \land 0 < B)) \to (B ⌊\frac{A}{B}⌋ \leq A \leftrightarrow ⌊\frac{A}{B}⌋ \leq \frac{A}{B})$
7	2 3 5 6	syl3anc	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (B ⌊\frac{A}{B}⌋ \leq A \leftrightarrow ⌊\frac{A}{B}⌋ \leq \frac{A}{B})$
8	1 7	mpbird	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \leq A$
9		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
10	9	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℝ$
11	10 2	remulcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \in ℝ$
12		subge0	$⊢ (A \in ℝ \land B ⌊\frac{A}{B}⌋ \in ℝ) \to (0 \leq A - B ⌊\frac{A}{B}⌋ \leftrightarrow B ⌊\frac{A}{B}⌋ \leq A)$
13	11 12	syldan	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (0 \leq A - B ⌊\frac{A}{B}⌋ \leftrightarrow B ⌊\frac{A}{B}⌋ \leq A)$
14	8 13	mpbird	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to 0 \leq A - B ⌊\frac{A}{B}⌋$
15		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
16	14 15	breqtrrd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to 0 \leq A \mod B$

Metamath Proof Explorer