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 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 ) )