# Metamath Proof Explorer

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}$