Metamath Proof Explorer


Theorem arisum

Description: Arithmetic series sum of the first N positive integers. This is Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006) (Proof shortened by Mario Carneiro, 22-May-2014)

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

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 1zzd ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
3 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
4 elfzelz ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
5 4 zcnd ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
6 5 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
7 id ( 𝑘 = ( 𝑗 + 1 ) → 𝑘 = ( 𝑗 + 1 ) )
8 2 2 3 6 7 fsumshftm ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝑗 + 1 ) )
9 1m1e0 ( 1 − 1 ) = 0
10 9 oveq1i ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
11 10 sumeq1i Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝑗 + 1 ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑗 + 1 )
12 8 11 eqtrdi ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑗 + 1 ) )
13 elfznn0 ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℕ0 )
14 13 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℕ0 )
15 bcnp1n ( 𝑗 ∈ ℕ0 → ( ( 𝑗 + 1 ) C 𝑗 ) = ( 𝑗 + 1 ) )
16 14 15 syl ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) C 𝑗 ) = ( 𝑗 + 1 ) )
17 14 nn0cnd ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℂ )
18 ax-1cn 1 ∈ ℂ
19 addcom ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑗 + 1 ) = ( 1 + 𝑗 ) )
20 17 18 19 sylancl ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) = ( 1 + 𝑗 ) )
21 20 oveq1d ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) C 𝑗 ) = ( ( 1 + 𝑗 ) C 𝑗 ) )
22 16 21 eqtr3d ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) = ( ( 1 + 𝑗 ) C 𝑗 ) )
23 22 sumeq2dv ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑗 + 1 ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 + 𝑗 ) C 𝑗 ) )
24 1nn0 1 ∈ ℕ0
25 nnm1nn0 ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
26 bcxmas ( ( 1 ∈ ℕ0 ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) C ( 𝑁 − 1 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 + 𝑗 ) C 𝑗 ) )
27 24 25 26 sylancr ( 𝑁 ∈ ℕ → ( ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) C ( 𝑁 − 1 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 + 𝑗 ) C 𝑗 ) )
28 23 27 eqtr4d ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑗 + 1 ) = ( ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) C ( 𝑁 − 1 ) ) )
29 1cnd ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
30 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
31 29 29 30 ppncand ( 𝑁 ∈ ℕ → ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) = ( 1 + 𝑁 ) )
32 29 30 31 comraddd ( 𝑁 ∈ ℕ → ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) = ( 𝑁 + 1 ) )
33 32 oveq1d ( 𝑁 ∈ ℕ → ( ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) C ( 𝑁 − 1 ) ) = ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) )
34 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
35 bcp1m1 ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )
36 34 35 syl ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) C ( 𝑁 − 1 ) ) = ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) )
37 sqval ( 𝑁 ∈ ℂ → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
38 37 eqcomd ( 𝑁 ∈ ℂ → ( 𝑁 · 𝑁 ) = ( 𝑁 ↑ 2 ) )
39 mulid2 ( 𝑁 ∈ ℂ → ( 1 · 𝑁 ) = 𝑁 )
40 38 39 oveq12d ( 𝑁 ∈ ℂ → ( ( 𝑁 · 𝑁 ) + ( 1 · 𝑁 ) ) = ( ( 𝑁 ↑ 2 ) + 𝑁 ) )
41 30 40 syl ( 𝑁 ∈ ℕ → ( ( 𝑁 · 𝑁 ) + ( 1 · 𝑁 ) ) = ( ( 𝑁 ↑ 2 ) + 𝑁 ) )
42 30 30 29 41 joinlmuladdmuld ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) · 𝑁 ) = ( ( 𝑁 ↑ 2 ) + 𝑁 ) )
43 42 oveq1d ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) · 𝑁 ) / 2 ) = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
44 33 36 43 3eqtrd ( 𝑁 ∈ ℕ → ( ( ( 1 + 1 ) + ( 𝑁 − 1 ) ) C ( 𝑁 − 1 ) ) = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
45 12 28 44 3eqtrd ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
46 oveq2 ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ( 1 ... 0 ) )
47 fz10 ( 1 ... 0 ) = ∅
48 46 47 eqtrdi ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ∅ )
49 48 sumeq1d ( 𝑁 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = Σ 𝑘 ∈ ∅ 𝑘 )
50 sum0 Σ 𝑘 ∈ ∅ 𝑘 = 0
51 49 50 eqtrdi ( 𝑁 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = 0 )
52 sq0i ( 𝑁 = 0 → ( 𝑁 ↑ 2 ) = 0 )
53 id ( 𝑁 = 0 → 𝑁 = 0 )
54 52 53 oveq12d ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) + 𝑁 ) = ( 0 + 0 ) )
55 00id ( 0 + 0 ) = 0
56 54 55 eqtrdi ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) + 𝑁 ) = 0 )
57 56 oveq1d ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) = ( 0 / 2 ) )
58 2cn 2 ∈ ℂ
59 2ne0 2 ≠ 0
60 58 59 div0i ( 0 / 2 ) = 0
61 57 60 eqtrdi ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) = 0 )
62 51 61 eqtr4d ( 𝑁 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
63 45 62 jaoi ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
64 1 63 sylbi ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )