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 Σ 𝑘 ∈ ( 1 ... 9 ) ( 𝑘 ↑ 3 ) = 2 0 2 5

Proof

Step Hyp Ref Expression
1 9nn0 9 ∈ ℕ0
2 sumcubes ( 9 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 9 ) ( 𝑘 ↑ 3 ) = ( Σ 𝑘 ∈ ( 1 ... 9 ) 𝑘 ↑ 2 ) )
3 1 2 ax-mp Σ 𝑘 ∈ ( 1 ... 9 ) ( 𝑘 ↑ 3 ) = ( Σ 𝑘 ∈ ( 1 ... 9 ) 𝑘 ↑ 2 )
4 arisum ( 9 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 9 ) 𝑘 = ( ( ( 9 ↑ 2 ) + 9 ) / 2 ) )
5 1 4 ax-mp Σ 𝑘 ∈ ( 1 ... 9 ) 𝑘 = ( ( ( 9 ↑ 2 ) + 9 ) / 2 )
6 8nn0 8 ∈ ℕ0
7 1nn0 1 ∈ ℕ0
8 sq9 ( 9 ↑ 2 ) = 8 1
9 8p1e9 ( 8 + 1 ) = 9
10 9cn 9 ∈ ℂ
11 ax-1cn 1 ∈ ℂ
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 ∈ ℕ0
16 4nn0 4 ∈ ℕ0
17 5nn0 5 ∈ ℕ0
18 eqid 4 5 = 4 5
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 ) = 1 0
24 15 16 17 18 19 7 22 23 decmul1c ( 4 5 · 2 ) = 9 0
25 14 24 eqtr4i ( ( 9 ↑ 2 ) + 9 ) = ( 4 5 · 2 )
26 25 oveq1i ( ( ( 9 ↑ 2 ) + 9 ) / 2 ) = ( ( 4 5 · 2 ) / 2 )
27 16 17 deccl 4 5 ∈ ℕ0
28 27 nn0cni 4 5 ∈ ℂ
29 2cn 2 ∈ ℂ
30 2ne0 2 ≠ 0
31 28 29 30 divcan4i ( ( 4 5 · 2 ) / 2 ) = 4 5
32 5 26 31 3eqtri Σ 𝑘 ∈ ( 1 ... 9 ) 𝑘 = 4 5
33 32 oveq1i ( Σ 𝑘 ∈ ( 1 ... 9 ) 𝑘 ↑ 2 ) = ( 4 5 ↑ 2 )
34 sq45 ( 4 5 ↑ 2 ) = 2 0 2 5
35 3 33 34 3eqtri Σ 𝑘 ∈ ( 1 ... 9 ) ( 𝑘 ↑ 3 ) = 2 0 2 5