Theorem acongid

Description: A wff like that in this theorem will be known as an "alternating congruence". A special symbol might be considered if more uses come up. They have many of the same properties as normal congruences, starting with reflexivity.

JonesMatijasevic uses "a ≡ ± b (mod c)" for this construction. The disjunction of divisibility constraints seems to adequately capture the concept, but it's rather verbose and somewhat inelegant. Use of an explicit equivalence relation might also work. (Contributed by Stefan O'Rear, 2-Oct-2014)

	Ref	Expression
Assertion	acongid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		congid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐵 − 𝐵 ) )
2	1	orcd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐵 ) ) )