Theorem nn0ehalf

Description: The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020) (Revised by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Assertion	nn0ehalf	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∥ 𝑁 ) → ( 𝑁 / 2 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
2		evend2	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ∥ 𝑁 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
4		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
5		2rp	⊢ 2 ∈ ℝ+
6	5	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ+ )
7		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
8	4 6 7	divge0d	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( 𝑁 / 2 ) )
9	8	anim1ci	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 / 2 ) ) )
10		elnn0z	⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 / 2 ) ) )
11	9 10	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( 𝑁 / 2 ) ∈ ℕ0 )
12	11	ex	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 / 2 ) ∈ ℤ → ( 𝑁 / 2 ) ∈ ℕ0 ) )
13	3 12	sylbid	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ∥ 𝑁 → ( 𝑁 / 2 ) ∈ ℕ0 ) )
14	13	imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∥ 𝑁 ) → ( 𝑁 / 2 ) ∈ ℕ0 )