Metamath Proof Explorer

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