Metamath Proof Explorer

Theorem congneg

Description: If two integers are congruent mod A , so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion congneg ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ - B - − C

Proof

Step Hyp Ref Expression
1 congsym ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ C − B
2 zcn ⊢ B ∈ ℤ → B ∈ ℂ
3 zcn ⊢ C ∈ ℤ → C ∈ ℂ
4 neg2sub ⊢ B ∈ ℂ ∧ C ∈ ℂ → - B - − C = C − B
5 2 3 4 syl2an ⊢ B ∈ ℤ ∧ C ∈ ℤ → - B - − C = C − B
6 5 ad2ant2lr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → - B - − C = C − B
7 1 6 breqtrrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ - B - − C