Metamath Proof Explorer


Theorem zesq

Description: An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion zesq
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 zcn
 |-  ( N e. ZZ -> N e. CC )
2 sqval
 |-  ( N e. CC -> ( N ^ 2 ) = ( N x. N ) )
3 1 2 syl
 |-  ( N e. ZZ -> ( N ^ 2 ) = ( N x. N ) )
4 3 oveq1d
 |-  ( N e. ZZ -> ( ( N ^ 2 ) / 2 ) = ( ( N x. N ) / 2 ) )
5 2cnd
 |-  ( N e. ZZ -> 2 e. CC )
6 2ne0
 |-  2 =/= 0
7 6 a1i
 |-  ( N e. ZZ -> 2 =/= 0 )
8 1 1 5 7 divassd
 |-  ( N e. ZZ -> ( ( N x. N ) / 2 ) = ( N x. ( N / 2 ) ) )
9 4 8 eqtrd
 |-  ( N e. ZZ -> ( ( N ^ 2 ) / 2 ) = ( N x. ( N / 2 ) ) )
10 9 adantr
 |-  ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( ( N ^ 2 ) / 2 ) = ( N x. ( N / 2 ) ) )
11 zmulcl
 |-  ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( N x. ( N / 2 ) ) e. ZZ )
12 10 11 eqeltrd
 |-  ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( ( N ^ 2 ) / 2 ) e. ZZ )
13 1 adantr
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> N e. CC )
14 sqcl
 |-  ( N e. CC -> ( N ^ 2 ) e. CC )
15 13 14 syl
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( N ^ 2 ) e. CC )
16 peano2cn
 |-  ( ( N ^ 2 ) e. CC -> ( ( N ^ 2 ) + 1 ) e. CC )
17 15 16 syl
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N ^ 2 ) + 1 ) e. CC )
18 17 halfcld
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N ^ 2 ) + 1 ) / 2 ) e. CC )
19 18 13 pncand
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) - N ) = ( ( ( N ^ 2 ) + 1 ) / 2 ) )
20 binom21
 |-  ( N e. CC -> ( ( N + 1 ) ^ 2 ) = ( ( ( N ^ 2 ) + ( 2 x. N ) ) + 1 ) )
21 13 20 syl
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) ^ 2 ) = ( ( ( N ^ 2 ) + ( 2 x. N ) ) + 1 ) )
22 peano2cn
 |-  ( N e. CC -> ( N + 1 ) e. CC )
23 13 22 syl
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( N + 1 ) e. CC )
24 sqval
 |-  ( ( N + 1 ) e. CC -> ( ( N + 1 ) ^ 2 ) = ( ( N + 1 ) x. ( N + 1 ) ) )
25 23 24 syl
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) ^ 2 ) = ( ( N + 1 ) x. ( N + 1 ) ) )
26 2cn
 |-  2 e. CC
27 mulcl
 |-  ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) e. CC )
28 26 13 27 sylancr
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( 2 x. N ) e. CC )
29 1cnd
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 1 e. CC )
30 15 28 29 add32d
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N ^ 2 ) + ( 2 x. N ) ) + 1 ) = ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) )
31 21 25 30 3eqtr3d
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( N + 1 ) ) = ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) )
32 31 oveq1d
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N + 1 ) x. ( N + 1 ) ) / 2 ) = ( ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) / 2 ) )
33 2cnd
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 2 e. CC )
34 6 a1i
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 2 =/= 0 )
35 23 23 33 34 divassd
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N + 1 ) x. ( N + 1 ) ) / 2 ) = ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) )
36 17 28 33 34 divdird
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) / 2 ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + ( ( 2 x. N ) / 2 ) ) )
37 13 33 34 divcan3d
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( 2 x. N ) / 2 ) = N )
38 37 oveq2d
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + ( ( 2 x. N ) / 2 ) ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) )
39 36 38 eqtrd
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) / 2 ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) )
40 32 35 39 3eqtr3d
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) )
41 peano2z
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
42 zmulcl
 |-  ( ( ( N + 1 ) e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) e. ZZ )
43 41 42 sylan
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) e. ZZ )
44 40 43 eqeltrrd
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) e. ZZ )
45 simpl
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> N e. ZZ )
46 44 45 zsubcld
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) - N ) e. ZZ )
47 19 46 eqeltrrd
 |-  ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ )
48 47 ex
 |-  ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) )
49 48 con3d
 |-  ( N e. ZZ -> ( -. ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ -> -. ( ( N + 1 ) / 2 ) e. ZZ ) )
50 zsqcl
 |-  ( N e. ZZ -> ( N ^ 2 ) e. ZZ )
51 zeo2
 |-  ( ( N ^ 2 ) e. ZZ -> ( ( ( N ^ 2 ) / 2 ) e. ZZ <-> -. ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) )
52 50 51 syl
 |-  ( N e. ZZ -> ( ( ( N ^ 2 ) / 2 ) e. ZZ <-> -. ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) )
53 zeo2
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> -. ( ( N + 1 ) / 2 ) e. ZZ ) )
54 49 52 53 3imtr4d
 |-  ( N e. ZZ -> ( ( ( N ^ 2 ) / 2 ) e. ZZ -> ( N / 2 ) e. ZZ ) )
55 54 imp
 |-  ( ( N e. ZZ /\ ( ( N ^ 2 ) / 2 ) e. ZZ ) -> ( N / 2 ) e. ZZ )
56 12 55 impbida
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) )