Metamath Proof Explorer

Theorem nn0enne

Description: A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nn0enne ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( 𝑁 / 2 ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( 𝑁 / 2 ) = 0 ) )
2 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
3 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
4 2ne0 ⊢ 2 ≠ 0
5 4 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
6 2 3 5 diveq0ad ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) = 0 ↔ 𝑁 = 0 ) )
7 eleq1 ⊢ ( 𝑁 = 0 → ( 𝑁 ∈ ℕ ↔ 0 ∈ ℕ ) )
8 0nnn ⊢ ¬ 0 ∈ ℕ
9 8 pm2.21i ⊢ ( 0 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ )
10 7 9 biimtrdi ⊢ ( 𝑁 = 0 → ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) )
11 10 com12 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 0 → ( 𝑁 / 2 ) ∈ ℕ ) )
12 6 11 sylbid ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) = 0 → ( 𝑁 / 2 ) ∈ ℕ ) )
13 12 com12 ⊢ ( ( 𝑁 / 2 ) = 0 → ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) )
14 13 jao1i ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( 𝑁 / 2 ) = 0 ) → ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) )
15 1 14 sylbi ⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) )
16 15 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ0 → ( 𝑁 / 2 ) ∈ ℕ ) )
17 nnnn0 ⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ0 )
18 16 17 impbid1 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( 𝑁 / 2 ) ∈ ℕ ) )