Metamath Proof Explorer

Theorem nneom

Description: A positive integer is even or odd. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nneom ⊢ N ∈ ℕ → N 2 ∈ ℕ ∨ N − 1 2 ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 nneop ⊢ N ∈ ℕ → N 2 ∈ ℕ ∨ N + 1 2 ∈ ℕ
2 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
3 nnnn0 ⊢ N + 1 2 ∈ ℕ → N + 1 2 ∈ ℕ 0
4 nn0o ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℕ 0 → N − 1 2 ∈ ℕ 0
5 2 3 4 syl2an ⊢ N ∈ ℕ ∧ N + 1 2 ∈ ℕ → N − 1 2 ∈ ℕ 0
6 5 ex ⊢ N ∈ ℕ → N + 1 2 ∈ ℕ → N − 1 2 ∈ ℕ 0
7 6 orim2d ⊢ N ∈ ℕ → N 2 ∈ ℕ ∨ N + 1 2 ∈ ℕ → N 2 ∈ ℕ ∨ N − 1 2 ∈ ℕ 0
8 1 7 mpd ⊢ N ∈ ℕ → N 2 ∈ ℕ ∨ N − 1 2 ∈ ℕ 0