This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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