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