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	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N{k}^3={\sum _{k=1}^{N}k}^2$$

Proof

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