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	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - - 𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
3	2	negnegd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → - - 𝐶 = 𝐶 )
4	3	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − - - 𝐶 ) = ( 𝐵 − 𝐶 ) )
5	4	breq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − - - 𝐶 ) ↔ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) )
6	5	biimpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − - - 𝐶 ) → 𝐴 ∥ ( 𝐵 − 𝐶 ) ) )
7	6	orim2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - - 𝐶 ) ) → ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) )
8	7	imp	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - - 𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) )
9	8	orcomd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - - 𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) )