modabs

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

Proof

Step	Hyp	Ref	Expression
1		modcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$
2	1	anim1i	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to (A \mod B \in ℝ \land C \in ℝ^{+})$
3	2	3impa	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \to (A \mod B \in ℝ \land C \in ℝ^{+})$
4	3	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to (A \mod B \in ℝ \land C \in ℝ^{+})$
5		modge0	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to 0 \leq A \mod B$
6	5	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \to 0 \leq A \mod B$
7	6	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to 0 \leq A \mod B$
8	1	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \to A \mod B \in ℝ$
9	8	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to A \mod B \in ℝ$
10		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
11	10	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \to B \in ℝ$
12	11	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to B \in ℝ$
13		rpre	$⊢ C \in ℝ^{+} \to C \in ℝ$
14	13	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \to C \in ℝ$
15	14	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to C \in ℝ$
16		modlt	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B < B$
17	16	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \to A \mod B < B$
18	17	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to A \mod B < B$
19		simpr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to B \leq C$
20	9 12 15 18 19	ltletrd	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to A \mod B < C$
21		modid	$⊢ ((A \mod B \in ℝ \land C \in ℝ^{+}) \land (0 \leq A \mod B \land A \mod B < C)) \to (A \mod B) \mod C = A \mod B$
22	4 7 20 21	syl12anc	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ^{+}) \land B \leq C) \to (A \mod B) \mod C = A \mod B$

Metamath Proof Explorer

Theorem modabs

Proof