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	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} k = \frac{N^{2} + N}{2}$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		1zzd	$⊢ N \in ℕ \to 1 \in ℤ$
3		nnz	$⊢ N \in ℕ \to N \in ℤ$
4		elfzelz	$⊢ k \in (1 \dots N) \to k \in ℤ$
5	4	zcnd	$⊢ k \in (1 \dots N) \to k \in ℂ$
6	5	adantl	$⊢ (N \in ℕ \land k \in (1 \dots N)) \to k \in ℂ$
7		id	$⊢ k = j + 1 \to k = j + 1$
8	2 2 3 6 7	fsumshftm	$⊢ N \in ℕ \to \sum_{k = 1}^{N} k = \sum_{j = 1 - 1}^{N - 1} (j + 1)$
9		1m1e0	$⊢ 1 - 1 = 0$
10	9	oveq1i	$⊢ (1 - 1 \dots N - 1) = (0 \dots N - 1)$
11	10	sumeq1i	$⊢ \sum_{j = 1 - 1}^{N - 1} (j + 1) = \sum_{j = 0}^{N - 1} (j + 1)$
12	8 11	eqtrdi	$⊢ N \in ℕ \to \sum_{k = 1}^{N} k = \sum_{j = 0}^{N - 1} (j + 1)$
13		elfznn0	$⊢ j \in (0 \dots N - 1) \to j \in ℕ_{0}$
14	13	adantl	$⊢ (N \in ℕ \land j \in (0 \dots N - 1)) \to j \in ℕ_{0}$
15		bcnp1n	$⊢ j \in ℕ_{0} \to (\binom{j + 1}{j}) = j + 1$
16	14 15	syl	$⊢ (N \in ℕ \land j \in (0 \dots N - 1)) \to (\binom{j + 1}{j}) = j + 1$
17	14	nn0cnd	$⊢ (N \in ℕ \land j \in (0 \dots N - 1)) \to j \in ℂ$
18		ax-1cn	$⊢ 1 \in ℂ$
19		addcom	$⊢ (j \in ℂ \land 1 \in ℂ) \to j + 1 = 1 + j$
20	17 18 19	sylancl	$⊢ (N \in ℕ \land j \in (0 \dots N - 1)) \to j + 1 = 1 + j$
21	20	oveq1d	$⊢ (N \in ℕ \land j \in (0 \dots N - 1)) \to (\binom{j + 1}{j}) = (\binom{1 + j}{j})$
22	16 21	eqtr3d	$⊢ (N \in ℕ \land j \in (0 \dots N - 1)) \to j + 1 = (\binom{1 + j}{j})$
23	22	sumeq2dv	$⊢ N \in ℕ \to \sum_{j = 0}^{N - 1} (j + 1) = \sum_{j = 0}^{N - 1} (\binom{1 + j}{j})$
24		1nn0	$⊢ 1 \in ℕ_{0}$
25		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
26		bcxmas	$⊢ (1 \in ℕ_{0} \land N - 1 \in ℕ_{0}) \to (\binom{1 + 1 + (N - 1)}{N - 1}) = \sum_{j = 0}^{N - 1} (\binom{1 + j}{j})$
27	24 25 26	sylancr	$⊢ N \in ℕ \to (\binom{1 + 1 + (N - 1)}{N - 1}) = \sum_{j = 0}^{N - 1} (\binom{1 + j}{j})$
28	23 27	eqtr4d	$⊢ N \in ℕ \to \sum_{j = 0}^{N - 1} (j + 1) = (\binom{1 + 1 + (N - 1)}{N - 1})$
29		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
30		nncn	$⊢ N \in ℕ \to N \in ℂ$
31	29 29 30	ppncand	$⊢ N \in ℕ \to 1 + 1 + (N - 1) = 1 + N$
32	29 30 31	comraddd	$⊢ N \in ℕ \to 1 + 1 + (N - 1) = N + 1$
33	32	oveq1d	$⊢ N \in ℕ \to (\binom{1 + 1 + (N - 1)}{N - 1}) = (\binom{N + 1}{N - 1})$
34		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
35		bcp1m1	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N - 1}) = \frac{(N + 1) \cdot N}{2}$
36	34 35	syl	$⊢ N \in ℕ \to (\binom{N + 1}{N - 1}) = \frac{(N + 1) \cdot N}{2}$
37		sqval	$⊢ N \in ℂ \to N^{2} = N \cdot N$
38	37	eqcomd	$⊢ N \in ℂ \to N \cdot N = N^{2}$
39		mulid2	$⊢ N \in ℂ \to 1 \cdot N = N$
40	38 39	oveq12d	$⊢ N \in ℂ \to N \cdot N + 1 \cdot N = N^{2} + N$
41	30 40	syl	$⊢ N \in ℕ \to N \cdot N + 1 \cdot N = N^{2} + N$
42	30 30 29 41	joinlmuladdmuld	$⊢ N \in ℕ \to (N + 1) \cdot N = N^{2} + N$
43	42	oveq1d	$⊢ N \in ℕ \to \frac{(N + 1) \cdot N}{2} = \frac{N^{2} + N}{2}$
44	33 36 43	3eqtrd	$⊢ N \in ℕ \to (\binom{1 + 1 + (N - 1)}{N - 1}) = \frac{N^{2} + N}{2}$
45	12 28 44	3eqtrd	$⊢ N \in ℕ \to \sum_{k = 1}^{N} k = \frac{N^{2} + N}{2}$
46		oveq2	$⊢ N = 0 \to (1 \dots N) = (1 \dots 0)$
47		fz10	$⊢ (1 \dots 0) = \emptyset$
48	46 47	eqtrdi	$⊢ N = 0 \to (1 \dots N) = \emptyset$
49	48	sumeq1d	$⊢ N = 0 \to \sum_{k = 1}^{N} k = \sum_{k \in \emptyset} k$
50		sum0	$⊢ \sum_{k \in \emptyset} k = 0$
51	49 50	eqtrdi	$⊢ N = 0 \to \sum_{k = 1}^{N} k = 0$
52		sq0i	$⊢ N = 0 \to N^{2} = 0$
53		id	$⊢ N = 0 \to N = 0$
54	52 53	oveq12d	$⊢ N = 0 \to N^{2} + N = 0 + 0$
55		00id	$⊢ 0 + 0 = 0$
56	54 55	eqtrdi	$⊢ N = 0 \to N^{2} + N = 0$
57	56	oveq1d	$⊢ N = 0 \to \frac{N^{2} + N}{2} = \frac{0}{2}$
58		2cn	$⊢ 2 \in ℂ$
59		2ne0	$⊢ 2 \neq 0$
60	58 59	div0i	$⊢ \frac{0}{2} = 0$
61	57 60	eqtrdi	$⊢ N = 0 \to \frac{N^{2} + N}{2} = 0$
62	51 61	eqtr4d	$⊢ N = 0 \to \sum_{k = 1}^{N} k = \frac{N^{2} + N}{2}$
63	45 62	jaoi	$⊢ (N \in ℕ \lor N = 0) \to \sum_{k = 1}^{N} k = \frac{N^{2} + N}{2}$
64	1 63	sylbi	$⊢ N \in ℕ_{0} \to \sum_{k = 1}^{N} k = \frac{N^{2} + N}{2}$

Metamath Proof Explorer

Theorem arisum

Proof