Metamath Proof Explorer

Theorem 0noddALTV

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

Ref Expression
Assertion 0noddALTV 
|- 0 e/ Odd

Proof

Step Hyp Ref Expression
1 0evenALTV 
 |-  0 e. Even
2 df-nel 
 |-  ( 0 e/ Odd <-> -. 0 e. Odd )
3 0z 
 |-  0 e. ZZ
4 zeo2ALTV 
 |-  ( 0 e. ZZ -> ( 0 e. Even <-> -. 0 e. Odd ) )
5 4 bicomd 
 |-  ( 0 e. ZZ -> ( -. 0 e. Odd <-> 0 e. Even ) )
6 3 5 ax-mp 
 |-  ( -. 0 e. Odd <-> 0 e. Even )
7 2 6 bitri 
 |-  ( 0 e/ Odd <-> 0 e. Even )
8 1 7 mpbir 
 |-  0 e/ Odd