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

Proof

Step Hyp Ref Expression
1 simprr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐴 ∥ ( 𝐵𝐶 ) )
2 zcn ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
3 2 ad2antrl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐶 ∈ ℂ )
4 zcn ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
5 4 ad2antlr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐵 ∈ ℂ )
6 3 5 negsubdi2d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → - ( 𝐶𝐵 ) = ( 𝐵𝐶 ) )
7 1 6 breqtrrd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐴 ∥ - ( 𝐶𝐵 ) )
8 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐴 ∈ ℤ )
9 simprl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐶 ∈ ℤ )
10 simplr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐵 ∈ ℤ )
11 9 10 zsubcld ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → ( 𝐶𝐵 ) ∈ ℤ )
12 dvdsnegb ( ( 𝐴 ∈ ℤ ∧ ( 𝐶𝐵 ) ∈ ℤ ) → ( 𝐴 ∥ ( 𝐶𝐵 ) ↔ 𝐴 ∥ - ( 𝐶𝐵 ) ) )
13 8 11 12 syl2anc ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐶𝐵 ) ↔ 𝐴 ∥ - ( 𝐶𝐵 ) ) )
14 7 13 mpbird ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵𝐶 ) ) ) → 𝐴 ∥ ( 𝐶𝐵 ) )