Description: 2 is not an odd number. (Contributed by AV, 3-Feb-2020) (Revised by AV, 18-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | 2noddALTV |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2evenALTV | ||
2 | df-nel | ||
3 | 2z | ||
4 | zeo2ALTV | ||
5 | 4 | bicomd | |
6 | 3 5 | ax-mp | |
7 | 2 6 | bitri | |
8 | 1 7 | mpbir |