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 ∉ Odd

Proof

Step	Hyp	Ref	Expression
1		0evenALTV	⊢ 0 ∈ Even
2		df-nel	⊢ ( 0 ∉ Odd ↔ ¬ 0 ∈ Odd )
3		0z	⊢ 0 ∈ ℤ
4		zeo2ALTV	⊢ ( 0 ∈ ℤ → ( 0 ∈ Even ↔ ¬ 0 ∈ Odd ) )
5	4	bicomd	⊢ ( 0 ∈ ℤ → ( ¬ 0 ∈ Odd ↔ 0 ∈ Even ) )
6	3 5	ax-mp	⊢ ( ¬ 0 ∈ Odd ↔ 0 ∈ Even )
7	2 6	bitri	⊢ ( 0 ∉ Odd ↔ 0 ∈ Even )
8	1 7	mpbir	⊢ 0 ∉ Odd