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 ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ↔ ( ( 𝑁 ↑ 2 ) / 2 ) ∈ ℤ ) )

Proof

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