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