Metamath Proof Explorer

Theorem nneop

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

Ref Expression
Assertion nneop ⊢ N ∈ ℕ → N 2 ∈ ℕ ∨ N + 1 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nneo ⊢ N ∈ ℕ → N 2 ∈ ℕ ↔ ¬ N + 1 2 ∈ ℕ
2 1 biimprd ⊢ N ∈ ℕ → ¬ N + 1 2 ∈ ℕ → N 2 ∈ ℕ
3 2 orrd ⊢ N ∈ ℕ → N + 1 2 ∈ ℕ ∨ N 2 ∈ ℕ
4 3 orcomd ⊢ N ∈ ℕ → N 2 ∈ ℕ ∨ N + 1 2 ∈ ℕ