Theorem nneop

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

	Ref	Expression
Assertion	nneop	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )

Proof

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