This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )