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