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

Proof

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