Metamath Proof Explorer

Theorem arisum2

Description: Arithmetic series sum of the first N nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 2-Aug-2021) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

Ref Expression
Assertion arisum2 ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
3 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4 2 3 eleqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
5 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
6 5 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
7 6 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
8 id ⊢ ( 𝑘 = 0 → 𝑘 = 0 )
9 4 7 8 fsum1p ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 ) )
10 1e0p1 ⊢ 1 = ( 0 + 1 )
11 10 oveq1i ⊢ ( 1 ... ( 𝑁 − 1 ) ) = ( ( 0 + 1 ) ... ( 𝑁 − 1 ) )
12 11 sumeq1i ⊢ Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘
13 12 oveq2i ⊢ ( 0 + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ) = ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 )
14 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin )
15 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ )
16 15 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ )
17 16 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
18 14 17 fsumcl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ∈ ℂ )
19 18 addlidd ⊢ ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 )
20 13 19 eqtr3id ⊢ ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 )
21 arisum ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) )
22 2 21 syl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) )
23 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
24 23 sqcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℂ )
25 24 23 subcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − 𝑁 ) ∈ ℂ )
26 2 nn0cnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
27 23 2timesd ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
28 27 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) = ( ( 𝑁 ↑ 2 ) − ( 𝑁 + 𝑁 ) ) )
29 24 23 23 subsub4d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) = ( ( 𝑁 ↑ 2 ) − ( 𝑁 + 𝑁 ) ) )
30 28 29 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) )
31 30 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) + 1 ) )
32 binom2sub1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) )
33 23 32 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) )
34 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
35 25 23 34 subsubd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) + 1 ) )
36 31 33 35 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) )
37 25 26 36 mvrrsubd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) = ( ( 𝑁 ↑ 2 ) − 𝑁 ) )
38 37 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
39 22 38 eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
40 9 20 39 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
41 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) = ( 0 − 1 ) )
42 41 oveq2d ⊢ ( 𝑁 = 0 → ( 0 ... ( 𝑁 − 1 ) ) = ( 0 ... ( 0 − 1 ) ) )
43 fz00m1 ⊢ ( 0 ... ( 0 − 1 ) ) = ∅
44 42 43 eqtrdi ⊢ ( 𝑁 = 0 → ( 0 ... ( 𝑁 − 1 ) ) = ∅ )
45 44 sumeq1d ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = Σ 𝑘 ∈ ∅ 𝑘 )
46 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝑘 = 0
47 45 46 eqtrdi ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = 0 )
48 sq0i ⊢ ( 𝑁 = 0 → ( 𝑁 ↑ 2 ) = 0 )
49 id ⊢ ( 𝑁 = 0 → 𝑁 = 0 )
50 48 49 oveq12d ⊢ ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) = ( 0 − 0 ) )
51 0m0e0 ⊢ ( 0 − 0 ) = 0
52 50 51 eqtrdi ⊢ ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) = 0 )
53 52 oveq1d ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) = ( 0 / 2 ) )
54 2cn ⊢ 2 ∈ ℂ
55 2ne0 ⊢ 2 ≠ 0
56 54 55 div0i ⊢ ( 0 / 2 ) = 0
57 53 56 eqtrdi ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) = 0 )
58 47 57 eqtr4d ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
59 40 58 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
60 1 59 sylbi ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )