Theorem nneom

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

	Ref	Expression
Assertion	nneom	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )

Proof

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