Metamath Proof Explorer

Theorem 1nevenALTV

Description: 1 is not an even number. (Contributed by AV, 12-Feb-2020) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion 1nevenALTV 
|- 1 e/ Even

Proof

Step Hyp Ref Expression
1 1oddALTV 
 |-  1 e. Odd
2 1z 
 |-  1 e. ZZ
3 zeo2ALTV 
 |-  ( 1 e. ZZ -> ( 1 e. Even <-> -. 1 e. Odd ) )
4 2 3 ax-mp 
 |-  ( 1 e. Even <-> -. 1 e. Odd )
5 4 con2bii 
 |-  ( 1 e. Odd <-> -. 1 e. Even )
6 df-nel 
 |-  ( 1 e/ Even <-> -. 1 e. Even )
7 5 6 bitr4i 
 |-  ( 1 e. Odd <-> 1 e/ Even )
8 1 7 mpbi 
 |-  1 e/ Even