Proof of Theorem zesq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zcn 12618 | . . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 2 |  | sqval 14155 | . . . . . . 7
⊢ (𝑁 ∈ ℂ → (𝑁↑2) = (𝑁 · 𝑁)) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝑁 ∈ ℤ → (𝑁↑2) = (𝑁 · 𝑁)) | 
| 4 | 3 | oveq1d 7446 | . . . . 5
⊢ (𝑁 ∈ ℤ → ((𝑁↑2) / 2) = ((𝑁 · 𝑁) / 2)) | 
| 5 |  | 2cnd 12344 | . . . . . 6
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) | 
| 6 |  | 2ne0 12370 | . . . . . . 7
⊢ 2 ≠
0 | 
| 7 | 6 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ ℤ → 2 ≠
0) | 
| 8 | 1, 1, 5, 7 | divassd 12078 | . . . . 5
⊢ (𝑁 ∈ ℤ → ((𝑁 · 𝑁) / 2) = (𝑁 · (𝑁 / 2))) | 
| 9 | 4, 8 | eqtrd 2777 | . . . 4
⊢ (𝑁 ∈ ℤ → ((𝑁↑2) / 2) = (𝑁 · (𝑁 / 2))) | 
| 10 | 9 | adantr 480 | . . 3
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
((𝑁↑2) / 2) = (𝑁 · (𝑁 / 2))) | 
| 11 |  | zmulcl 12666 | . . 3
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
(𝑁 · (𝑁 / 2)) ∈
ℤ) | 
| 12 | 10, 11 | eqeltrd 2841 | . 2
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) →
((𝑁↑2) / 2) ∈
ℤ) | 
| 13 | 1 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ 𝑁 ∈
ℂ) | 
| 14 |  | sqcl 14158 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℂ → (𝑁↑2) ∈
ℂ) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (𝑁↑2) ∈
ℂ) | 
| 16 |  | peano2cn 11433 | . . . . . . . . . 10
⊢ ((𝑁↑2) ∈ ℂ →
((𝑁↑2) + 1) ∈
ℂ) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((𝑁↑2) + 1)
∈ ℂ) | 
| 18 | 17 | halfcld 12511 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((𝑁↑2) + 1) /
2) ∈ ℂ) | 
| 19 | 18, 13 | pncand 11621 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((((𝑁↑2) + 1)
/ 2) + 𝑁) − 𝑁) = (((𝑁↑2) + 1) / 2)) | 
| 20 |  | binom21 14258 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1)↑2) = (((𝑁↑2) + (2 · 𝑁)) + 1)) | 
| 21 | 13, 20 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((𝑁 + 1)↑2) =
(((𝑁↑2) + (2 ·
𝑁)) + 1)) | 
| 22 |  | peano2cn 11433 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) | 
| 23 | 13, 22 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (𝑁 + 1) ∈
ℂ) | 
| 24 |  | sqval 14155 | . . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈ ℂ →
((𝑁 + 1)↑2) = ((𝑁 + 1) · (𝑁 + 1))) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((𝑁 + 1)↑2) =
((𝑁 + 1) · (𝑁 + 1))) | 
| 26 |  | 2cn 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 27 |  | mulcl 11239 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → (2 · 𝑁) ∈ ℂ) | 
| 28 | 26, 13, 27 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (2 · 𝑁)
∈ ℂ) | 
| 29 |  | 1cnd 11256 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ 1 ∈ ℂ) | 
| 30 | 15, 28, 29 | add32d 11489 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((𝑁↑2) + (2
· 𝑁)) + 1) =
(((𝑁↑2) + 1) + (2
· 𝑁))) | 
| 31 | 21, 25, 30 | 3eqtr3d 2785 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((𝑁 + 1) ·
(𝑁 + 1)) = (((𝑁↑2) + 1) + (2 ·
𝑁))) | 
| 32 | 31 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((𝑁 + 1) ·
(𝑁 + 1)) / 2) = ((((𝑁↑2) + 1) + (2 ·
𝑁)) / 2)) | 
| 33 |  | 2cnd 12344 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ 2 ∈ ℂ) | 
| 34 | 6 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ 2 ≠ 0) | 
| 35 | 23, 23, 33, 34 | divassd 12078 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((𝑁 + 1) ·
(𝑁 + 1)) / 2) = ((𝑁 + 1) · ((𝑁 + 1) / 2))) | 
| 36 | 17, 28, 33, 34 | divdird 12081 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((((𝑁↑2) + 1) +
(2 · 𝑁)) / 2) =
((((𝑁↑2) + 1) / 2) +
((2 · 𝑁) /
2))) | 
| 37 | 13, 33, 34 | divcan3d 12048 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((2 · 𝑁) / 2)
= 𝑁) | 
| 38 | 37 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((((𝑁↑2) + 1) /
2) + ((2 · 𝑁) / 2))
= ((((𝑁↑2) + 1) / 2) +
𝑁)) | 
| 39 | 36, 38 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((((𝑁↑2) + 1) +
(2 · 𝑁)) / 2) =
((((𝑁↑2) + 1) / 2) +
𝑁)) | 
| 40 | 32, 35, 39 | 3eqtr3d 2785 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((𝑁 + 1) ·
((𝑁 + 1) / 2)) = ((((𝑁↑2) + 1) / 2) + 𝑁)) | 
| 41 |  | peano2z 12658 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℤ) | 
| 42 |  | zmulcl 12666 | . . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ ℤ ∧
((𝑁 + 1) / 2) ∈
ℤ) → ((𝑁 + 1)
· ((𝑁 + 1) / 2))
∈ ℤ) | 
| 43 | 41, 42 | sylan 580 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((𝑁 + 1) ·
((𝑁 + 1) / 2)) ∈
ℤ) | 
| 44 | 40, 43 | eqeltrrd 2842 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ ((((𝑁↑2) + 1) /
2) + 𝑁) ∈
ℤ) | 
| 45 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ 𝑁 ∈
ℤ) | 
| 46 | 44, 45 | zsubcld 12727 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((((𝑁↑2) + 1)
/ 2) + 𝑁) − 𝑁) ∈
ℤ) | 
| 47 | 19, 46 | eqeltrrd 2842 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ)
→ (((𝑁↑2) + 1) /
2) ∈ ℤ) | 
| 48 | 47 | ex 412 | . . . . 5
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ →
(((𝑁↑2) + 1) / 2)
∈ ℤ)) | 
| 49 | 48 | con3d 152 | . . . 4
⊢ (𝑁 ∈ ℤ → (¬
(((𝑁↑2) + 1) / 2)
∈ ℤ → ¬ ((𝑁 + 1) / 2) ∈ ℤ)) | 
| 50 |  | zsqcl 14169 | . . . . 5
⊢ (𝑁 ∈ ℤ → (𝑁↑2) ∈
ℤ) | 
| 51 |  | zeo2 12705 | . . . . 5
⊢ ((𝑁↑2) ∈ ℤ →
(((𝑁↑2) / 2) ∈
ℤ ↔ ¬ (((𝑁↑2) + 1) / 2) ∈
ℤ)) | 
| 52 | 50, 51 | syl 17 | . . . 4
⊢ (𝑁 ∈ ℤ → (((𝑁↑2) / 2) ∈ ℤ
↔ ¬ (((𝑁↑2) +
1) / 2) ∈ ℤ)) | 
| 53 |  | zeo2 12705 | . . . 4
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔
¬ ((𝑁 + 1) / 2) ∈
ℤ)) | 
| 54 | 49, 52, 53 | 3imtr4d 294 | . . 3
⊢ (𝑁 ∈ ℤ → (((𝑁↑2) / 2) ∈ ℤ
→ (𝑁 / 2) ∈
ℤ)) | 
| 55 | 54 | imp 406 | . 2
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁↑2) / 2) ∈ ℤ)
→ (𝑁 / 2) ∈
ℤ) | 
| 56 | 12, 55 | impbida 801 | 1
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔
((𝑁↑2) / 2) ∈
ℤ)) |