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 
|- sum_ k e. ( 1 ... 9 ) ( k ^ 3 ) = ; ; ; 2 0 2 5

Proof

Step Hyp Ref Expression
1 9nn0 
 |-  9 e. NN0
2 sumcubes 
 |-  ( 9 e. NN0 -> sum_ k e. ( 1 ... 9 ) ( k ^ 3 ) = ( sum_ k e. ( 1 ... 9 ) k ^ 2 ) )
3 1 2 ax-mp 
 |-  sum_ k e. ( 1 ... 9 ) ( k ^ 3 ) = ( sum_ k e. ( 1 ... 9 ) k ^ 2 )
4 arisum 
 |-  ( 9 e. NN0 -> sum_ k e. ( 1 ... 9 ) k = ( ( ( 9 ^ 2 ) + 9 ) / 2 ) )
5 1 4 ax-mp 
 |-  sum_ k e. ( 1 ... 9 ) k = ( ( ( 9 ^ 2 ) + 9 ) / 2 )
6 8nn0 
 |-  8 e. NN0
7 1nn0 
 |-  1 e. NN0
8 sq9 
 |-  ( 9 ^ 2 ) = ; 8 1
9 8p1e9 
 |-  ( 8 + 1 ) = 9
10 9cn 
 |-  9 e. CC
11 ax-1cn 
 |-  1 e. CC
12 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
13 10 11 12 addcomli 
 |-  ( 1 + 9 ) = ; 1 0
14 6 7 1 8 9 13 decaddci2 
 |-  ( ( 9 ^ 2 ) + 9 ) = ; 9 0
15 2nn0 
 |-  2 e. NN0
16 4nn0 
 |-  4 e. NN0
17 5nn0 
 |-  5 e. NN0
18 eqid 
 |-  ; 4 5 = ; 4 5
19 0nn0 
 |-  0 e. NN0
20 4t2e8 
 |-  ( 4 x. 2 ) = 8
21 20 oveq1i 
 |-  ( ( 4 x. 2 ) + 1 ) = ( 8 + 1 )
22 21 9 eqtri 
 |-  ( ( 4 x. 2 ) + 1 ) = 9
23 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
24 15 16 17 18 19 7 22 23 decmul1c 
 |-  ( ; 4 5 x. 2 ) = ; 9 0
25 14 24 eqtr4i 
 |-  ( ( 9 ^ 2 ) + 9 ) = ( ; 4 5 x. 2 )
26 25 oveq1i 
 |-  ( ( ( 9 ^ 2 ) + 9 ) / 2 ) = ( ( ; 4 5 x. 2 ) / 2 )
27 16 17 deccl 
 |-  ; 4 5 e. NN0
28 27 nn0cni 
 |-  ; 4 5 e. CC
29 2cn 
 |-  2 e. CC
30 2ne0 
 |-  2 =/= 0
31 28 29 30 divcan4i 
 |-  ( ( ; 4 5 x. 2 ) / 2 ) = ; 4 5
32 5 26 31 3eqtri 
 |-  sum_ k e. ( 1 ... 9 ) k = ; 4 5
33 32 oveq1i 
 |-  ( sum_ k e. ( 1 ... 9 ) k ^ 2 ) = ( ; 4 5 ^ 2 )
34 sq45 
 |-  ( ; 4 5 ^ 2 ) = ; ; ; 2 0 2 5
35 3 33 34 3eqtri 
 |-  sum_ k e. ( 1 ... 9 ) ( k ^ 3 ) = ; ; ; 2 0 2 5