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

Metamath Proof Explorer

Theorem nnehalf

Description: The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021)

Ref Expression
Assertion nnehalf ⊢ N ∈ ℕ ∧ 2 ∥ N → N 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
2 nn0ehalf ⊢ N ∈ ℕ 0 ∧ 2 ∥ N → N 2 ∈ ℕ 0
3 1 2 sylan ⊢ N ∈ ℕ ∧ 2 ∥ N → N 2 ∈ ℕ 0
4 nn0enne ⊢ N ∈ ℕ → N 2 ∈ ℕ 0 ↔ N 2 ∈ ℕ
5 4 adantr ⊢ N ∈ ℕ ∧ 2 ∥ N → N 2 ∈ ℕ 0 ↔ N 2 ∈ ℕ
6 3 5 mpbid ⊢ N ∈ ℕ ∧ 2 ∥ N → N 2 ∈ ℕ