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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 − 𝐷 ) − ( 𝐶 − 𝐸 ) ) )

Proof

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