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
|- ( ( A e. Even /\ B e. Odd ) -> A =/= B )

Proof

Step Hyp Ref Expression
1 oddneven
 |-  ( B e. Odd -> -. B e. Even )
2 nelne2
 |-  ( ( A e. Even /\ -. B e. Even ) -> A =/= B )
3 1 2 sylan2
 |-  ( ( A e. Even /\ B e. Odd ) -> A =/= B )