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