Metamath Proof Explorer


Theorem zneoALTV

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. (Contributed by NM, 31-Jul-2004) (Revised by AV, 16-Jun-2020)

Ref Expression
Assertion zneoALTV ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 oddneven ( 𝐵 ∈ Odd → ¬ 𝐵 ∈ Even )
2 nelne2 ( ( 𝐴 ∈ Even ∧ ¬ 𝐵 ∈ Even ) → 𝐴𝐵 )
3 1 2 sylan2 ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → 𝐴𝐵 )