Metamath Proof Explorer

Theorem congadd

Description: If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion congadd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 + 𝐷 ) − ( 𝐶 + 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
2 zsubcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
3 2 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
5 zsubcl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( 𝐷 − 𝐸 ) ∈ ℤ )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → ( 𝐷 − 𝐸 ) ∈ ℤ )
7 dvds2add ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ∈ ℤ ∧ ( 𝐷 − 𝐸 ) ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) → 𝐴 ∥ ( ( 𝐵 − 𝐶 ) + ( 𝐷 − 𝐸 ) ) ) )
8 1 4 6 7 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → ( ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) → 𝐴 ∥ ( ( 𝐵 − 𝐶 ) + ( 𝐷 − 𝐸 ) ) ) )
9 8 3impia ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 − 𝐶 ) + ( 𝐷 − 𝐸 ) ) )
10 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
11 10 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
12 zcn ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
13 12 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐷 ∈ ℂ )
14 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐶 ∈ ℤ )
15 14 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐶 ∈ ℂ )
16 zcn ⊢ ( 𝐸 ∈ ℤ → 𝐸 ∈ ℂ )
17 16 ad2antll ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → 𝐸 ∈ ℂ )
18 11 13 15 17 addsub4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ) → ( ( 𝐵 + 𝐷 ) − ( 𝐶 + 𝐸 ) ) = ( ( 𝐵 − 𝐶 ) + ( 𝐷 − 𝐸 ) ) )
19 18 3adant3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( ( 𝐵 + 𝐷 ) − ( 𝐶 + 𝐸 ) ) = ( ( 𝐵 − 𝐶 ) + ( 𝐷 − 𝐸 ) ) )
20 9 19 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 + 𝐷 ) − ( 𝐶 + 𝐸 ) ) )