Metamath Proof Explorer

Theorem congsub

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

Ref Expression
Assertion congsub ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B-D-C−E

Proof

Step Hyp Ref Expression
1 simp11 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∈ℤ
2 simp12 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→B∈ℤ
3 simp13 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→C∈ℤ
4 simp2l ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→D∈ℤ
5 4 znegcld ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→−D∈ℤ
6 simp2r ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→E∈ℤ
7 6 znegcld ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→−E∈ℤ
8 simp3l ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B−C
9 simp3r ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥D−E
10 congneg ⊢A∈ℤ∧D∈ℤ∧E∈ℤ∧A∥D−E→A∥-D-−E
11 1 4 6 9 10 syl22anc ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥-D-−E
12 congadd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧−D∈ℤ∧−E∈ℤ∧A∥B−C∧A∥-D-−E→A∥B+−D-C+−E
13 1 2 3 5 7 8 11 12 syl322anc ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B+−D-C+−E
14 2 zcnd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→B∈ℂ
15 4 zcnd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→D∈ℂ
16 14 15 negsubd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→B+−D=B−D
17 3 zcnd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→C∈ℂ
18 6 zcnd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→E∈ℂ
19 17 18 negsubd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→C+−E=C−E
20 16 19 oveq12d ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→B+−D-C+−E=B-D-C−E
21 13 20 breqtrd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B-D-C−E