modaddabs

Description: Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		modcl	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to A \mod C \in ℝ$
2	1	recnd	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to A \mod C \in ℂ$
3	2	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A \mod C \in ℂ$
4		modcl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to B \mod C \in ℝ$
5	4	recnd	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to B \mod C \in ℂ$
6	5	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to B \mod C \in ℂ$
7	3 6	addcomd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) + (B \mod C) = (B \mod C) + (A \mod C)$
8	7	oveq1d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ((A \mod C) + (B \mod C)) \mod C = ((B \mod C) + (A \mod C)) \mod C$
9		simpl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to B \in ℝ$
10	4 9	jca	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to (B \mod C \in ℝ \land B \in ℝ)$
11	10	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (B \mod C \in ℝ \land B \in ℝ)$
12		simpr	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to C \in ℝ^{+}$
13	1 12	jca	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to (A \mod C \in ℝ \land C \in ℝ^{+})$
14	13	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C \in ℝ \land C \in ℝ^{+})$
15		modabs2	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to (B \mod C) \mod C = B \mod C$
16	15	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (B \mod C) \mod C = B \mod C$
17		modadd1	$⊢ ((B \mod C \in ℝ \land B \in ℝ) \land (A \mod C \in ℝ \land C \in ℝ^{+}) \land (B \mod C) \mod C = B \mod C) \to ((B \mod C) + (A \mod C)) \mod C = (B + (A \mod C)) \mod C$
18	11 14 16 17	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ((B \mod C) + (A \mod C)) \mod C = (B + (A \mod C)) \mod C$
19		recn	$⊢ B \in ℝ \to B \in ℂ$
20	19	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to B \in ℂ$
21	3 20	addcomd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) + B = B + (A \mod C)$
22	21	oveq1d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ((A \mod C) + B) \mod C = (B + (A \mod C)) \mod C$
23	18 22	eqtr4d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ((B \mod C) + (A \mod C)) \mod C = ((A \mod C) + B) \mod C$
24		simpl	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to A \in ℝ$
25	1 24	jca	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to (A \mod C \in ℝ \land A \in ℝ)$
26	25	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C \in ℝ \land A \in ℝ)$
27		3simpc	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (B \in ℝ \land C \in ℝ^{+})$
28		modabs2	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to (A \mod C) \mod C = A \mod C$
29	28	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) \mod C = A \mod C$
30		modadd1	$⊢ ((A \mod C \in ℝ \land A \in ℝ) \land (B \in ℝ \land C \in ℝ^{+}) \land (A \mod C) \mod C = A \mod C) \to ((A \mod C) + B) \mod C = (A + B) \mod C$
31	26 27 29 30	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ((A \mod C) + B) \mod C = (A + B) \mod C$
32	8 23 31	3eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ((A \mod C) + (B \mod C)) \mod C = (A + B) \mod C$

Metamath Proof Explorer

Theorem modaddabs

Proof