This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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