Theorem sum9cubes

Description: The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025)

	Ref	Expression
Assertion	sum9cubes	$$⊢\sum _{k=1}^9{k}^3=2025$$

Proof

Step	Hyp	Ref	Expression
1		9nn0	$$⊢9\in {\mathbb{N}}_0$$
2		sumcubes	$$⊢9\in {\mathbb{N}}_0\to \sum _{k=1}^9{k}^3={\sum _{k=1}^{9}k}^2$$
3	1 2	ax-mp	$$⊢\sum _{k=1}^9{k}^3={\sum _{k=1}^{9}k}^2$$
4		arisum	$$⊢9\in {\mathbb{N}}_0\to \sum _{k=1}^{9}k=\frac{9^2+9}{2}$$
5	1 4	ax-mp	$$⊢\sum _{k=1}^{9}k=\frac{9^2+9}{2}$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		sq9	$$⊢9^2=81$$
9		8p1e9	$$⊢8+1=9$$
10		9cn	$$⊢9\in ℂ$$
11		ax-1cn	$$⊢1\in ℂ$$
12		9p1e10	$$⊢9+1=10$$
13	10 11 12	addcomli	$$⊢1+9=10$$
14	6 7 1 8 9 13	decaddci2	$$⊢9^2+9=90$$
15		2nn0	$$⊢2\in {\mathbb{N}}_0$$
16		4nn0	$$⊢4\in {\mathbb{N}}_0$$
17		5nn0	$$⊢5\in {\mathbb{N}}_0$$
18		eqid	$$⊢45=45$$
19		0nn0	$$⊢0\in {\mathbb{N}}_0$$
20		4t2e8	$$⊢4\cdot 2=8$$
21	20	oveq1i	$$⊢4\cdot 2+1=8+1$$
22	21 9	eqtri	$$⊢4\cdot 2+1=9$$
23		5t2e10	$$⊢5\cdot 2=10$$
24	15 16 17 18 19 7 22 23	decmul1c	$$⊢45\cdot 2=90$$
25	14 24	eqtr4i	$$⊢9^2+9=45\cdot 2$$
26	25	oveq1i	$$⊢\frac{9^2+9}{2}=\frac{45\cdot 2}{2}$$
27	16 17	deccl	$$⊢45\in {\mathbb{N}}_0$$
28	27	nn0cni	$$⊢45\in ℂ$$
29		2cn	$$⊢2\in ℂ$$
30		2ne0	$$⊢2\ne 0$$
31	28 29 30	divcan4i	$$⊢\frac{45\cdot 2}{2}=45$$
32	5 26 31	3eqtri	$$⊢\sum _{k=1}^{9}k=45$$
33	32	oveq1i	$$⊢{\sum _{k=1}^{9}k}^2={45}^2$$
34		sq45	$$⊢{45}^2=2025$$
35	3 33 34	3eqtri	$$⊢\sum _{k=1}^9{k}^3=2025$$