modabs2

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

Step	Hyp	Ref	Expression
1		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
2	1	leidd	$⊢ B \in ℝ^{+} \to B \leq B$
3	2	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \leq B$
4		modabs	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land B \in ℝ^{+}) \land B \leq B) \to (A \mod B) \mod B = A \mod B$
5	4	ex	$⊢ (A \in ℝ \land B \in ℝ^{+} \land B \in ℝ^{+}) \to (B \leq B \to (A \mod B) \mod B = A \mod B)$
6	5	3anidm23	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (B \leq B \to (A \mod B) \mod B = A \mod B)$
7	3 6	mpd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B) \mod B = A \mod B$

Metamath Proof Explorer