This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem modadd12d

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

Ref Expression
Hypotheses modadd12d.1 ⊢ φ → A ∈ ℝ
modadd12d.2 ⊢ φ → B ∈ ℝ
modadd12d.3 ⊢ φ → C ∈ ℝ
modadd12d.4 ⊢ φ → D ∈ ℝ
modadd12d.5 ⊢ φ → E ∈ ℝ +
modadd12d.6 ⊢ φ → A mod E = B mod E
modadd12d.7 ⊢ φ → C mod E = D mod E
Assertion modadd12d ⊢ φ → A + C mod E = B + D mod E

Proof

Step Hyp Ref Expression
1 modadd12d.1 ⊢ φ → A ∈ ℝ
2 modadd12d.2 ⊢ φ → B ∈ ℝ
3 modadd12d.3 ⊢ φ → C ∈ ℝ
4 modadd12d.4 ⊢ φ → D ∈ ℝ
5 modadd12d.5 ⊢ φ → E ∈ ℝ +
6 modadd12d.6 ⊢ φ → A mod E = B mod E
7 modadd12d.7 ⊢ φ → C mod E = D mod E
8 modadd1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ E ∈ ℝ + ∧ A mod E = B mod E → A + C mod E = B + C mod E
9 1 2 3 5 6 8 syl221anc ⊢ φ → A + C mod E = B + C mod E
10 2 recnd ⊢ φ → B ∈ ℂ
11 3 recnd ⊢ φ → C ∈ ℂ
12 10 11 addcomd ⊢ φ → B + C = C + B
13 12 oveq1d ⊢ φ → B + C mod E = C + B mod E
14 modadd1 ⊢ C ∈ ℝ ∧ D ∈ ℝ ∧ B ∈ ℝ ∧ E ∈ ℝ + ∧ C mod E = D mod E → C + B mod E = D + B mod E
15 3 4 2 5 7 14 syl221anc ⊢ φ → C + B mod E = D + B mod E
16 4 recnd ⊢ φ → D ∈ ℂ
17 16 10 addcomd ⊢ φ → D + B = B + D
18 17 oveq1d ⊢ φ → D + B mod E = B + D mod E
19 13 15 18 3eqtrd ⊢ φ → B + C mod E = B + D mod E
20 9 19 eqtrd ⊢ φ → A + C mod E = B + D mod E