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	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 2 · 𝑘 ) − 1 ) = ( 𝑁 ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
2		2cnd	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 2 ∈ ℂ )
3		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
4	3	nncnd	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
5	2 4	mulcld	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 2 · 𝑘 ) ∈ ℂ )
6	5	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 · 𝑘 ) ∈ ℂ )
7		1cnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
8	1 6 7	fsumsub	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 2 · 𝑘 ) − 1 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 2 · 𝑘 ) − Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 ) )
9		arisum	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
10	9	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) = ( 2 · ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) ) )
11		2cnd	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
12	4	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
13	1 11 12	fsummulc2	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 2 · 𝑘 ) )
14		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
15	14	sqcld	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ↑ 2 ) ∈ ℂ )
16	15 14	addcld	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ↑ 2 ) + 𝑁 ) ∈ ℂ )
17		2ne0	⊢ 2 ≠ 0
18	17	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ≠ 0 )
19	16 11 18	divcan2d	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) ) = ( ( 𝑁 ↑ 2 ) + 𝑁 ) )
20	10 13 19	3eqtr3d	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 2 · 𝑘 ) = ( ( 𝑁 ↑ 2 ) + 𝑁 ) )
21		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
22		1cnd	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
23	21 22	fz1sumconst	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 = ( 𝑁 · 1 ) )
24	14	mulridd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 · 1 ) = 𝑁 )
25	23 24	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 = 𝑁 )
26	20 25	oveq12d	⊢ ( 𝑁 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 2 · 𝑘 ) − Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 ) = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) − 𝑁 ) )
27	15 14	pncand	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) − 𝑁 ) = ( 𝑁 ↑ 2 ) )
28	8 26 27	3eqtrd	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 2 · 𝑘 ) − 1 ) = ( 𝑁 ↑ 2 ) )