# Metamath Proof Explorer

## Theorem acongsym

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

Ref Expression
Assertion acongsym ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)\to \left({A}\parallel \left({C}-{B}\right)\vee {A}\parallel \left({C}-\left(-{B}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 congsym ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {A}\parallel \left({B}-{C}\right)\right)\right)\to {A}\parallel \left({C}-{B}\right)$
2 1 exp32 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({C}\in ℤ\to \left({A}\parallel \left({B}-{C}\right)\to {A}\parallel \left({C}-{B}\right)\right)\right)$
3 2 3impia ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\parallel \left({B}-{C}\right)\to {A}\parallel \left({C}-{B}\right)\right)$
4 zcn ${⊢}{B}\in ℤ\to {B}\in ℂ$
5 4 3ad2ant2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}\in ℂ$
6 5 negnegd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to -\left(-{B}\right)={B}$
7 6 oveq1d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to -\left(-{B}\right)-\left(-{C}\right)={B}-\left(-{C}\right)$
8 4 negcld ${⊢}{B}\in ℤ\to -{B}\in ℂ$
9 8 3ad2ant2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to -{B}\in ℂ$
10 zcn ${⊢}{C}\in ℤ\to {C}\in ℂ$
11 10 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {C}\in ℂ$
12 9 11 neg2subd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to -\left(-{B}\right)-\left(-{C}\right)={C}-\left(-{B}\right)$
13 7 12 eqtr3d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}-\left(-{C}\right)={C}-\left(-{B}\right)$
14 13 breq2d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\parallel \left({B}-\left(-{C}\right)\right)↔{A}\parallel \left({C}-\left(-{B}\right)\right)\right)$
15 14 biimpd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\parallel \left({B}-\left(-{C}\right)\right)\to {A}\parallel \left({C}-\left(-{B}\right)\right)\right)$
16 3 15 orim12d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(\left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to \left({A}\parallel \left({C}-{B}\right)\vee {A}\parallel \left({C}-\left(-{B}\right)\right)\right)\right)$
17 16 imp ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)\to \left({A}\parallel \left({C}-{B}\right)\vee {A}\parallel \left({C}-\left(-{B}\right)\right)\right)$