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 e/ Odd

Proof

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