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 e. NN -> ( ( N / 2 ) e. NN <-> ( ( N ^ 2 ) / 2 ) e. NN ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	|- ( N e. NN -> N e. ZZ )
2		zesq	|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) )
3	1 2	syl	|- ( N e. NN -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) )
4		nnrp	|- ( N e. NN -> N e. RR+ )
5	4	rphalfcld	|- ( N e. NN -> ( N / 2 ) e. RR+ )
6	5	rpgt0d	|- ( N e. NN -> 0 < ( N / 2 ) )
7		nnsqcl	|- ( N e. NN -> ( N ^ 2 ) e. NN )
8	7	nnrpd	|- ( N e. NN -> ( N ^ 2 ) e. RR+ )
9	8	rphalfcld	|- ( N e. NN -> ( ( N ^ 2 ) / 2 ) e. RR+ )
10	9	rpgt0d	|- ( N e. NN -> 0 < ( ( N ^ 2 ) / 2 ) )
11	6 10	2thd	|- ( N e. NN -> ( 0 < ( N / 2 ) <-> 0 < ( ( N ^ 2 ) / 2 ) ) )
12	3 11	anbi12d	|- ( N e. NN -> ( ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) <-> ( ( ( N ^ 2 ) / 2 ) e. ZZ /\ 0 < ( ( N ^ 2 ) / 2 ) ) ) )
13		elnnz	|- ( ( N / 2 ) e. NN <-> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
14		elnnz	|- ( ( ( N ^ 2 ) / 2 ) e. NN <-> ( ( ( N ^ 2 ) / 2 ) e. ZZ /\ 0 < ( ( N ^ 2 ) / 2 ) ) )
15	12 13 14	3bitr4g	|- ( N e. NN -> ( ( N / 2 ) e. NN <-> ( ( N ^ 2 ) / 2 ) e. NN ) )