Metamath Proof Explorer

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