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