Metamath Proof Explorer

Theorem elmod2

Description: An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020) (Proof shortened by OpenAI, 3-Jul-2020)

Ref Expression
Assertion elmod2 ⊢ N ∈ ℤ → N mod 2 ∈ 0 1

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 zmodfzo ⊢ N ∈ ℤ ∧ 2 ∈ ℕ → N mod 2 ∈ 0 ..^ 2
3 2 ancoms ⊢ 2 ∈ ℕ ∧ N ∈ ℤ → N mod 2 ∈ 0 ..^ 2
4 1 3 mpan ⊢ N ∈ ℤ → N mod 2 ∈ 0 ..^ 2
5 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
6 4 5 eleqtrdi ⊢ N ∈ ℤ → N mod 2 ∈ 0 1