# Metamath Proof Explorer

## Theorem acongneg2

Description: Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014)

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

### Proof

Step Hyp Ref Expression
1 zcn ${⊢}{C}\in ℤ\to {C}\in ℂ$
2 1 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {C}\in ℂ$
3 2 negnegd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to -\left(-{C}\right)={C}$
4 3 oveq2d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}-\left(-\left(-{C}\right)\right)={B}-{C}$
5 4 breq2d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\parallel \left({B}-\left(-\left(-{C}\right)\right)\right)↔{A}\parallel \left({B}-{C}\right)\right)$
6 5 biimpd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\parallel \left({B}-\left(-\left(-{C}\right)\right)\right)\to {A}\parallel \left({B}-{C}\right)\right)$
7 6 orim2d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(\left({A}\parallel \left({B}-\left(-{C}\right)\right)\vee {A}\parallel \left({B}-\left(-\left(-{C}\right)\right)\right)\right)\to \left({A}\parallel \left({B}-\left(-{C}\right)\right)\vee {A}\parallel \left({B}-{C}\right)\right)\right)$
8 7 imp ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({A}\parallel \left({B}-\left(-{C}\right)\right)\vee {A}\parallel \left({B}-\left(-\left(-{C}\right)\right)\right)\right)\right)\to \left({A}\parallel \left({B}-\left(-{C}\right)\right)\vee {A}\parallel \left({B}-{C}\right)\right)$
9 8 orcomd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({A}\parallel \left({B}-\left(-{C}\right)\right)\vee {A}\parallel \left({B}-\left(-\left(-{C}\right)\right)\right)\right)\right)\to \left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)$