Theorem acongsym

Description: Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014)

	Ref	Expression
Assertion	acongsym	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		congsym	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∥ ( 𝐶 − 𝐵 ) )
2	1	exp32	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐶 ∈ ℤ → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) → 𝐴 ∥ ( 𝐶 − 𝐵 ) ) ) )
3	2	3impia	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) → 𝐴 ∥ ( 𝐶 − 𝐵 ) ) )
4		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
5	4	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℂ )
6	5	negnegd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → - - 𝐵 = 𝐵 )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( - - 𝐵 − - 𝐶 ) = ( 𝐵 − - 𝐶 ) )
8	4	negcld	⊢ ( 𝐵 ∈ ℤ → - 𝐵 ∈ ℂ )
9	8	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → - 𝐵 ∈ ℂ )
10		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
11	10	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
12	9 11	neg2subd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( - - 𝐵 − - 𝐶 ) = ( 𝐶 − - 𝐵 ) )
13	7 12	eqtr3d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − - 𝐶 ) = ( 𝐶 − - 𝐵 ) )
14	13	breq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ↔ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )
15	14	biimpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) → 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )
16	3 15	orim12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) )
17	16	imp	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )