Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sumcubes Structured version   Visualization version   GIF version

Theorem sumcubes 42325
Description: The sum of the first 𝑁 perfect cubes is the sum of the first 𝑁 nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025.)
Assertion
Ref Expression
sumcubes (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(𝑘↑3) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2))
Distinct variable group:   𝑘,𝑁

Proof of Theorem sumcubes
Dummy variables 𝑙 𝑚 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7438 . . . . 5 (𝑥 = 0 → (1...𝑥) = (1...0))
21sumeq1d 15732 . . . 4 (𝑥 = 0 → Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...0)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)))
31sumeq1d 15732 . . . . . 6 (𝑥 = 0 → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...0)𝑘)
43oveq2d 7446 . . . . 5 (𝑥 = 0 → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...0)𝑘))
54sumeq1d 15732 . . . 4 (𝑥 = 0 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...0)𝑘)((2 · 𝑚) − 1))
62, 5eqeq12d 2750 . . 3 (𝑥 = 0 → (Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...0)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...0)𝑘)((2 · 𝑚) − 1)))
7 oveq2 7438 . . . . 5 (𝑥 = 𝑦 → (1...𝑥) = (1...𝑦))
87sumeq1d 15732 . . . 4 (𝑥 = 𝑦 → Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)))
97sumeq1d 15732 . . . . . 6 (𝑥 = 𝑦 → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...𝑦)𝑘)
109oveq2d 7446 . . . . 5 (𝑥 = 𝑦 → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...𝑦)𝑘))
1110sumeq1d 15732 . . . 4 (𝑥 = 𝑦 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1))
128, 11eqeq12d 2750 . . 3 (𝑥 = 𝑦 → (Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)))
13 oveq2 7438 . . . . 5 (𝑥 = (𝑦 + 1) → (1...𝑥) = (1...(𝑦 + 1)))
1413sumeq1d 15732 . . . 4 (𝑥 = (𝑦 + 1) → Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)))
1513sumeq1d 15732 . . . . . 6 (𝑥 = (𝑦 + 1) → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)
1615oveq2d 7446 . . . . 5 (𝑥 = (𝑦 + 1) → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘))
1716sumeq1d 15732 . . . 4 (𝑥 = (𝑦 + 1) → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1))
1814, 17eqeq12d 2750 . . 3 (𝑥 = (𝑦 + 1) → (Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1)))
19 oveq2 7438 . . . . 5 (𝑥 = 𝑁 → (1...𝑥) = (1...𝑁))
2019sumeq1d 15732 . . . 4 (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...𝑁𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)))
2119sumeq1d 15732 . . . . . 6 (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑥)𝑘 = Σ𝑘 ∈ (1...𝑁)𝑘)
2221oveq2d 7446 . . . . 5 (𝑥 = 𝑁 → (1...Σ𝑘 ∈ (1...𝑥)𝑘) = (1...Σ𝑘 ∈ (1...𝑁)𝑘))
2322sumeq1d 15732 . . . 4 (𝑥 = 𝑁 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1))
2420, 23eqeq12d 2750 . . 3 (𝑥 = 𝑁 → (Σ𝑘 ∈ (1...𝑥𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑥)𝑘)((2 · 𝑚) − 1) ↔ Σ𝑘 ∈ (1...𝑁𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1)))
25 sum0 15753 . . . . 5 Σ𝑘 ∈ ∅ Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = 0
26 sum0 15753 . . . . 5 Σ𝑚 ∈ ∅ ((2 · 𝑚) − 1) = 0
2725, 26eqtr4i 2765 . . . 4 Σ𝑘 ∈ ∅ Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ ∅ ((2 · 𝑚) − 1)
28 fz10 13581 . . . . 5 (1...0) = ∅
2928sumeq1i 15729 . . . 4 Σ𝑘 ∈ (1...0)Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ ∅ Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1))
3028sumeq1i 15729 . . . . . . . 8 Σ𝑘 ∈ (1...0)𝑘 = Σ𝑘 ∈ ∅ 𝑘
31 sum0 15753 . . . . . . . 8 Σ𝑘 ∈ ∅ 𝑘 = 0
3230, 31eqtri 2762 . . . . . . 7 Σ𝑘 ∈ (1...0)𝑘 = 0
3332oveq2i 7441 . . . . . 6 (1...Σ𝑘 ∈ (1...0)𝑘) = (1...0)
3433, 28eqtri 2762 . . . . 5 (1...Σ𝑘 ∈ (1...0)𝑘) = ∅
3534sumeq1i 15729 . . . 4 Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...0)𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ ∅ ((2 · 𝑚) − 1)
3627, 29, 353eqtr4i 2772 . . 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 14010 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → (1...𝑦) ∈ Fin)
39 elfznn 13589 . . . . . . . . . . . . 13 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
4039adantl 481 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℕ)
4140nnnn0d 12584 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℕ0)
4238, 41fsumnn0cl 15768 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 ∈ ℕ0)
4342nn0zd 12636 . . . . . . . . 9 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 ∈ ℤ)
44 nn0p1nn 12562 . . . . . . . . . . 11 𝑘 ∈ (1...𝑦)𝑘 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦)𝑘 + 1) ∈ ℕ)
4542, 44syl 17 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦)𝑘 + 1) ∈ ℕ)
4645nnzd 12637 . . . . . . . . 9 (𝑦 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦)𝑘 + 1) ∈ ℤ)
47 peano2nn0 12563 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ0)
4847nn0zd 12636 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℤ)
4943, 48zaddcld 12723 . . . . . . . . 9 (𝑦 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) ∈ ℤ)
50 2cnd 12341 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 2 ∈ ℂ)
51 elfzelz 13560 . . . . . . . . . . . . 13 (𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℤ)
5251zcnd 12720 . . . . . . . . . . . 12 (𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℂ)
5352adantl 481 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 𝑚 ∈ ℂ)
5450, 53mulcld 11278 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → (2 · 𝑚) ∈ ℂ)
55 1cnd 11253 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 1 ∈ ℂ)
5654, 55subcld 11617 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → ((2 · 𝑚) − 1) ∈ ℂ)
57 oveq2 7438 . . . . . . . . . 10 (𝑚 = (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘) → (2 · 𝑚) = (2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)))
5857oveq1d 7445 . . . . . . . . 9 (𝑚 = (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘) → ((2 · 𝑚) − 1) = ((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1))
5943, 46, 49, 56, 58fsumshftm 15813 . . . . . . . 8 (𝑦 ∈ ℕ0 → Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1) = Σ𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘))((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1))
60 elfzelz 13560 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℤ)
6160adantl 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℤ)
6261zred 12719 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑘 ∈ (1...𝑦)) → 𝑘 ∈ ℝ)
6338, 62fsumrecl 15766 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 ∈ ℝ)
6463recnd 11286 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 ∈ ℂ)
65 1cnd 11253 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → 1 ∈ ℂ)
6664, 65pncan2d 11619 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘) = 1)
6747nn0cnd 12586 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℂ)
6864, 67pncan2d 11619 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → ((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘) = (𝑦 + 1))
6966, 68oveq12d 7448 . . . . . . . . 9 (𝑦 ∈ ℕ0 → (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘)) = (1...(𝑦 + 1)))
70 elfzelz 13560 . . . . . . . . . . 11 (𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘)) → 𝑙 ∈ ℤ)
7170zcnd 12720 . . . . . . . . . 10 (𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘)) → 𝑙 ∈ ℂ)
72 2cnd 12341 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → 2 ∈ ℂ)
73 simpr 484 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → 𝑙 ∈ ℂ)
7464adantr 480 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → Σ𝑘 ∈ (1...𝑦)𝑘 ∈ ℂ)
7572, 73, 74adddid 11282 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → (2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) = ((2 · 𝑙) + (2 · Σ𝑘 ∈ (1...𝑦)𝑘)))
7675oveq1d 7445 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → ((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = (((2 · 𝑙) + (2 · Σ𝑘 ∈ (1...𝑦)𝑘)) − 1))
7772, 73mulcld 11278 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → (2 · 𝑙) ∈ ℂ)
7872, 74mulcld 11278 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → (2 · Σ𝑘 ∈ (1...𝑦)𝑘) ∈ ℂ)
79 1cnd 11253 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → 1 ∈ ℂ)
8077, 78, 79addsubassd 11637 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → (((2 · 𝑙) + (2 · Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = ((2 · 𝑙) + ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) − 1)))
8177, 78, 79addsub12d 11640 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → ((2 · 𝑙) + ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) − 1)) = ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) + ((2 · 𝑙) − 1)))
82 arisum 15892 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 = (((𝑦↑2) + 𝑦) / 2))
8382oveq2d 7446 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (2 · Σ𝑘 ∈ (1...𝑦)𝑘) = (2 · (((𝑦↑2) + 𝑦) / 2)))
84 nn0cn 12533 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0𝑦 ∈ ℂ)
8584sqcld 14180 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ0 → (𝑦↑2) ∈ ℂ)
8685, 84addcld 11277 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → ((𝑦↑2) + 𝑦) ∈ ℂ)
87 2cnd 12341 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → 2 ∈ ℂ)
88 2ne0 12367 . . . . . . . . . . . . . . . . 17 2 ≠ 0
8988a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → 2 ≠ 0)
9086, 87, 89divcan2d 12042 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (2 · (((𝑦↑2) + 𝑦) / 2)) = ((𝑦↑2) + 𝑦))
91 binom21 14254 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ → ((𝑦 + 1)↑2) = (((𝑦↑2) + (2 · 𝑦)) + 1))
9284, 91syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ0 → ((𝑦 + 1)↑2) = (((𝑦↑2) + (2 · 𝑦)) + 1))
9392oveq1d 7445 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → (((𝑦 + 1)↑2) − (𝑦 + 1)) = ((((𝑦↑2) + (2 · 𝑦)) + 1) − (𝑦 + 1)))
9487, 84mulcld 11278 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0 → (2 · 𝑦) ∈ ℂ)
9585, 94addcld 11277 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ0 → ((𝑦↑2) + (2 · 𝑦)) ∈ ℂ)
9695, 84, 65pnpcan2d 11655 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → ((((𝑦↑2) + (2 · 𝑦)) + 1) − (𝑦 + 1)) = (((𝑦↑2) + (2 · 𝑦)) − 𝑦))
9785, 94, 84addsubassd 11637 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ0 → (((𝑦↑2) + (2 · 𝑦)) − 𝑦) = ((𝑦↑2) + ((2 · 𝑦) − 𝑦)))
98842timesd 12506 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ0 → (2 · 𝑦) = (𝑦 + 𝑦))
9984, 84, 98mvrladdd 11673 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0 → ((2 · 𝑦) − 𝑦) = 𝑦)
10099oveq2d 7446 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ0 → ((𝑦↑2) + ((2 · 𝑦) − 𝑦)) = ((𝑦↑2) + 𝑦))
10197, 100eqtrd 2774 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → (((𝑦↑2) + (2 · 𝑦)) − 𝑦) = ((𝑦↑2) + 𝑦))
10293, 96, 1013eqtrrd 2779 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → ((𝑦↑2) + 𝑦) = (((𝑦 + 1)↑2) − (𝑦 + 1)))
10383, 90, 1023eqtrd 2778 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ0 → (2 · Σ𝑘 ∈ (1...𝑦)𝑘) = (((𝑦 + 1)↑2) − (𝑦 + 1)))
104103adantr 480 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → (2 · Σ𝑘 ∈ (1...𝑦)𝑘) = (((𝑦 + 1)↑2) − (𝑦 + 1)))
105104oveq1d 7445 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) + ((2 · 𝑙) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
10681, 105eqtrd 2774 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → ((2 · 𝑙) + ((2 · Σ𝑘 ∈ (1...𝑦)𝑘) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
10776, 80, 1063eqtrd 2778 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑙 ∈ ℂ) → ((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
10871, 107sylan2 593 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘))) → ((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
10969, 108sumeq12dv 15738 . . . . . . . 8 (𝑦 ∈ ℕ0 → Σ𝑙 ∈ (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) − Σ𝑘 ∈ (1...𝑦)𝑘)...((Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) − Σ𝑘 ∈ (1...𝑦)𝑘))((2 · (𝑙 + Σ𝑘 ∈ (1...𝑦)𝑘)) − 1) = Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
11059, 109eqtr2d 2775 . . . . . . 7 (𝑦 ∈ ℕ0 → Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1))
111110adantr 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))
11237, 111oveq12d 7448 . . . . 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 14010 . . . . . . . 8 ((𝑦 ∈ ℕ0𝑘 ∈ (1...(𝑦 + 1))) → (1...𝑘) ∈ Fin)
115 elfzelz 13560 . . . . . . . . . . . . 13 (𝑘 ∈ (1...(𝑦 + 1)) → 𝑘 ∈ ℤ)
116115zcnd 12720 . . . . . . . . . . . 12 (𝑘 ∈ (1...(𝑦 + 1)) → 𝑘 ∈ ℂ)
117116sqcld 14180 . . . . . . . . . . 11 (𝑘 ∈ (1...(𝑦 + 1)) → (𝑘↑2) ∈ ℂ)
118117, 116subcld 11617 . . . . . . . . . 10 (𝑘 ∈ (1...(𝑦 + 1)) → ((𝑘↑2) − 𝑘) ∈ ℂ)
119 2cnd 12341 . . . . . . . . . . . 12 (𝑙 ∈ (1...𝑘) → 2 ∈ ℂ)
120 elfzelz 13560 . . . . . . . . . . . . 13 (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℤ)
121120zcnd 12720 . . . . . . . . . . . 12 (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℂ)
122119, 121mulcld 11278 . . . . . . . . . . 11 (𝑙 ∈ (1...𝑘) → (2 · 𝑙) ∈ ℂ)
123 1cnd 11253 . . . . . . . . . . 11 (𝑙 ∈ (1...𝑘) → 1 ∈ ℂ)
124122, 123subcld 11617 . . . . . . . . . 10 (𝑙 ∈ (1...𝑘) → ((2 · 𝑙) − 1) ∈ ℂ)
125 addcl 11234 . . . . . . . . . 10 ((((𝑘↑2) − 𝑘) ∈ ℂ ∧ ((2 · 𝑙) − 1) ∈ ℂ) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈ ℂ)
126118, 124, 125syl2an 596 . . . . . . . . 9 ((𝑘 ∈ (1...(𝑦 + 1)) ∧ 𝑙 ∈ (1...𝑘)) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈ ℂ)
127126adantll 714 . . . . . . . 8 (((𝑦 ∈ ℕ0𝑘 ∈ (1...(𝑦 + 1))) ∧ 𝑙 ∈ (1...𝑘)) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈ ℂ)
128114, 127fsumcl 15765 . . . . . . 7 ((𝑦 ∈ ℕ0𝑘 ∈ (1...(𝑦 + 1))) → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) ∈ ℂ)
129 oveq2 7438 . . . . . . . 8 (𝑘 = (𝑦 + 1) → (1...𝑘) = (1...(𝑦 + 1)))
130 oveq1 7437 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → (𝑘↑2) = ((𝑦 + 1)↑2))
131 id 22 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → 𝑘 = (𝑦 + 1))
132130, 131oveq12d 7448 . . . . . . . . . 10 (𝑘 = (𝑦 + 1) → ((𝑘↑2) − 𝑘) = (((𝑦 + 1)↑2) − (𝑦 + 1)))
133132oveq1d 7445 . . . . . . . . 9 (𝑘 = (𝑦 + 1) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
134133adantr 480 . . . . . . . 8 ((𝑘 = (𝑦 + 1) ∧ 𝑙 ∈ (1...𝑘)) → (((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = ((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
135129, 134sumeq12dv 15738 . . . . . . 7 (𝑘 = (𝑦 + 1) → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1)))
136113, 128, 135fz1sump1 42322 . . . . . 6 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) + Σ𝑙 ∈ (1...(𝑦 + 1))((((𝑦 + 1)↑2) − (𝑦 + 1)) + ((2 · 𝑙) − 1))))
137136adantr 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))))
138116adantl 481 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑘 ∈ (1...(𝑦 + 1))) → 𝑘 ∈ ℂ)
139113, 138, 131fz1sump1 42322 . . . . . . . . 9 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...(𝑦 + 1))𝑘 = (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))
140139adantr 480 . . . . . . . 8 ((𝑦 ∈ ℕ0 ∧ Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑘 ∈ (1...(𝑦 + 1))𝑘 = (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))
141140oveq2d 7446 . . . . . . 7 ((𝑦 ∈ ℕ0 ∧ Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘) = (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))))
142141sumeq1d 15732 . . . . . 6 ((𝑦 ∈ ℕ0 ∧ Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1) = Σ𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1))
14363ltp1d 12195 . . . . . . . . 9 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 < (Σ𝑘 ∈ (1...𝑦)𝑘 + 1))
144 fzdisj 13587 . . . . . . . . 9 𝑘 ∈ (1...𝑦)𝑘 < (Σ𝑘 ∈ (1...𝑦)𝑘 + 1) → ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∩ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) = ∅)
145143, 144syl 17 . . . . . . . 8 (𝑦 ∈ ℕ0 → ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∩ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) = ∅)
146 nnuz 12918 . . . . . . . . . 10 ℕ = (ℤ‘1)
14745, 146eleqtrdi 2848 . . . . . . . . 9 (𝑦 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦)𝑘 + 1) ∈ (ℤ‘1))
14843uzidd 12891 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑦)𝑘 ∈ (ℤ‘Σ𝑘 ∈ (1...𝑦)𝑘))
149 uzaddcl 12943 . . . . . . . . . 10 ((Σ𝑘 ∈ (1...𝑦)𝑘 ∈ (ℤ‘Σ𝑘 ∈ (1...𝑦)𝑘) ∧ (𝑦 + 1) ∈ ℕ0) → (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) ∈ (ℤ‘Σ𝑘 ∈ (1...𝑦)𝑘))
150148, 47, 149syl2anc 584 . . . . . . . . 9 (𝑦 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) ∈ (ℤ‘Σ𝑘 ∈ (1...𝑦)𝑘))
151 fzsplit2 13585 . . . . . . . . 9 (((Σ𝑘 ∈ (1...𝑦)𝑘 + 1) ∈ (ℤ‘1) ∧ (Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)) ∈ (ℤ‘Σ𝑘 ∈ (1...𝑦)𝑘)) → (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) = ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∪ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))))
152147, 150, 151syl2anc 584 . . . . . . . 8 (𝑦 ∈ ℕ0 → (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) = ((1...Σ𝑘 ∈ (1...𝑦)𝑘) ∪ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))))
153 fzfid 14010 . . . . . . . 8 (𝑦 ∈ ℕ0 → (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) ∈ Fin)
154 2cnd 12341 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 2 ∈ ℂ)
155 elfzelz 13560 . . . . . . . . . . . 12 (𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℤ)
156155zcnd 12720 . . . . . . . . . . 11 (𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1))) → 𝑚 ∈ ℂ)
157156adantl 481 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 𝑚 ∈ ℂ)
158154, 157mulcld 11278 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → (2 · 𝑚) ∈ ℂ)
159 1cnd 11253 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → 1 ∈ ℂ)
160158, 159subcld 11617 . . . . . . . 8 ((𝑦 ∈ ℕ0𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))) → ((2 · 𝑚) − 1) ∈ ℂ)
161145, 152, 153, 160fsumsplit 15773 . . . . . . 7 (𝑦 ∈ ℕ0 → Σ𝑚 ∈ (1...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1) = (Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) + Σ𝑚 ∈ ((Σ𝑘 ∈ (1...𝑦)𝑘 + 1)...(Σ𝑘 ∈ (1...𝑦)𝑘 + (𝑦 + 1)))((2 · 𝑚) − 1)))
162161adantr 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)))
163142, 162eqtrd 2774 . . . . 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)))
164112, 137, 1633eqtr4d 2784 . . . 4 ((𝑦 ∈ ℕ0 ∧ Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1)) → Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1))
165164ex 412 . . 3 (𝑦 ∈ ℕ0 → (Σ𝑘 ∈ (1...𝑦𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑦)𝑘)((2 · 𝑚) − 1) → Σ𝑘 ∈ (1...(𝑦 + 1))Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...(𝑦 + 1))𝑘)((2 · 𝑚) − 1)))
1666, 12, 18, 24, 36, 165nn0ind 12710 . 2 (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1))
167 fz1ssnn 13591 . . . . . . 7 (1...𝑁) ⊆ ℕ
168 nnssnn0 12526 . . . . . . 7 ℕ ⊆ ℕ0
169167, 168sstri 4004 . . . . . 6 (1...𝑁) ⊆ ℕ0
170169a1i 11 . . . . 5 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ ℕ0)
171170sselda 3994 . . . 4 ((𝑁 ∈ ℕ0𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ0)
172 nicomachus 42324 . . . 4 (𝑘 ∈ ℕ0 → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (𝑘↑3))
173171, 172syl 17 . . 3 ((𝑁 ∈ ℕ0𝑘 ∈ (1...𝑁)) → Σ𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = (𝑘↑3))
174173sumeq2dv 15734 . 2 (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁𝑙 ∈ (1...𝑘)(((𝑘↑2) − 𝑘) + ((2 · 𝑙) − 1)) = Σ𝑘 ∈ (1...𝑁)(𝑘↑3))
175 fzfid 14010 . . . 4 (𝑁 ∈ ℕ0 → (1...𝑁) ∈ Fin)
176175, 171fsumnn0cl 15768 . . 3 (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)𝑘 ∈ ℕ0)
177 oddnumth 42323 . . 3 𝑘 ∈ (1...𝑁)𝑘 ∈ ℕ0 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2))
178176, 177syl 17 . 2 (𝑁 ∈ ℕ0 → Σ𝑚 ∈ (1...Σ𝑘 ∈ (1...𝑁)𝑘)((2 · 𝑚) − 1) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2))
179166, 174, 1783eqtr3d 2782 1 (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(𝑘↑3) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wne 2937  cun 3960  cin 3961  wss 3962  c0 4338   class class class wbr 5147  cfv 6562  (class class class)co 7430  cc 11150  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cmin 11489   / cdiv 11917  cn 12263  2c2 12318  3c3 12319  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543  cexp 14098  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719
This theorem is referenced by:  sum9cubes  42658
  Copyright terms: Public domain W3C validator