Metamath Proof Explorer


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 ) )