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

### Proof

Step Hyp Ref Expression
1 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
2 1zzd ${⊢}{N}\in ℕ\to 1\in ℤ$
3 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
4 elfzelz ${⊢}{k}\in \left(1\dots {N}\right)\to {k}\in ℤ$
5 4 zcnd ${⊢}{k}\in \left(1\dots {N}\right)\to {k}\in ℂ$
6 5 adantl ${⊢}\left({N}\in ℕ\wedge {k}\in \left(1\dots {N}\right)\right)\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}\left({j}+1\right)$
9 1m1e0 ${⊢}1-1=0$
10 9 oveq1i ${⊢}\left(1-1\dots {N}-1\right)=\left(0\dots {N}-1\right)$
11 10 sumeq1i ${⊢}\sum _{{j}=1-1}^{{N}-1}\left({j}+1\right)=\sum _{{j}=0}^{{N}-1}\left({j}+1\right)$
12 8 11 eqtrdi ${⊢}{N}\in ℕ\to \sum _{{k}=1}^{{N}}{k}=\sum _{{j}=0}^{{N}-1}\left({j}+1\right)$
13 elfznn0 ${⊢}{j}\in \left(0\dots {N}-1\right)\to {j}\in {ℕ}_{0}$
14 13 adantl ${⊢}\left({N}\in ℕ\wedge {j}\in \left(0\dots {N}-1\right)\right)\to {j}\in {ℕ}_{0}$
15 bcnp1n ${⊢}{j}\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{{j}+1}{{j}}\right)={j}+1$
16 14 15 syl ${⊢}\left({N}\in ℕ\wedge {j}\in \left(0\dots {N}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{j}+1}{{j}}\right)={j}+1$
17 14 nn0cnd ${⊢}\left({N}\in ℕ\wedge {j}\in \left(0\dots {N}-1\right)\right)\to {j}\in ℂ$
18 ax-1cn ${⊢}1\in ℂ$
19 addcom ${⊢}\left({j}\in ℂ\wedge 1\in ℂ\right)\to {j}+1=1+{j}$
20 17 18 19 sylancl ${⊢}\left({N}\in ℕ\wedge {j}\in \left(0\dots {N}-1\right)\right)\to {j}+1=1+{j}$
21 20 oveq1d ${⊢}\left({N}\in ℕ\wedge {j}\in \left(0\dots {N}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{j}+1}{{j}}\right)=\left(\genfrac{}{}{0}{}{1+{j}}{{j}}\right)$
22 16 21 eqtr3d ${⊢}\left({N}\in ℕ\wedge {j}\in \left(0\dots {N}-1\right)\right)\to {j}+1=\left(\genfrac{}{}{0}{}{1+{j}}{{j}}\right)$
23 22 sumeq2dv ${⊢}{N}\in ℕ\to \sum _{{j}=0}^{{N}-1}\left({j}+1\right)=\sum _{{j}=0}^{{N}-1}\left(\genfrac{}{}{0}{}{1+{j}}{{j}}\right)$
24 1nn0 ${⊢}1\in {ℕ}_{0}$
25 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
26 bcxmas ${⊢}\left(1\in {ℕ}_{0}\wedge {N}-1\in {ℕ}_{0}\right)\to \left(\genfrac{}{}{0}{}{1+1+\left({N}-1\right)}{{N}-1}\right)=\sum _{{j}=0}^{{N}-1}\left(\genfrac{}{}{0}{}{1+{j}}{{j}}\right)$
27 24 25 26 sylancr ${⊢}{N}\in ℕ\to \left(\genfrac{}{}{0}{}{1+1+\left({N}-1\right)}{{N}-1}\right)=\sum _{{j}=0}^{{N}-1}\left(\genfrac{}{}{0}{}{1+{j}}{{j}}\right)$
28 23 27 eqtr4d ${⊢}{N}\in ℕ\to \sum _{{j}=0}^{{N}-1}\left({j}+1\right)=\left(\genfrac{}{}{0}{}{1+1+\left({N}-1\right)}{{N}-1}\right)$
29 1cnd ${⊢}{N}\in ℕ\to 1\in ℂ$
30 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
31 29 29 30 ppncand ${⊢}{N}\in ℕ\to 1+1+\left({N}-1\right)=1+{N}$
32 29 30 31 comraddd ${⊢}{N}\in ℕ\to 1+1+\left({N}-1\right)={N}+1$
33 32 oveq1d ${⊢}{N}\in ℕ\to \left(\genfrac{}{}{0}{}{1+1+\left({N}-1\right)}{{N}-1}\right)=\left(\genfrac{}{}{0}{}{{N}+1}{{N}-1}\right)$
34 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
35 bcp1m1 ${⊢}{N}\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{{N}+1}{{N}-1}\right)=\frac{\left({N}+1\right)\cdot {N}}{2}$
36 34 35 syl ${⊢}{N}\in ℕ\to \left(\genfrac{}{}{0}{}{{N}+1}{{N}-1}\right)=\frac{\left({N}+1\right)\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 \left({N}+1\right)\cdot {N}={{N}}^{2}+{N}$
43 42 oveq1d ${⊢}{N}\in ℕ\to \frac{\left({N}+1\right)\cdot {N}}{2}=\frac{{{N}}^{2}+{N}}{2}$
44 33 36 43 3eqtrd ${⊢}{N}\in ℕ\to \left(\genfrac{}{}{0}{}{1+1+\left({N}-1\right)}{{N}-1}\right)=\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 \left(1\dots {N}\right)=\left(1\dots 0\right)$
47 fz10 ${⊢}\left(1\dots 0\right)=\varnothing$
48 46 47 eqtrdi ${⊢}{N}=0\to \left(1\dots {N}\right)=\varnothing$
49 48 sumeq1d ${⊢}{N}=0\to \sum _{{k}=1}^{{N}}{k}=\sum _{{k}\in \varnothing }{k}$
50 sum0 ${⊢}\sum _{{k}\in \varnothing }{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\ne 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 ${⊢}\left({N}\in ℕ\vee {N}=0\right)\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}$