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 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B+D-C+E

Proof

Step Hyp Ref Expression
1 simpl1 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→A∈ℤ
2 zsubcl ⊢B∈ℤ∧C∈ℤ→B−C∈ℤ
3 2 3adant1 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→B−C∈ℤ
4 3 adantr ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→B−C∈ℤ
5 zsubcl ⊢D∈ℤ∧E∈ℤ→D−E∈ℤ
6 5 adantl ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→D−E∈ℤ
7 dvds2add ⊢A∈ℤ∧B−C∈ℤ∧D−E∈ℤ→A∥B−C∧A∥D−E→A∥B−C+D-E
8 1 4 6 7 syl3anc ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→A∥B−C∧A∥D−E→A∥B−C+D-E
9 8 3impia ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B−C+D-E
10 simpl2 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→B∈ℤ
11 10 zcnd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→B∈ℂ
12 zcn ⊢D∈ℤ→D∈ℂ
13 12 ad2antrl ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→D∈ℂ
14 simpl3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→C∈ℤ
15 14 zcnd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→C∈ℂ
16 zcn ⊢E∈ℤ→E∈ℂ
17 16 ad2antll ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→E∈ℂ
18 11 13 15 17 addsub4d ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ→B+D-C+E=B−C+D-E
19 18 3adant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→B+D-C+E=B−C+D-E
20 9 19 breqtrrd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B+D-C+E