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