Metamath Proof Explorer


Theorem 2noddALTV

Description: 2 is not an odd number. (Contributed by AV, 3-Feb-2020) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion 2noddALTV 2 Odd

Proof

Step Hyp Ref Expression
1 2evenALTV 2 Even
2 df-nel 2 Odd ¬ 2 Odd
3 2z 2
4 zeo2ALTV 2 2 Even ¬ 2 Odd
5 4 bicomd 2 ¬ 2 Odd 2 Even
6 3 5 ax-mp ¬ 2 Odd 2 Even
7 2 6 bitri 2 Odd 2 Even
8 1 7 mpbir 2 Odd