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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵 ) → 𝐴𝐵 ) )

Proof

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