Metamath Proof Explorer

Theorem modadd12d

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

Ref Expression
Hypotheses modadd12d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
modadd12d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
modadd12d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
modadd12d.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
modadd12d.5 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
modadd12d.6 ⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) )
modadd12d.7 ⊢ ( 𝜑 → ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) )
Assertion modadd12d ( 𝜑 → ( ( 𝐴 + 𝐶 ) mod 𝐸 ) = ( ( 𝐵 + 𝐷 ) mod 𝐸 ) )

Proof

Step Hyp Ref Expression
1 modadd12d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 modadd12d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 modadd12d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 modadd12d.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 modadd12d.5 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6 modadd12d.6 ⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) )
7 modadd12d.7 ⊢ ( 𝜑 → ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) )
8 modadd1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐸 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) ) → ( ( 𝐴 + 𝐶 ) mod 𝐸 ) = ( ( 𝐵 + 𝐶 ) mod 𝐸 ) )
9 1 2 3 5 6 8 syl221anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) mod 𝐸 ) = ( ( 𝐵 + 𝐶 ) mod 𝐸 ) )
10 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
11 3 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
12 10 11 addcomd ⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) = ( 𝐶 + 𝐵 ) )
13 12 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) mod 𝐸 ) = ( ( 𝐶 + 𝐵 ) mod 𝐸 ) )
14 modadd1 ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐸 ∈ ℝ+ ) ∧ ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) ) → ( ( 𝐶 + 𝐵 ) mod 𝐸 ) = ( ( 𝐷 + 𝐵 ) mod 𝐸 ) )
15 3 4 2 5 7 14 syl221anc ⊢ ( 𝜑 → ( ( 𝐶 + 𝐵 ) mod 𝐸 ) = ( ( 𝐷 + 𝐵 ) mod 𝐸 ) )
16 4 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
17 16 10 addcomd ⊢ ( 𝜑 → ( 𝐷 + 𝐵 ) = ( 𝐵 + 𝐷 ) )
18 17 oveq1d ⊢ ( 𝜑 → ( ( 𝐷 + 𝐵 ) mod 𝐸 ) = ( ( 𝐵 + 𝐷 ) mod 𝐸 ) )
19 13 15 18 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) mod 𝐸 ) = ( ( 𝐵 + 𝐷 ) mod 𝐸 ) )
20 9 19 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) mod 𝐸 ) = ( ( 𝐵 + 𝐷 ) mod 𝐸 ) )