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