This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ∥ A ∧ ¬ 2 ∥ B → A ≠ B

Proof

Step Hyp Ref Expression
1 nbrne1 ⊢ 2 ∥ A ∧ ¬ 2 ∥ B → A ≠ B
2 1 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ∥ A ∧ ¬ 2 ∥ B → A ≠ B