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

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 mullid ⊢ ( 𝑁 ∈ ℂ → ( 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 ) )