Metamath Proof Explorer

Theorem nnesq

Description: A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion nnesq ⊢ N ∈ ℕ → N 2 ∈ ℕ ↔ N 2 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnz ⊢ N ∈ ℕ → N ∈ ℤ
2 zesq ⊢ N ∈ ℤ → N 2 ∈ ℤ ↔ N 2 2 ∈ ℤ
3 1 2 syl ⊢ N ∈ ℕ → N 2 ∈ ℤ ↔ N 2 2 ∈ ℤ
4 nnrp ⊢ N ∈ ℕ → N ∈ ℝ +
5 4 rphalfcld ⊢ N ∈ ℕ → N 2 ∈ ℝ +
6 5 rpgt0d ⊢ N ∈ ℕ → 0 < N 2
7 nnsqcl ⊢ N ∈ ℕ → N 2 ∈ ℕ
8 7 nnrpd ⊢ N ∈ ℕ → N 2 ∈ ℝ +
9 8 rphalfcld ⊢ N ∈ ℕ → N 2 2 ∈ ℝ +
10 9 rpgt0d ⊢ N ∈ ℕ → 0 < N 2 2
11 6 10 2thd ⊢ N ∈ ℕ → 0 < N 2 ↔ 0 < N 2 2
12 3 11 anbi12d ⊢ N ∈ ℕ → N 2 ∈ ℤ ∧ 0 < N 2 ↔ N 2 2 ∈ ℤ ∧ 0 < N 2 2
13 elnnz ⊢ N 2 ∈ ℕ ↔ N 2 ∈ ℤ ∧ 0 < N 2
14 elnnz ⊢ N 2 2 ∈ ℕ ↔ N 2 2 ∈ ℤ ∧ 0 < N 2 2
15 12 13 14 3bitr4g ⊢ N ∈ ℕ → N 2 ∈ ℕ ↔ N 2 2 ∈ ℕ