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 ) )