Metamath Proof Explorer

Theorem congsym

Description: Congruence mod A is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 simprr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ B − C
2 zcn ⊢ C ∈ ℤ → C ∈ ℂ
3 2 ad2antrl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → C ∈ ℂ
4 zcn ⊢ B ∈ ℤ → B ∈ ℂ
5 4 ad2antlr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → B ∈ ℂ
6 3 5 negsubdi2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → − C − B = B − C
7 1 6 breqtrrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ − C − B
8 simpll ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∈ ℤ
9 simprl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → C ∈ ℤ
10 simplr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → B ∈ ℤ
11 9 10 zsubcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → C − B ∈ ℤ
12 dvdsnegb ⊢ A ∈ ℤ ∧ C − B ∈ ℤ → A ∥ C − B ↔ A ∥ − C − B
13 8 11 12 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ C − B ↔ A ∥ − C − B
14 7 13 mpbird ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → A ∥ C − B