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