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 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − − C ∨ A ∥ B − − − C → A ∥ B − C ∨ A ∥ B − − C

Proof

Step Hyp Ref Expression
1 zcn ⊢ C ∈ ℤ → C ∈ ℂ
2 1 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → C ∈ ℂ
3 2 negnegd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → − − C = C
4 3 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B − − − C = B − C
5 4 breq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ B − − − C ↔ A ∥ B − C
6 5 biimpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ B − − − C → A ∥ B − C
7 6 orim2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ B − − C ∨ A ∥ B − − − C → A ∥ B − − C ∨ A ∥ B − C
8 7 imp ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − − C ∨ A ∥ B − − − C → A ∥ B − − C ∨ A ∥ B − C
9 8 orcomd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − − C ∨ A ∥ B − − − C → A ∥ B − C ∨ A ∥ B − − C