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

Proof

Step	Hyp	Ref	Expression
1		1oddALTV	⊢ 1 ∈ Odd
2		1z	⊢ 1 ∈ ℤ
3		zeo2ALTV	⊢ ( 1 ∈ ℤ → ( 1 ∈ Even ↔ ¬ 1 ∈ Odd ) )
4	2 3	ax-mp	⊢ ( 1 ∈ Even ↔ ¬ 1 ∈ Odd )
5	4	con2bii	⊢ ( 1 ∈ Odd ↔ ¬ 1 ∈ Even )
6		df-nel	⊢ ( 1 ∉ Even ↔ ¬ 1 ∈ Even )
7	5 6	bitr4i	⊢ ( 1 ∈ Odd ↔ 1 ∉ Even )
8	1 7	mpbi	⊢ 1 ∉ Even