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

Proof

Step	Hyp	Ref	Expression
1		congsym	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∥ ( 𝐶 − 𝐵 ) )
2		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
3		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
4		neg2sub	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( - 𝐵 − - 𝐶 ) = ( 𝐶 − 𝐵 ) )
5	2 3 4	syl2an	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( - 𝐵 − - 𝐶 ) = ( 𝐶 − 𝐵 ) )
6	5	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → ( - 𝐵 − - 𝐶 ) = ( 𝐶 − 𝐵 ) )
7	1 6	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∥ ( - 𝐵 − - 𝐶 ) )