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 N 0 k = 1 N N 2 N + 2 k - 1 = N 3

Proof

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