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 ℕ_{0} \to \sum_{k = 1}^{N} (2 k - 1) = N^{2}$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
2		2cnd	$⊢ k \in (1 \dots N) \to 2 \in ℂ$
3		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
4	3	nncnd	$⊢ k \in (1 \dots N) \to k \in ℂ$
5	2 4	mulcld	$⊢ k \in (1 \dots N) \to 2 k \in ℂ$
6	5	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 2 k \in ℂ$
7		1cnd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 1 \in ℂ$
8	1 6 7	fsumsub	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} (2 k - 1) = \sum_{k = 1}^{N} 2 k - \sum_{k = 1}^{N} 1$
9		arisum	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} k = \frac{N^{2} + N}{2}$
10	9	oveq2d	$⊢ N \in ℕ_{0} \to 2 \sum_{k = 1}^{N} k = 2 (\frac{N^{2} + N}{2})$
11		2cnd	$⊢ N \in ℕ_{0} \to 2 \in ℂ$
12	4	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to k \in ℂ$
13	1 11 12	fsummulc2	$⊢ N \in ℕ_{0} \to 2 \sum_{k = 1}^{N} k = \sum_{k = 1}^{N} 2 k$
14		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
15	14	sqcld	$⊢ N \in ℕ_{0} \to N^{2} \in ℂ$
16	15 14	addcld	$⊢ N \in ℕ_{0} \to N^{2} + N \in ℂ$
17		2ne0	$⊢ 2 \neq 0$
18	17	a1i	$⊢ N \in ℕ_{0} \to 2 \neq 0$
19	16 11 18	divcan2d	$⊢ N \in ℕ_{0} \to 2 (\frac{N^{2} + N}{2}) = N^{2} + N$
20	10 13 19	3eqtr3d	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} 2 k = N^{2} + N$
21		id	$⊢ N \in ℕ_{0} \to N \in ℕ_{0}$
22		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
23	21 22	fz1sumconst	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} 1 = N \cdot 1$
24	14	mulridd	$⊢ N \in ℕ_{0} \to N \cdot 1 = N$
25	23 24	eqtrd	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} 1 = N$
26	20 25	oveq12d	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} 2 k - \sum_{k = 1}^{N} 1 = N^{2} + N - N$
27	15 14	pncand	$⊢ N \in ℕ_{0} \to N^{2} + N - N = N^{2}$
28	8 26 27	3eqtrd	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} (2 k - 1) = N^{2}$

Metamath Proof Explorer

Theorem oddnumth

Proof