Theorem oddnumth

Description: The Odd Number Theorem. The sum of the first N odd numbers is N ^ 2 . A corollary of arisum . (Contributed by SN, 21-Mar-2025)

	Ref	Expression
Assertion	oddnumth	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(2k-1\right)=N^2$$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢N\in {\mathbb{N}}_0\to \left(1\dots N\right)\in \mathrm{Fin}$$
2		2cnd	$$⊢k\in \left(1\dots N\right)\to 2\in ℂ$$
3		elfznn	$$⊢k\in \left(1\dots N\right)\to k\in \mathbb{N}$$
4	3	nncnd	$$⊢k\in \left(1\dots N\right)\to k\in ℂ$$
5	2 4	mulcld	$$⊢k\in \left(1\dots N\right)\to 2k\in ℂ$$
6	5	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 2k\in ℂ$$
7		1cnd	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 1\in ℂ$$
8	1 6 7	fsumsub	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(2k-1\right)=\sum _{k=1}^{N}2k-\sum _{k=1}^{N}1$$
9		arisum	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^{N}k=\frac{N^2+N}{2}$$
10	9	oveq2d	$$⊢N\in {\mathbb{N}}_0\to 2\sum _{k=1}^{N}k=2\left(\frac{N^2+N}{2}\right)$$
11		2cnd	$$⊢N\in {\mathbb{N}}_0\to 2\in ℂ$$
12	4	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to k\in ℂ$$
13	1 11 12	fsummulc2	$$⊢N\in {\mathbb{N}}_0\to 2\sum _{k=1}^{N}k=\sum _{k=1}^{N}2k$$
14		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
15	14	sqcld	$$⊢N\in {\mathbb{N}}_0\to N^2\in ℂ$$
16	15 14	addcld	$$⊢N\in {\mathbb{N}}_0\to N^2+N\in ℂ$$
17		2ne0	$$⊢2\ne 0$$
18	17	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\ne 0$$
19	16 11 18	divcan2d	$$⊢N\in {\mathbb{N}}_0\to 2\left(\frac{N^2+N}{2}\right)=N^2+N$$
20	10 13 19	3eqtr3d	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^{N}2k=N^2+N$$
21		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
22		1cnd	$$⊢N\in {\mathbb{N}}_0\to 1\in ℂ$$
23	21 22	fz1sumconst	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^{N}1=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1$$
24	14	mulridd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1=N$$
25	23 24	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^{N}1=N$$
26	20 25	oveq12d	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^{N}2k-\sum _{k=1}^{N}1=N^2+N-N$$
27	15 14	pncand	$$⊢N\in {\mathbb{N}}_0\to N^2+N-N=N^2$$
28	8 26 27	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=1}^N\left(2k-1\right)=N^2$$