Theorem modadd12d

Description: Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	modadd12d.1	$$⊢\phi \to A\in ℝ$$
	modadd12d.2	$$⊢\phi \to B\in ℝ$$
	modadd12d.3	$$⊢\phi \to C\in ℝ$$
	modadd12d.4	$$⊢\phi \to D\in ℝ$$
	modadd12d.5	$$⊢\phi \to E\in {ℝ}^{+}$$
	modadd12d.6	$$⊢\phi \to A\mathrm{mod}E=B\mathrm{mod}E$$
	modadd12d.7	$$⊢\phi \to C\mathrm{mod}E=D\mathrm{mod}E$$
Assertion	modadd12d	$$⊢\phi \to \left(A+C\right)\mathrm{mod}E=\left(B+D\right)\mathrm{mod}E$$

Proof

Step	Hyp	Ref	Expression
1		modadd12d.1	$$⊢\phi \to A\in ℝ$$
2		modadd12d.2	$$⊢\phi \to B\in ℝ$$
3		modadd12d.3	$$⊢\phi \to C\in ℝ$$
4		modadd12d.4	$$⊢\phi \to D\in ℝ$$
5		modadd12d.5	$$⊢\phi \to E\in {ℝ}^{+}$$
6		modadd12d.6	$$⊢\phi \to A\mathrm{mod}E=B\mathrm{mod}E$$
7		modadd12d.7	$$⊢\phi \to C\mathrm{mod}E=D\mathrm{mod}E$$
8		modadd1	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(C\in ℝ\wedge E\in {ℝ}^{+}\right)\wedge A\mathrm{mod}E=B\mathrm{mod}E\right)\to \left(A+C\right)\mathrm{mod}E=\left(B+C\right)\mathrm{mod}E$$
9	1 2 3 5 6 8	syl221anc	$$⊢\phi \to \left(A+C\right)\mathrm{mod}E=\left(B+C\right)\mathrm{mod}E$$
10	2	recnd	$$⊢\phi \to B\in ℂ$$
11	3	recnd	$$⊢\phi \to C\in ℂ$$
12	10 11	addcomd	$$⊢\phi \to B+C=C+B$$
13	12	oveq1d	$$⊢\phi \to \left(B+C\right)\mathrm{mod}E=\left(C+B\right)\mathrm{mod}E$$
14		modadd1	$$⊢\left(\left(C\in ℝ\wedge D\in ℝ\right)\wedge \left(B\in ℝ\wedge E\in {ℝ}^{+}\right)\wedge C\mathrm{mod}E=D\mathrm{mod}E\right)\to \left(C+B\right)\mathrm{mod}E=\left(D+B\right)\mathrm{mod}E$$
15	3 4 2 5 7 14	syl221anc	$$⊢\phi \to \left(C+B\right)\mathrm{mod}E=\left(D+B\right)\mathrm{mod}E$$
16	4	recnd	$$⊢\phi \to D\in ℂ$$
17	16 10	addcomd	$$⊢\phi \to D+B=B+D$$
18	17	oveq1d	$$⊢\phi \to \left(D+B\right)\mathrm{mod}E=\left(B+D\right)\mathrm{mod}E$$
19	13 15 18	3eqtrd	$$⊢\phi \to \left(B+C\right)\mathrm{mod}E=\left(B+D\right)\mathrm{mod}E$$
20	9 19	eqtrd	$$⊢\phi \to \left(A+C\right)\mathrm{mod}E=\left(B+D\right)\mathrm{mod}E$$