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)

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 addid2d ⊢ ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 )
20 13 19 syl5eqr ⊢ ( 𝑁 ∈ ℕ → ( 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 2timesd ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
25 24 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) = ( ( 𝑁 ↑ 2 ) − ( 𝑁 + 𝑁 ) ) )
26 23 sqcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℂ )
27 26 23 23 subsub4d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) = ( ( 𝑁 ↑ 2 ) − ( 𝑁 + 𝑁 ) ) )
28 25 27 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) )
29 28 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) + 1 ) )
30 binom2sub1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) )
31 23 30 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) )
32 26 23 subcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − 𝑁 ) ∈ ℂ )
33 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
34 32 23 33 subsubd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) + 1 ) )
35 29 31 34 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) )
36 35 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) )
37 ax-1cn ⊢ 1 ∈ ℂ
38 subcl ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℂ )
39 23 37 38 sylancl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
40 32 39 npcand ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) = ( ( 𝑁 ↑ 2 ) − 𝑁 ) )
41 36 40 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) = ( ( 𝑁 ↑ 2 ) − 𝑁 ) )
42 41 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
43 22 42 eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
44 20 43 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
45 9 44 eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
46 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) = ( 0 − 1 ) )
47 46 oveq2d ⊢ ( 𝑁 = 0 → ( 0 ... ( 𝑁 − 1 ) ) = ( 0 ... ( 0 − 1 ) ) )
48 0re ⊢ 0 ∈ ℝ
49 ltm1 ⊢ ( 0 ∈ ℝ → ( 0 − 1 ) < 0 )
50 48 49 ax-mp ⊢ ( 0 − 1 ) < 0
51 0z ⊢ 0 ∈ ℤ
52 peano2zm ⊢ ( 0 ∈ ℤ → ( 0 − 1 ) ∈ ℤ )
53 51 52 ax-mp ⊢ ( 0 − 1 ) ∈ ℤ
54 fzn ⊢ ( ( 0 ∈ ℤ ∧ ( 0 − 1 ) ∈ ℤ ) → ( ( 0 − 1 ) < 0 ↔ ( 0 ... ( 0 − 1 ) ) = ∅ ) )
55 51 53 54 mp2an ⊢ ( ( 0 − 1 ) < 0 ↔ ( 0 ... ( 0 − 1 ) ) = ∅ )
56 50 55 mpbi ⊢ ( 0 ... ( 0 − 1 ) ) = ∅
57 47 56 syl6eq ⊢ ( 𝑁 = 0 → ( 0 ... ( 𝑁 − 1 ) ) = ∅ )
58 57 sumeq1d ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = Σ 𝑘 ∈ ∅ 𝑘 )
59 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝑘 = 0
60 58 59 syl6eq ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = 0 )
61 sq0i ⊢ ( 𝑁 = 0 → ( 𝑁 ↑ 2 ) = 0 )
62 id ⊢ ( 𝑁 = 0 → 𝑁 = 0 )
63 61 62 oveq12d ⊢ ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) = ( 0 − 0 ) )
64 0m0e0 ⊢ ( 0 − 0 ) = 0
65 63 64 syl6eq ⊢ ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) = 0 )
66 65 oveq1d ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) = ( 0 / 2 ) )
67 2cn ⊢ 2 ∈ ℂ
68 2ne0 ⊢ 2 ≠ 0
69 67 68 div0i ⊢ ( 0 / 2 ) = 0
70 66 69 syl6eq ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) = 0 )
71 60 70 eqtr4d ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
72 45 71 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
73 1 72 sylbi ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )