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

Proof

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