Metamath Proof Explorer


Theorem nicomachus

Description: Nicomachus's Theorem. The sum of the odd numbers from N ^ 2 - N + 1 to N ^ 2 + N - 1 is N ^ 3 . Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem . (Contributed by SN, 21-Mar-2025)

Ref Expression
Assertion nicomachus ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) + ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝑁 ↑ 3 ) )

Proof

Step Hyp Ref Expression
1 fzfid ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
2 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
3 2 adantr ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
4 3 sqcld ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 ↑ 2 ) ∈ ℂ )
5 4 3 subcld ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑁 ↑ 2 ) − 𝑁 ) ∈ ℂ )
6 2cnd ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → 2 ∈ ℂ )
7 elfznn ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
8 7 nncnd ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
9 8 adantl ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
10 6 9 mulcld ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 · 𝑘 ) ∈ ℂ )
11 1cnd ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
12 10 11 subcld ( ( 𝑁 ∈ ℕ0𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 2 · 𝑘 ) − 1 ) ∈ ℂ )
13 1 5 12 fsumadd ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) + ( ( 2 · 𝑘 ) − 1 ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑁 ↑ 2 ) − 𝑁 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 2 · 𝑘 ) − 1 ) ) )
14 id ( 𝑁 ∈ ℕ0𝑁 ∈ ℕ0 )
15 2 sqcld ( 𝑁 ∈ ℕ0 → ( 𝑁 ↑ 2 ) ∈ ℂ )
16 15 2 subcld ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) ∈ ℂ )
17 14 16 fz1sumconst ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑁 ↑ 2 ) − 𝑁 ) = ( 𝑁 · ( ( 𝑁 ↑ 2 ) − 𝑁 ) ) )
18 2 15 2 subdid ( 𝑁 ∈ ℕ0 → ( 𝑁 · ( ( 𝑁 ↑ 2 ) − 𝑁 ) ) = ( ( 𝑁 · ( 𝑁 ↑ 2 ) ) − ( 𝑁 · 𝑁 ) ) )
19 df-3 3 = ( 2 + 1 )
20 19 oveq2i ( 𝑁 ↑ 3 ) = ( 𝑁 ↑ ( 2 + 1 ) )
21 2nn0 2 ∈ ℕ0
22 21 a1i ( 𝑁 ∈ ℕ0 → 2 ∈ ℕ0 )
23 2 22 expp1d ( 𝑁 ∈ ℕ0 → ( 𝑁 ↑ ( 2 + 1 ) ) = ( ( 𝑁 ↑ 2 ) · 𝑁 ) )
24 20 23 eqtrid ( 𝑁 ∈ ℕ0 → ( 𝑁 ↑ 3 ) = ( ( 𝑁 ↑ 2 ) · 𝑁 ) )
25 15 2 mulcomd ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ↑ 2 ) · 𝑁 ) = ( 𝑁 · ( 𝑁 ↑ 2 ) ) )
26 24 25 eqtr2d ( 𝑁 ∈ ℕ0 → ( 𝑁 · ( 𝑁 ↑ 2 ) ) = ( 𝑁 ↑ 3 ) )
27 2 sqvald ( 𝑁 ∈ ℕ0 → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
28 27 eqcomd ( 𝑁 ∈ ℕ0 → ( 𝑁 · 𝑁 ) = ( 𝑁 ↑ 2 ) )
29 26 28 oveq12d ( 𝑁 ∈ ℕ0 → ( ( 𝑁 · ( 𝑁 ↑ 2 ) ) − ( 𝑁 · 𝑁 ) ) = ( ( 𝑁 ↑ 3 ) − ( 𝑁 ↑ 2 ) ) )
30 17 18 29 3eqtrd ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑁 ↑ 2 ) − 𝑁 ) = ( ( 𝑁 ↑ 3 ) − ( 𝑁 ↑ 2 ) ) )
31 oddnumth ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 2 · 𝑘 ) − 1 ) = ( 𝑁 ↑ 2 ) )
32 30 31 oveq12d ( 𝑁 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑁 ↑ 2 ) − 𝑁 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 2 · 𝑘 ) − 1 ) ) = ( ( ( 𝑁 ↑ 3 ) − ( 𝑁 ↑ 2 ) ) + ( 𝑁 ↑ 2 ) ) )
33 3nn0 3 ∈ ℕ0
34 33 a1i ( 𝑁 ∈ ℕ0 → 3 ∈ ℕ0 )
35 2 34 expcld ( 𝑁 ∈ ℕ0 → ( 𝑁 ↑ 3 ) ∈ ℂ )
36 35 15 npcand ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 ↑ 3 ) − ( 𝑁 ↑ 2 ) ) + ( 𝑁 ↑ 2 ) ) = ( 𝑁 ↑ 3 ) )
37 13 32 36 3eqtrd ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) + ( ( 2 · 𝑘 ) − 1 ) ) = ( 𝑁 ↑ 3 ) )