Theorem zeneo

Description: No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of Apostol p. 28. This variant of zneo follows immediately from the fact that a contradiction implies anything, see pm2.21i . (Contributed by AV, 22-Jun-2021)

	Ref	Expression
Assertion	zeneo	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 𝐴 ≠ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nbrne1	⊢ ( ( 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 𝐴 ≠ 𝐵 )
2	1	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 𝐴 ≠ 𝐵 ) )