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 ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ( ( 𝑁 ↑ 2 ) / 2 ) ∈ ℕ ) )

Proof

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