Step | Hyp | Ref
| Expression |
1 | | oveq2 7420 |
. . . . 5
⊢ (𝑥 = 0 → (1...𝑥) = (1...0)) |
2 | 1 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = 0 → Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...0)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1))) |
3 | 1 | sumeq1d 15654 |
. . . . . 6
⊢ (𝑥 = 0 → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...0)𝑘) |
4 | 3 | oveq2d 7428 |
. . . . 5
⊢ (𝑥 = 0 → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...0)𝑘)) |
5 | 4 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = 0 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...0)𝑘)((2 · 𝑚) − 1)) |
6 | 2, 5 | eqeq12d 2747 |
. . 3
⊢ (𝑥 = 0 → (Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...0)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...0)𝑘)((2 · 𝑚) − 1))) |
7 | | oveq2 7420 |
. . . . 5
⊢ (𝑥 = 𝑦 → (1...𝑥) = (1...𝑦)) |
8 | 7 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1))) |
9 | 7 | sumeq1d 15654 |
. . . . . 6
⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...𝑦)𝑘) |
10 | 9 | oveq2d 7428 |
. . . . 5
⊢ (𝑥 = 𝑦 → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...𝑦)𝑘)) |
11 | 10 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = 𝑦 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) |
12 | 8, 11 | eqeq12d 2747 |
. . 3
⊢ (𝑥 = 𝑦 → (Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1))) |
13 | | oveq2 7420 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (1...𝑥) = (1...(𝑦 + 1))) |
14 | 13 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1))) |
15 | 13 | sumeq1d 15654 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...(𝑦 + 1))𝑘) |
16 | 15 | oveq2d 7428 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)) |
17 | 16 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1)) |
18 | 14, 17 | eqeq12d 2747 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1))) |
19 | | oveq2 7420 |
. . . . 5
⊢ (𝑥 = 𝑁 → (1...𝑥) = (1...𝑁)) |
20 | 19 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...𝑁)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1))) |
21 | 19 | sumeq1d 15654 |
. . . . . 6
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...𝑁)𝑘) |
22 | 21 | oveq2d 7428 |
. . . . 5
⊢ (𝑥 = 𝑁 → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...𝑁)𝑘)) |
23 | 22 | sumeq1d 15654 |
. . . 4
⊢ (𝑥 = 𝑁 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1)) |
24 | 20, 23 | eqeq12d 2747 |
. . 3
⊢ (𝑥 = 𝑁 → (Σ𝑘 ∈ (1...𝑥)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...𝑁)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1))) |
25 | | sum0 15674 |
. . . . 5
⊢
Σ𝑘 ∈
∅ Σ𝑙 ∈
(1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) =
0 |
26 | | sum0 15674 |
. . . . 5
⊢
Σ𝑚 ∈
∅ ((2 · 𝑚)
− 1) = 0 |
27 | 25, 26 | eqtr4i 2762 |
. . . 4
⊢
Σ𝑘 ∈
∅ Σ𝑙 ∈
(1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ ∅ ((2 ·
𝑚) −
1) |
28 | | fz10 13529 |
. . . . 5
⊢ (1...0) =
∅ |
29 | 28 | sumeq1i 15651 |
. . . 4
⊢
Σ𝑘 ∈
(1...0)Σ𝑙 ∈
(1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ ∅ Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) |
30 | 28 | sumeq1i 15651 |
. . . . . . . 8
⊢
Σ𝑘 ∈
(1...0)𝑘 = Σ𝑘 ∈ ∅ 𝑘 |
31 | | sum0 15674 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ 𝑘 =
0 |
32 | 30, 31 | eqtri 2759 |
. . . . . . 7
⊢
Σ𝑘 ∈
(1...0)𝑘 =
0 |
33 | 32 | oveq2i 7423 |
. . . . . 6
⊢
(1...Σ𝑘 ∈
(1...0)𝑘) =
(1...0) |
34 | 33, 28 | eqtri 2759 |
. . . . 5
⊢
(1...Σ𝑘 ∈
(1...0)𝑘) =
∅ |
35 | 34 | sumeq1i 15651 |
. . . 4
⊢
Σ𝑚 ∈
(1...Σ𝑘 ∈
(1...0)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ ∅ ((2 ·
𝑚) −
1) |
36 | 27, 29, 35 | 3eqtr4i 2769 |
. . 3
⊢
Σ𝑘 ∈
(1...0)Σ𝑙 ∈
(1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...0)𝑘)((2 · 𝑚) − 1) |
37 | | simpr 484 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑘 ∈ (1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) |
38 | | fzfid 13945 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (1...𝑦) ∈
Fin) |
39 | | elfznn 13537 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℕ) |
41 | 40 | nnnn0d 12539 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℕ0) |
42 | 38, 41 | fsumnn0cl 15689 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 ∈ ℕ0) |
43 | 42 | nn0zd 12591 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 ∈ ℤ) |
44 | | nn0p1nn 12518 |
. . . . . . . . . . 11
⊢
(Σ𝑘 ∈
(1...𝑦)𝑘 ∈ ℕ0 →
(Σ𝑘 ∈ (1...𝑦)𝑘 + 1) ∈ ℕ) |
45 | 42, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ (Σ𝑘 ∈
(1...𝑦)𝑘 + 1) ∈ ℕ) |
46 | 45 | nnzd 12592 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (Σ𝑘 ∈
(1...𝑦)𝑘 + 1) ∈ ℤ) |
47 | | peano2nn0 12519 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ0) |
48 | 47 | nn0zd 12591 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℤ) |
49 | 43, 48 | zaddcld 12677 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)) ∈ ℤ) |
50 | | 2cnd 12297 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
((Σ𝑘 ∈
(1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 2 ∈
ℂ) |
51 | | elfzelz 13508 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℤ) |
52 | 51 | zcnd 12674 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℂ) |
53 | 52 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
((Σ𝑘 ∈
(1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 𝑚 ∈ ℂ) |
54 | 50, 53 | mulcld 11241 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
((Σ𝑘 ∈
(1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → (2 · 𝑚) ∈
ℂ) |
55 | | 1cnd 11216 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
((Σ𝑘 ∈
(1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 1 ∈
ℂ) |
56 | 54, 55 | subcld 11578 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
((Σ𝑘 ∈
(1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → ((2 · 𝑚) − 1) ∈
ℂ) |
57 | | oveq2 7420 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘) → (2 · 𝑚) = (2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘))) |
58 | 57 | oveq1d 7427 |
. . . . . . . . 9
⊢ (𝑚 = (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘) → ((2 · 𝑚) − 1) = ((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1)) |
59 | 43, 46, 49, 56, 58 | fsumshftm 15734 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ Σ𝑚 ∈
((Σ𝑘 ∈
(1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1) = Σ𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘))((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1)) |
60 | | elfzelz 13508 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℤ) |
61 | 60 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℤ) |
62 | 61 | zred 12673 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℝ) |
63 | 38, 62 | fsumrecl 15687 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 ∈ ℝ) |
64 | 63 | recnd 11249 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 ∈ ℂ) |
65 | | 1cnd 11216 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ 1 ∈ ℂ) |
66 | 64, 65 | pncan2d 11580 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ ((Σ𝑘 ∈
(1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘) = 1) |
67 | 47 | nn0cnd 12541 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℂ) |
68 | 64, 67 | pncan2d 11580 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ ((Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘) = (𝑦 + 1)) |
69 | 66, 68 | oveq12d 7430 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (((Σ𝑘 ∈
(1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘)) = (1...(𝑦 + 1))) |
70 | | elfzelz 13508 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘)) → 𝑙 ∈ ℤ) |
71 | 70 | zcnd 12674 |
. . . . . . . . . 10
⊢ (𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘)) → 𝑙 ∈ ℂ) |
72 | | 2cnd 12297 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ 2 ∈ ℂ) |
73 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ 𝑙 ∈
ℂ) |
74 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ Σ𝑘 ∈
(1...𝑦)𝑘 ∈ ℂ) |
75 | 72, 73, 74 | adddid 11245 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ (2 · (𝑙 +
Σ𝑘 ∈ (1...𝑦)𝑘)) = ((2 · 𝑙) + (2 · Σ𝑘 ∈ (1...𝑦)𝑘))) |
76 | 75 | oveq1d 7427 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ ((2 · (𝑙 +
Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = (((2 · 𝑙) + (2 · Σ𝑘 ∈ (1...𝑦)𝑘)) − 1)) |
77 | 72, 73 | mulcld 11241 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ (2 · 𝑙)
∈ ℂ) |
78 | 72, 74 | mulcld 11241 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ (2 · Σ𝑘
∈ (1...𝑦)𝑘) ∈
ℂ) |
79 | | 1cnd 11216 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ 1 ∈ ℂ) |
80 | 77, 78, 79 | addsubassd 11598 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ (((2 · 𝑙) +
(2 · Σ𝑘 ∈
(1...𝑦)𝑘)) − 1) = ((2 · 𝑙) + ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) − 1))) |
81 | 77, 78, 79 | addsub12d 11601 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ ((2 · 𝑙) +
((2 · Σ𝑘
∈ (1...𝑦)𝑘) − 1)) = ((2 ·
Σ𝑘 ∈ (1...𝑦)𝑘) + ((2 · 𝑙) − 1))) |
82 | | arisum 15813 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 = (((𝑦↑2) + 𝑦) / 2)) |
83 | 82 | oveq2d 7428 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (2 · Σ𝑘
∈ (1...𝑦)𝑘) = (2 · (((𝑦↑2) + 𝑦) / 2))) |
84 | | nn0cn 12489 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
85 | 84 | sqcld 14116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
→ (𝑦↑2) ∈
ℂ) |
86 | 85, 84 | addcld 11240 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ ((𝑦↑2) + 𝑦) ∈
ℂ) |
87 | | 2cnd 12297 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ 2 ∈ ℂ) |
88 | | 2ne0 12323 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ 2 ≠ 0) |
90 | 86, 87, 89 | divcan2d 11999 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (2 · (((𝑦↑2) + 𝑦) / 2)) = ((𝑦↑2) + 𝑦)) |
91 | | binom21 14189 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℂ → ((𝑦 + 1)↑2) = (((𝑦↑2) + (2 · 𝑦)) + 1)) |
92 | 84, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
→ ((𝑦 + 1)↑2) =
(((𝑦↑2) + (2 ·
𝑦)) + 1)) |
93 | 92 | oveq1d 7427 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ (((𝑦 + 1)↑2)
− (𝑦 + 1)) =
((((𝑦↑2) + (2 ·
𝑦)) + 1) − (𝑦 + 1))) |
94 | 87, 84 | mulcld 11241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0
→ (2 · 𝑦)
∈ ℂ) |
95 | 85, 94 | addcld 11240 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
→ ((𝑦↑2) + (2
· 𝑦)) ∈
ℂ) |
96 | 95, 84, 65 | pnpcan2d 11616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ ((((𝑦↑2) + (2
· 𝑦)) + 1) −
(𝑦 + 1)) = (((𝑦↑2) + (2 · 𝑦)) − 𝑦)) |
97 | 85, 94, 84 | addsubassd 11598 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
→ (((𝑦↑2) + (2
· 𝑦)) − 𝑦) = ((𝑦↑2) + ((2 · 𝑦) − 𝑦))) |
98 | 84 | 2timesd 12462 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℕ0
→ (2 · 𝑦) =
(𝑦 + 𝑦)) |
99 | 84, 84, 98 | mvrladdd 11634 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0
→ ((2 · 𝑦)
− 𝑦) = 𝑦) |
100 | 99 | oveq2d 7428 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ0
→ ((𝑦↑2) + ((2
· 𝑦) − 𝑦)) = ((𝑦↑2) + 𝑦)) |
101 | 97, 100 | eqtrd 2771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
→ (((𝑦↑2) + (2
· 𝑦)) − 𝑦) = ((𝑦↑2) + 𝑦)) |
102 | 93, 96, 101 | 3eqtrrd 2776 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ ((𝑦↑2) + 𝑦) = (((𝑦 + 1)↑2) − (𝑦 + 1))) |
103 | 83, 90, 102 | 3eqtrd 2775 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2 · Σ𝑘
∈ (1...𝑦)𝑘) = (((𝑦 + 1)↑2) − (𝑦 + 1))) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ (2 · Σ𝑘
∈ (1...𝑦)𝑘) = (((𝑦 + 1)↑2) − (𝑦 + 1))) |
105 | 104 | oveq1d 7427 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) + ((2 · 𝑙) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
106 | 81, 105 | eqtrd 2771 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ ((2 · 𝑙) +
((2 · Σ𝑘
∈ (1...𝑦)𝑘) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
107 | 76, 80, 106 | 3eqtrd 2775 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈ ℂ)
→ ((2 · (𝑙 +
Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
108 | 71, 107 | sylan2 592 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝑙 ∈
(((Σ𝑘 ∈
(1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘))) → ((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
109 | 69, 108 | sumeq12dv 15659 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ Σ𝑙 ∈
(((Σ𝑘 ∈
(1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘))((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
110 | 59, 109 | eqtr2d 2772 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ Σ𝑙 ∈
(1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1)) |
111 | 110 | adantr 480 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1)) |
112 | 37, 111 | oveq12d 7430 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → (Σ𝑘 ∈ (1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) + Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) = (Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) + Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1))) |
113 | | id 22 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℕ0) |
114 | | fzfid 13945 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑦 + 1))) → (1...𝑘) ∈ Fin) |
115 | | elfzelz 13508 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑦 + 1)) → 𝑘 ∈ ℤ) |
116 | 115 | zcnd 12674 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑦 + 1)) → 𝑘 ∈ ℂ) |
117 | 116 | sqcld 14116 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑦 + 1)) → (𝑘↑2) ∈ ℂ) |
118 | 117, 116 | subcld 11578 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝑦 + 1)) → ((𝑘↑2) − 𝑘) ∈ ℂ) |
119 | | 2cnd 12297 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ (1...𝑘) → 2 ∈ ℂ) |
120 | | elfzelz 13508 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℤ) |
121 | 120 | zcnd 12674 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℂ) |
122 | 119, 121 | mulcld 11241 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (1...𝑘) → (2 · 𝑙) ∈ ℂ) |
123 | | 1cnd 11216 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (1...𝑘) → 1 ∈ ℂ) |
124 | 122, 123 | subcld 11578 |
. . . . . . . . . 10
⊢ (𝑙 ∈ (1...𝑘) → ((2 · 𝑙) − 1) ∈ ℂ) |
125 | | addcl 11198 |
. . . . . . . . . 10
⊢ ((((𝑘↑2) − 𝑘) ∈ ℂ ∧ ((2
· 𝑙) − 1)
∈ ℂ) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈
ℂ) |
126 | 118, 124,
125 | syl2an 595 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (1...(𝑦 + 1)) ∧ 𝑙 ∈ (1...𝑘)) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈
ℂ) |
127 | 126 | adantll 711 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑦 + 1))) ∧ 𝑙 ∈ (1...𝑘)) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈
ℂ) |
128 | 114, 127 | fsumcl 15686 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑦 + 1))) → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈
ℂ) |
129 | | oveq2 7420 |
. . . . . . . 8
⊢ (𝑘 = (𝑦 + 1) → (1...𝑘) = (1...(𝑦 + 1))) |
130 | | oveq1 7419 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑦 + 1) → (𝑘↑2) = ((𝑦 + 1)↑2)) |
131 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑦 + 1) → 𝑘 = (𝑦 + 1)) |
132 | 130, 131 | oveq12d 7430 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑦 + 1) → ((𝑘↑2) − 𝑘) = (((𝑦 + 1)↑2) − (𝑦 + 1))) |
133 | 132 | oveq1d 7427 |
. . . . . . . . 9
⊢ (𝑘 = (𝑦 + 1) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
134 | 133 | adantr 480 |
. . . . . . . 8
⊢ ((𝑘 = (𝑦 + 1) ∧ 𝑙 ∈ (1...𝑘)) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
135 | 129, 134 | sumeq12dv 15659 |
. . . . . . 7
⊢ (𝑘 = (𝑦 + 1) → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))) |
136 | 113, 128,
135 | fz1sump1 41523 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (Σ𝑘 ∈ (1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) + Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))) |
137 | 136 | adantr 480 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (Σ𝑘 ∈ (1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) + Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))) |
138 | 116 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑦 + 1))) → 𝑘 ∈
ℂ) |
139 | 113, 138,
131 | fz1sump1 41523 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...(𝑦 + 1))𝑘 = (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) |
140 | 139 | adantr 480 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑘 ∈ (1...(𝑦 + 1))𝑘 = (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) |
141 | 140 | oveq2d 7428 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘) = (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) |
142 | 141 | sumeq1d 15654 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1)) |
143 | 63 | ltp1d 12151 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 < (Σ𝑘 ∈ (1...𝑦)𝑘 + 1)) |
144 | | fzdisj 13535 |
. . . . . . . . 9
⊢
(Σ𝑘 ∈
(1...𝑦)𝑘 < (Σ𝑘 ∈ (1...𝑦)𝑘 + 1) → ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∩ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) = ∅) |
145 | 143, 144 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ ((1...Σ𝑘
∈ (1...𝑦)𝑘) ∩ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) = ∅) |
146 | | nnuz 12872 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
147 | 45, 146 | eleqtrdi 2842 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (Σ𝑘 ∈
(1...𝑦)𝑘 + 1) ∈
(ℤ≥‘1)) |
148 | 43 | uzidd 12845 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑦)𝑘 ∈
(ℤ≥‘Σ𝑘 ∈ (1...𝑦)𝑘)) |
149 | | uzaddcl 12895 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
(1...𝑦)𝑘 ∈
(ℤ≥‘Σ𝑘 ∈ (1...𝑦)𝑘) ∧ (𝑦 + 1) ∈ ℕ0) →
(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) ∈
(ℤ≥‘Σ𝑘 ∈ (1...𝑦)𝑘)) |
150 | 148, 47, 149 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)) ∈
(ℤ≥‘Σ𝑘 ∈ (1...𝑦)𝑘)) |
151 | | fzsplit2 13533 |
. . . . . . . . 9
⊢
(((Σ𝑘 ∈
(1...𝑦)𝑘 + 1) ∈ (ℤ≥‘1)
∧ (Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)) ∈
(ℤ≥‘Σ𝑘 ∈ (1...𝑦)𝑘)) → (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) = ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∪ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))))) |
152 | 147, 150,
151 | syl2anc 583 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ (1...(Σ𝑘
∈ (1...𝑦)𝑘 + (𝑦 + 1))) = ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∪ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))))) |
153 | | fzfid 13945 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ (1...(Σ𝑘
∈ (1...𝑦)𝑘 + (𝑦 + 1))) ∈ Fin) |
154 | | 2cnd 12297 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
(1...(Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)))) → 2 ∈
ℂ) |
155 | | elfzelz 13508 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℤ) |
156 | 155 | zcnd 12674 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℂ) |
157 | 156 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
(1...(Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)))) → 𝑚 ∈ ℂ) |
158 | 154, 157 | mulcld 11241 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
(1...(Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)))) → (2 · 𝑚) ∈
ℂ) |
159 | | 1cnd 11216 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
(1...(Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)))) → 1 ∈
ℂ) |
160 | 158, 159 | subcld 11578 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ 𝑚 ∈
(1...(Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)))) → ((2 · 𝑚) − 1) ∈
ℂ) |
161 | 145, 152,
153, 160 | fsumsplit 15694 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ Σ𝑚 ∈
(1...(Σ𝑘 ∈
(1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1) = (Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) + Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1))) |
162 | 161 | adantr 480 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1) = (Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) + Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1))) |
163 | 142, 162 | eqtrd 2771 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1) = (Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) + Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1))) |
164 | 112, 137,
163 | 3eqtr4d 2781 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1)) |
165 | 164 | ex 412 |
. . 3
⊢ (𝑦 ∈ ℕ0
→ (Σ𝑘 ∈
(1...𝑦)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) → Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1))) |
166 | 6, 12, 18, 24, 36, 165 | nn0ind 12664 |
. 2
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑁)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1)) |
167 | | fz1ssnn 13539 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℕ |
168 | | nnssnn0 12482 |
. . . . . . 7
⊢ ℕ
⊆ ℕ0 |
169 | 167, 168 | sstri 3991 |
. . . . . 6
⊢
(1...𝑁) ⊆
ℕ0 |
170 | 169 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ⊆
ℕ0) |
171 | 170 | sselda 3982 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ0) |
172 | | nicomachus 41525 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ Σ𝑙 ∈
(1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (𝑘↑3)) |
173 | 171, 172 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (𝑘↑3)) |
174 | 173 | sumeq2dv 15656 |
. 2
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑁)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...𝑁)(𝑘↑3)) |
175 | | fzfid 13945 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ∈
Fin) |
176 | 175, 171 | fsumnn0cl 15689 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑁)𝑘 ∈ ℕ0) |
177 | | oddnumth 41524 |
. . 3
⊢
(Σ𝑘 ∈
(1...𝑁)𝑘 ∈ ℕ0 →
Σ𝑚 ∈
(1...Σ𝑘 ∈
(1...𝑁)𝑘)((2 · 𝑚) − 1) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2)) |
178 | 176, 177 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ0
→ Σ𝑚 ∈
(1...Σ𝑘 ∈
(1...𝑁)𝑘)((2 · 𝑚) − 1) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2)) |
179 | 166, 174,
178 | 3eqtr3d 2779 |
1
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(1...𝑁)(𝑘↑3) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2)) |