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