Metamath Proof Explorer


Theorem sum9cubes

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

Ref Expression
Assertion sum9cubes k = 1 9 k 3 = 2025

Proof

Step Hyp Ref Expression
1 9nn0 9 0
2 sumcubes 9 0 k = 1 9 k 3 = k = 1 9 k 2
3 1 2 ax-mp k = 1 9 k 3 = k = 1 9 k 2
4 arisum 9 0 k = 1 9 k = 9 2 + 9 2
5 1 4 ax-mp k = 1 9 k = 9 2 + 9 2
6 8nn0 8 0
7 1nn0 1 0
8 sq9 9 2 = 81
9 8p1e9 8 + 1 = 9
10 9cn 9
11 ax-1cn 1
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 0
16 4nn0 4 0
17 5nn0 5 0
18 eqid 45 = 45
19 0nn0 0 0
20 4t2e8 4 2 = 8
21 20 oveq1i 4 2 + 1 = 8 + 1
22 21 9 eqtri 4 2 + 1 = 9
23 5t2e10 5 2 = 10
24 15 16 17 18 19 7 22 23 decmul1c 45 2 = 90
25 14 24 eqtr4i 9 2 + 9 = 45 2
26 25 oveq1i 9 2 + 9 2 = 45 2 2
27 16 17 deccl 45 0
28 27 nn0cni 45
29 2cn 2
30 2ne0 2 0
31 28 29 30 divcan4i 45 2 2 = 45
32 5 26 31 3eqtri k = 1 9 k = 45
33 32 oveq1i k = 1 9 k 2 = 45 2
34 sq45 45 2 = 2025
35 3 33 34 3eqtri k = 1 9 k 3 = 2025