Metamath Proof Explorer


Theorem sumcubes

Description: The sum of the first N perfect cubes is the sum of the first N 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)

Ref Expression
Assertion sumcubes ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 ↑ 3 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = 0 → ( 1 ... 𝑥 ) = ( 1 ... 0 ) )
2 1 sumeq1d ( 𝑥 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑘 ∈ ( 1 ... 0 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) )
3 1 sumeq1d ( 𝑥 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 = Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 )
4 3 oveq2d ( 𝑥 = 0 → ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) = ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) )
5 4 sumeq1d ( 𝑥 = 0 → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
6 2 5 eqeq12d ( 𝑥 = 0 → ( Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ↔ Σ 𝑘 ∈ ( 1 ... 0 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) )
7 oveq2 ( 𝑥 = 𝑦 → ( 1 ... 𝑥 ) = ( 1 ... 𝑦 ) )
8 7 sumeq1d ( 𝑥 = 𝑦 → Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) )
9 7 sumeq1d ( 𝑥 = 𝑦 → Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 = Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 )
10 9 oveq2d ( 𝑥 = 𝑦 → ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) = ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) )
11 10 sumeq1d ( 𝑥 = 𝑦 → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
12 8 11 eqeq12d ( 𝑥 = 𝑦 → ( Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ↔ Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) )
13 oveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 1 ... 𝑥 ) = ( 1 ... ( 𝑦 + 1 ) ) )
14 13 sumeq1d ( 𝑥 = ( 𝑦 + 1 ) → Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) )
15 13 sumeq1d ( 𝑥 = ( 𝑦 + 1 ) → Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 = Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 )
16 15 oveq2d ( 𝑥 = ( 𝑦 + 1 ) → ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) = ( 1 ... Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 ) )
17 16 sumeq1d ( 𝑥 = ( 𝑦 + 1 ) → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
18 14 17 eqeq12d ( 𝑥 = ( 𝑦 + 1 ) → ( Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ↔ Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) )
19 oveq2 ( 𝑥 = 𝑁 → ( 1 ... 𝑥 ) = ( 1 ... 𝑁 ) )
20 19 sumeq1d ( 𝑥 = 𝑁 → Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) )
21 19 sumeq1d ( 𝑥 = 𝑁 → Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 = Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
22 21 oveq2d ( 𝑥 = 𝑁 → ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) = ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) )
23 22 sumeq1d ( 𝑥 = 𝑁 → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
24 20 23 eqeq12d ( 𝑥 = 𝑁 → ( Σ 𝑘 ∈ ( 1 ... 𝑥 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑥 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ↔ Σ 𝑘 ∈ ( 1 ... 𝑁 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) )
25 sum0 Σ 𝑘 ∈ ∅ Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = 0
26 sum0 Σ 𝑚 ∈ ∅ ( ( 2 · 𝑚 ) − 1 ) = 0
27 25 26 eqtr4i Σ 𝑘 ∈ ∅ Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ∅ ( ( 2 · 𝑚 ) − 1 )
28 fz10 ( 1 ... 0 ) = ∅
29 28 sumeq1i Σ 𝑘 ∈ ( 1 ... 0 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑘 ∈ ∅ Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) )
30 28 sumeq1i Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 = Σ 𝑘 ∈ ∅ 𝑘
31 sum0 Σ 𝑘 ∈ ∅ 𝑘 = 0
32 30 31 eqtri Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 = 0
33 32 oveq2i ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) = ( 1 ... 0 )
34 33 28 eqtri ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) = ∅
35 34 sumeq1i Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑚 ∈ ∅ ( ( 2 · 𝑚 ) − 1 )
36 27 29 35 3eqtr4i Σ 𝑘 ∈ ( 1 ... 0 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 0 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 )
37 simpr ( ( 𝑦 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
38 fzfid ( 𝑦 ∈ ℕ0 → ( 1 ... 𝑦 ) ∈ Fin )
39 elfznn ( 𝑘 ∈ ( 1 ... 𝑦 ) → 𝑘 ∈ ℕ )
40 39 adantl ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑦 ) ) → 𝑘 ∈ ℕ )
41 40 nnnn0d ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑦 ) ) → 𝑘 ∈ ℕ0 )
42 38 41 fsumnn0cl ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ℕ0 )
43 42 nn0zd ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ℤ )
44 nn0p1nn ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ∈ ℕ )
45 42 44 syl ( 𝑦 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ∈ ℕ )
46 45 nnzd ( 𝑦 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ∈ ℤ )
47 peano2nn0 ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ0 )
48 47 nn0zd ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℤ )
49 43 48 zaddcld ( 𝑦 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ∈ ℤ )
50 2cnd ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → 2 ∈ ℂ )
51 elfzelz ( 𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) → 𝑚 ∈ ℤ )
52 51 zcnd ( 𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) → 𝑚 ∈ ℂ )
53 52 adantl ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → 𝑚 ∈ ℂ )
54 50 53 mulcld ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → ( 2 · 𝑚 ) ∈ ℂ )
55 1cnd ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → 1 ∈ ℂ )
56 54 55 subcld ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → ( ( 2 · 𝑚 ) − 1 ) ∈ ℂ )
57 oveq2 ( 𝑚 = ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) → ( 2 · 𝑚 ) = ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) )
58 57 oveq1d ( 𝑚 = ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) → ( ( 2 · 𝑚 ) − 1 ) = ( ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) )
59 43 46 49 56 58 fsumshftm ( 𝑦 ∈ ℕ0 → Σ 𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑙 ∈ ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ... ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) ( ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) )
60 elfzelz ( 𝑘 ∈ ( 1 ... 𝑦 ) → 𝑘 ∈ ℤ )
61 60 adantl ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑦 ) ) → 𝑘 ∈ ℤ )
62 61 zred ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑦 ) ) → 𝑘 ∈ ℝ )
63 38 62 fsumrecl ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ℝ )
64 63 recnd ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ℂ )
65 1cnd ( 𝑦 ∈ ℕ0 → 1 ∈ ℂ )
66 64 65 pncan2d ( 𝑦 ∈ ℕ0 → ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) = 1 )
67 47 nn0cnd ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℂ )
68 64 67 pncan2d ( 𝑦 ∈ ℕ0 → ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) = ( 𝑦 + 1 ) )
69 66 68 oveq12d ( 𝑦 ∈ ℕ0 → ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ... ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
70 elfzelz ( 𝑙 ∈ ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ... ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) → 𝑙 ∈ ℤ )
71 70 zcnd ( 𝑙 ∈ ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ... ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) → 𝑙 ∈ ℂ )
72 2cnd ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → 2 ∈ ℂ )
73 simpr ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → 𝑙 ∈ ℂ )
74 64 adantr ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ℂ )
75 72 73 74 adddid ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) = ( ( 2 · 𝑙 ) + ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) )
76 75 oveq1d ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) = ( ( ( 2 · 𝑙 ) + ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) )
77 72 73 mulcld ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( 2 · 𝑙 ) ∈ ℂ )
78 72 74 mulcld ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ∈ ℂ )
79 1cnd ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → 1 ∈ ℂ )
80 77 78 79 addsubassd ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( ( ( 2 · 𝑙 ) + ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) = ( ( 2 · 𝑙 ) + ( ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) − 1 ) ) )
81 77 78 79 addsub12d ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( ( 2 · 𝑙 ) + ( ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) − 1 ) ) = ( ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) )
82 arisum ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 = ( ( ( 𝑦 ↑ 2 ) + 𝑦 ) / 2 ) )
83 82 oveq2d ( 𝑦 ∈ ℕ0 → ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) = ( 2 · ( ( ( 𝑦 ↑ 2 ) + 𝑦 ) / 2 ) ) )
84 nn0cn ( 𝑦 ∈ ℕ0𝑦 ∈ ℂ )
85 84 sqcld ( 𝑦 ∈ ℕ0 → ( 𝑦 ↑ 2 ) ∈ ℂ )
86 85 84 addcld ( 𝑦 ∈ ℕ0 → ( ( 𝑦 ↑ 2 ) + 𝑦 ) ∈ ℂ )
87 2cnd ( 𝑦 ∈ ℕ0 → 2 ∈ ℂ )
88 2ne0 2 ≠ 0
89 88 a1i ( 𝑦 ∈ ℕ0 → 2 ≠ 0 )
90 86 87 89 divcan2d ( 𝑦 ∈ ℕ0 → ( 2 · ( ( ( 𝑦 ↑ 2 ) + 𝑦 ) / 2 ) ) = ( ( 𝑦 ↑ 2 ) + 𝑦 ) )
91 binom21 ( 𝑦 ∈ ℂ → ( ( 𝑦 + 1 ) ↑ 2 ) = ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) + 1 ) )
92 84 91 syl ( 𝑦 ∈ ℕ0 → ( ( 𝑦 + 1 ) ↑ 2 ) = ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) + 1 ) )
93 92 oveq1d ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) = ( ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) + 1 ) − ( 𝑦 + 1 ) ) )
94 87 84 mulcld ( 𝑦 ∈ ℕ0 → ( 2 · 𝑦 ) ∈ ℂ )
95 85 94 addcld ( 𝑦 ∈ ℕ0 → ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) ∈ ℂ )
96 95 84 65 pnpcan2d ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) + 1 ) − ( 𝑦 + 1 ) ) = ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) − 𝑦 ) )
97 85 94 84 addsubassd ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) − 𝑦 ) = ( ( 𝑦 ↑ 2 ) + ( ( 2 · 𝑦 ) − 𝑦 ) ) )
98 84 2timesd ( 𝑦 ∈ ℕ0 → ( 2 · 𝑦 ) = ( 𝑦 + 𝑦 ) )
99 84 84 98 mvrladdd ( 𝑦 ∈ ℕ0 → ( ( 2 · 𝑦 ) − 𝑦 ) = 𝑦 )
100 99 oveq2d ( 𝑦 ∈ ℕ0 → ( ( 𝑦 ↑ 2 ) + ( ( 2 · 𝑦 ) − 𝑦 ) ) = ( ( 𝑦 ↑ 2 ) + 𝑦 ) )
101 97 100 eqtrd ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 ↑ 2 ) + ( 2 · 𝑦 ) ) − 𝑦 ) = ( ( 𝑦 ↑ 2 ) + 𝑦 ) )
102 93 96 101 3eqtrrd ( 𝑦 ∈ ℕ0 → ( ( 𝑦 ↑ 2 ) + 𝑦 ) = ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) )
103 83 90 102 3eqtrd ( 𝑦 ∈ ℕ0 → ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) = ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) )
104 103 adantr ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) = ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) )
105 104 oveq1d ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
106 81 105 eqtrd ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( ( 2 · 𝑙 ) + ( ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) − 1 ) ) = ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
107 76 80 106 3eqtrd ( ( 𝑦 ∈ ℕ0𝑙 ∈ ℂ ) → ( ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) = ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
108 71 107 sylan2 ( ( 𝑦 ∈ ℕ0𝑙 ∈ ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ... ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) ) → ( ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) = ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
109 69 108 sumeq12dv ( 𝑦 ∈ ℕ0 → Σ 𝑙 ∈ ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ... ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) − Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) ( ( 2 · ( 𝑙 + Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) − 1 ) = Σ 𝑙 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
110 59 109 eqtr2d ( 𝑦 ∈ ℕ0 → Σ 𝑙 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ( ( 2 · 𝑚 ) − 1 ) )
111 110 adantr ( ( 𝑦 ∈ ℕ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 ( ( 𝑦 ∈ ℕ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 ( 𝑦 ∈ ℕ0𝑦 ∈ ℕ0 )
114 fzfid ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → ( 1 ... 𝑘 ) ∈ Fin )
115 elfzelz ( 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) → 𝑘 ∈ ℤ )
116 115 zcnd ( 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) → 𝑘 ∈ ℂ )
117 116 sqcld ( 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) → ( 𝑘 ↑ 2 ) ∈ ℂ )
118 117 116 subcld ( 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) → ( ( 𝑘 ↑ 2 ) − 𝑘 ) ∈ ℂ )
119 2cnd ( 𝑙 ∈ ( 1 ... 𝑘 ) → 2 ∈ ℂ )
120 elfzelz ( 𝑙 ∈ ( 1 ... 𝑘 ) → 𝑙 ∈ ℤ )
121 120 zcnd ( 𝑙 ∈ ( 1 ... 𝑘 ) → 𝑙 ∈ ℂ )
122 119 121 mulcld ( 𝑙 ∈ ( 1 ... 𝑘 ) → ( 2 · 𝑙 ) ∈ ℂ )
123 1cnd ( 𝑙 ∈ ( 1 ... 𝑘 ) → 1 ∈ ℂ )
124 122 123 subcld ( 𝑙 ∈ ( 1 ... 𝑘 ) → ( ( 2 · 𝑙 ) − 1 ) ∈ ℂ )
125 addcl ( ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) ∈ ℂ ∧ ( ( 2 · 𝑙 ) − 1 ) ∈ ℂ ) → ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) ∈ ℂ )
126 118 124 125 syl2an ( ( 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) ∈ ℂ )
127 126 adantll ( ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) ∧ 𝑙 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) ∈ ℂ )
128 114 127 fsumcl ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) ∈ ℂ )
129 oveq2 ( 𝑘 = ( 𝑦 + 1 ) → ( 1 ... 𝑘 ) = ( 1 ... ( 𝑦 + 1 ) ) )
130 oveq1 ( 𝑘 = ( 𝑦 + 1 ) → ( 𝑘 ↑ 2 ) = ( ( 𝑦 + 1 ) ↑ 2 ) )
131 id ( 𝑘 = ( 𝑦 + 1 ) → 𝑘 = ( 𝑦 + 1 ) )
132 130 131 oveq12d ( 𝑘 = ( 𝑦 + 1 ) → ( ( 𝑘 ↑ 2 ) − 𝑘 ) = ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) )
133 132 oveq1d ( 𝑘 = ( 𝑦 + 1 ) → ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
134 133 adantr ( ( 𝑘 = ( 𝑦 + 1 ) ∧ 𝑙 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
135 129 134 sumeq12dv ( 𝑘 = ( 𝑦 + 1 ) → Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑙 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) )
136 113 128 135 fz1sump1 ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) + Σ 𝑙 ∈ ( 1 ... ( 𝑦 + 1 ) ) ( ( ( ( 𝑦 + 1 ) ↑ 2 ) − ( 𝑦 + 1 ) ) + ( ( 2 · 𝑙 ) − 1 ) ) ) )
137 136 adantr ( ( 𝑦 ∈ ℕ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 ( ( 𝑦 ∈ ℕ0𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → 𝑘 ∈ ℂ )
139 113 138 131 fz1sump1 ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 = ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) )
140 139 adantr ( ( 𝑦 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) → Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 = ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) )
141 140 oveq2d ( ( 𝑦 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) → ( 1 ... Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 ) = ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) )
142 141 sumeq1d ( ( 𝑦 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = Σ 𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ( ( 2 · 𝑚 ) − 1 ) )
143 63 ltp1d ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 < ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) )
144 fzdisj ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 < ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) → ( ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ∩ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) = ∅ )
145 143 144 syl ( 𝑦 ∈ ℕ0 → ( ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ∩ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) = ∅ )
146 nnuz ℕ = ( ℤ ‘ 1 )
147 45 146 eleqtrdi ( 𝑦 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ∈ ( ℤ ‘ 1 ) )
148 43 uzidd ( 𝑦 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ( ℤ ‘ Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) )
149 uzaddcl ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ∈ ( ℤ ‘ Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ∧ ( 𝑦 + 1 ) ∈ ℕ0 ) → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ∈ ( ℤ ‘ Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) )
150 148 47 149 syl2anc ( 𝑦 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ∈ ( ℤ ‘ Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) )
151 fzsplit2 ( ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ∈ ( ℤ ‘ 1 ) ∧ ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ∈ ( ℤ ‘ Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ) → ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) = ( ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ∪ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) )
152 147 150 151 syl2anc ( 𝑦 ∈ ℕ0 → ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) = ( ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ∪ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) )
153 fzfid ( 𝑦 ∈ ℕ0 → ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ∈ Fin )
154 2cnd ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → 2 ∈ ℂ )
155 elfzelz ( 𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) → 𝑚 ∈ ℤ )
156 155 zcnd ( 𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) → 𝑚 ∈ ℂ )
157 156 adantl ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → 𝑚 ∈ ℂ )
158 154 157 mulcld ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → ( 2 · 𝑚 ) ∈ ℂ )
159 1cnd ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → 1 ∈ ℂ )
160 158 159 subcld ( ( 𝑦 ∈ ℕ0𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ) → ( ( 2 · 𝑚 ) − 1 ) ∈ ℂ )
161 145 152 153 160 fsumsplit ( 𝑦 ∈ ℕ0 → Σ 𝑚 ∈ ( 1 ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ( ( 2 · 𝑚 ) − 1 ) = ( Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) + Σ 𝑚 ∈ ( ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + 1 ) ... ( Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 + ( 𝑦 + 1 ) ) ) ( ( 2 · 𝑚 ) − 1 ) ) )
162 161 adantr ( ( 𝑦 ∈ ℕ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 ( ( 𝑦 ∈ ℕ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 ( ( 𝑦 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... 𝑦 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑦 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) ) → Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... ( 𝑦 + 1 ) ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
165 164 ex ( 𝑦 ∈ ℕ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 ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) )
167 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
168 nnssnn0 ℕ ⊆ ℕ0
169 167 168 sstri ( 1 ... 𝑁 ) ⊆ ℕ0
170 169 a1i ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ⊆ ℕ0 )
171 170 sselda ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
172 nicomachus ( 𝑘 ∈ ℕ0 → Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = ( 𝑘 ↑ 3 ) )
173 171 172 syl ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = ( 𝑘 ↑ 3 ) )
174 173 sumeq2dv ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) Σ 𝑙 ∈ ( 1 ... 𝑘 ) ( ( ( 𝑘 ↑ 2 ) − 𝑘 ) + ( ( 2 · 𝑙 ) − 1 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 ↑ 3 ) )
175 fzfid ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
176 175 171 fsumnn0cl ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∈ ℕ0 )
177 oddnumth ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∈ ℕ0 → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ↑ 2 ) )
178 176 177 syl ( 𝑁 ∈ ℕ0 → Σ 𝑚 ∈ ( 1 ... Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) ( ( 2 · 𝑚 ) − 1 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ↑ 2 ) )
179 166 174 178 3eqtr3d ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 ↑ 3 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ↑ 2 ) )