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\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\leftrightarrow \frac{N^2}{2}\in \mathbb{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
2		zesq	$$⊢N\in \mathbb{Z}\to \left(\frac{N}{2}\in \mathbb{Z}\leftrightarrow \frac{N^2}{2}\in \mathbb{Z}\right)$$
3	1 2	syl	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{Z}\leftrightarrow \frac{N^2}{2}\in \mathbb{Z}\right)$$
4		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
5	4	rphalfcld	$$⊢N\in \mathbb{N}\to \frac{N}{2}\in {ℝ}^{+}$$
6	5	rpgt0d	$$⊢N\in \mathbb{N}\to 0<\frac{N}{2}$$
7		nnsqcl	$$⊢N\in \mathbb{N}\to N^2\in \mathbb{N}$$
8	7	nnrpd	$$⊢N\in \mathbb{N}\to N^2\in {ℝ}^{+}$$
9	8	rphalfcld	$$⊢N\in \mathbb{N}\to \frac{N^2}{2}\in {ℝ}^{+}$$
10	9	rpgt0d	$$⊢N\in \mathbb{N}\to 0<\frac{N^2}{2}$$
11	6 10	2thd	$$⊢N\in \mathbb{N}\to \left(0<\frac{N}{2}\leftrightarrow 0<\frac{N^2}{2}\right)$$
12	3 11	anbi12d	$$⊢N\in \mathbb{N}\to \left(\left(\frac{N}{2}\in \mathbb{Z}\wedge 0<\frac{N}{2}\right)\leftrightarrow \left(\frac{N^2}{2}\in \mathbb{Z}\wedge 0<\frac{N^2}{2}\right)\right)$$
13		elnnz	$$⊢\frac{N}{2}\in \mathbb{N}\leftrightarrow \left(\frac{N}{2}\in \mathbb{Z}\wedge 0<\frac{N}{2}\right)$$
14		elnnz	$$⊢\frac{N^2}{2}\in \mathbb{N}\leftrightarrow \left(\frac{N^2}{2}\in \mathbb{Z}\wedge 0<\frac{N^2}{2}\right)$$
15	12 13 14	3bitr4g	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\leftrightarrow \frac{N^2}{2}\in \mathbb{N}\right)$$