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 ⊢ N ∈ ℕ 0 ∧ 2 ∥ N → N 2 ∈ ℕ 0

Proof

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