Metamath Proof Explorer

Theorem acongsym

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

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

Proof

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