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\notin \mathrm{Odd}$$

Proof

Step	Hyp	Ref	Expression
1		0evenALTV	$$⊢0\in \mathrm{Even}$$
2		df-nel	$$⊢0\notin \mathrm{Odd}\leftrightarrow \neg 0\in \mathrm{Odd}$$
3		0z	$$⊢0\in \mathbb{Z}$$
4		zeo2ALTV	$$⊢0\in \mathbb{Z}\to \left(0\in \mathrm{Even}\leftrightarrow \neg 0\in \mathrm{Odd}\right)$$
5	4	bicomd	$$⊢0\in \mathbb{Z}\to \left(\neg 0\in \mathrm{Odd}\leftrightarrow 0\in \mathrm{Even}\right)$$
6	3 5	ax-mp	$$⊢\neg 0\in \mathrm{Odd}\leftrightarrow 0\in \mathrm{Even}$$
7	2 6	bitri	$$⊢0\notin \mathrm{Odd}\leftrightarrow 0\in \mathrm{Even}$$
8	1 7	mpbir	$$⊢0\notin \mathrm{Odd}$$