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\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(\left(N^2-N\right)+2k-1\right)=N^3$$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢N\in {\mathbb{N}}_0\to \left(1\dots N\right)\in \mathrm{Fin}$$
2		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
3	2	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to N\in ℂ$$
4	3	sqcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to N^2\in ℂ$$
5	4 3	subcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to N^2-N\in ℂ$$
6		2cnd	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 2\in ℂ$$
7		elfznn	$$⊢k\in \left(1\dots N\right)\to k\in \mathbb{N}$$
8	7	nncnd	$$⊢k\in \left(1\dots N\right)\to k\in ℂ$$
9	8	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to k\in ℂ$$
10	6 9	mulcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 2k\in ℂ$$
11		1cnd	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 1\in ℂ$$
12	10 11	subcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 2k-1\in ℂ$$
13	1 5 12	fsumadd	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(\left(N^2-N\right)+2k-1\right)=\sum _{k=1}^N\left(N^2-N\right)+\sum _{k=1}^N\left(2k-1\right)$$
14		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
15	2	sqcld	$$⊢N\in {\mathbb{N}}_0\to N^2\in ℂ$$
16	15 2	subcld	$$⊢N\in {\mathbb{N}}_0\to N^2-N\in ℂ$$
17	14 16	fz1sumconst	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(N^2-N\right)=N\left(N^2-N\right)$$
18	2 15 2	subdid	$$⊢N\in {\mathbb{N}}_0\to N\left(N^2-N\right)=N{N}^2-\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
19		df-3	$$⊢3=2+1$$
20	19	oveq2i	$$⊢N^3=N^{2+1}$$
21		2nn0	$$⊢2\in {\mathbb{N}}_0$$
22	21	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
23	2 22	expp1d	$$⊢N\in {\mathbb{N}}_0\to N^{2+1}=N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
24	20 23	eqtrid	$$⊢N\in {\mathbb{N}}_0\to N^3=N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
25	15 2	mulcomd	$$⊢N\in {\mathbb{N}}_0\to N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N{N}^2$$
26	24 25	eqtr2d	$$⊢N\in {\mathbb{N}}_0\to N{N}^2=N^3$$
27	2	sqvald	$$⊢N\in {\mathbb{N}}_0\to N^2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
28	27	eqcomd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^2$$
29	26 28	oveq12d	$$⊢N\in {\mathbb{N}}_0\to N{N}^2-\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^3-N^2$$
30	17 18 29	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(N^2-N\right)=N^3-N^2$$
31		oddnumth	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(2k-1\right)=N^2$$
32	30 31	oveq12d	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(N^2-N\right)+\sum _{k=1}^N\left(2k-1\right)=N^3-N^2+N^2$$
33		3nn0	$$⊢3\in {\mathbb{N}}_0$$
34	33	a1i	$$⊢N\in {\mathbb{N}}_0\to 3\in {\mathbb{N}}_0$$
35	2 34	expcld	$$⊢N\in {\mathbb{N}}_0\to N^3\in ℂ$$
36	35 15	npcand	$$⊢N\in {\mathbb{N}}_0\to N^3-N^2+N^2=N^3$$
37	13 32 36	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(\left(N^2-N\right)+2k-1\right)=N^3$$