This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )