# Metamath Proof Explorer

## Theorem arisum2

Description: Arithmetic series sum of the first N nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 2-Aug-2021)

Ref Expression
Assertion arisum2 ${⊢}{N}\in {ℕ}_{0}\to \sum _{{k}=0}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$

### Proof

Step Hyp Ref Expression
1 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
2 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
3 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
4 2 3 eleqtrdi ${⊢}{N}\in ℕ\to {N}-1\in {ℤ}_{\ge 0}$
5 elfznn0 ${⊢}{k}\in \left(0\dots {N}-1\right)\to {k}\in {ℕ}_{0}$
6 5 adantl ${⊢}\left({N}\in ℕ\wedge {k}\in \left(0\dots {N}-1\right)\right)\to {k}\in {ℕ}_{0}$
7 6 nn0cnd ${⊢}\left({N}\in ℕ\wedge {k}\in \left(0\dots {N}-1\right)\right)\to {k}\in ℂ$
8 id ${⊢}{k}=0\to {k}=0$
9 4 7 8 fsum1p ${⊢}{N}\in ℕ\to \sum _{{k}=0}^{{N}-1}{k}=0+\sum _{{k}=0+1}^{{N}-1}{k}$
10 1e0p1 ${⊢}1=0+1$
11 10 oveq1i ${⊢}\left(1\dots {N}-1\right)=\left(0+1\dots {N}-1\right)$
12 11 sumeq1i ${⊢}\sum _{{k}=1}^{{N}-1}{k}=\sum _{{k}=0+1}^{{N}-1}{k}$
13 12 oveq2i ${⊢}0+\sum _{{k}=1}^{{N}-1}{k}=0+\sum _{{k}=0+1}^{{N}-1}{k}$
14 fzfid ${⊢}{N}\in ℕ\to \left(1\dots {N}-1\right)\in \mathrm{Fin}$
15 elfznn ${⊢}{k}\in \left(1\dots {N}-1\right)\to {k}\in ℕ$
16 15 adantl ${⊢}\left({N}\in ℕ\wedge {k}\in \left(1\dots {N}-1\right)\right)\to {k}\in ℕ$
17 16 nncnd ${⊢}\left({N}\in ℕ\wedge {k}\in \left(1\dots {N}-1\right)\right)\to {k}\in ℂ$
18 14 17 fsumcl ${⊢}{N}\in ℕ\to \sum _{{k}=1}^{{N}-1}{k}\in ℂ$
19 18 addid2d ${⊢}{N}\in ℕ\to 0+\sum _{{k}=1}^{{N}-1}{k}=\sum _{{k}=1}^{{N}-1}{k}$
20 13 19 syl5eqr ${⊢}{N}\in ℕ\to 0+\sum _{{k}=0+1}^{{N}-1}{k}=\sum _{{k}=1}^{{N}-1}{k}$
21 arisum ${⊢}{N}-1\in {ℕ}_{0}\to \sum _{{k}=1}^{{N}-1}{k}=\frac{{\left({N}-1\right)}^{2}+{N}-1}{2}$
22 2 21 syl ${⊢}{N}\in ℕ\to \sum _{{k}=1}^{{N}-1}{k}=\frac{{\left({N}-1\right)}^{2}+{N}-1}{2}$
23 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
24 23 2timesd ${⊢}{N}\in ℕ\to 2\cdot {N}={N}+{N}$
25 24 oveq2d ${⊢}{N}\in ℕ\to {{N}}^{2}-2\cdot {N}={{N}}^{2}-\left({N}+{N}\right)$
26 23 sqcld ${⊢}{N}\in ℕ\to {{N}}^{2}\in ℂ$
27 26 23 23 subsub4d ${⊢}{N}\in ℕ\to {{N}}^{2}-{N}-{N}={{N}}^{2}-\left({N}+{N}\right)$
28 25 27 eqtr4d ${⊢}{N}\in ℕ\to {{N}}^{2}-2\cdot {N}={{N}}^{2}-{N}-{N}$
29 28 oveq1d ${⊢}{N}\in ℕ\to {{N}}^{2}-2\cdot {N}+1=\left({{N}}^{2}-{N}\right)-{N}+1$
30 binom2sub1 ${⊢}{N}\in ℂ\to {\left({N}-1\right)}^{2}={{N}}^{2}-2\cdot {N}+1$
31 23 30 syl ${⊢}{N}\in ℕ\to {\left({N}-1\right)}^{2}={{N}}^{2}-2\cdot {N}+1$
32 26 23 subcld ${⊢}{N}\in ℕ\to {{N}}^{2}-{N}\in ℂ$
33 1cnd ${⊢}{N}\in ℕ\to 1\in ℂ$
34 32 23 33 subsubd ${⊢}{N}\in ℕ\to {{N}}^{2}-{N}-\left({N}-1\right)=\left({{N}}^{2}-{N}\right)-{N}+1$
35 29 31 34 3eqtr4d ${⊢}{N}\in ℕ\to {\left({N}-1\right)}^{2}={{N}}^{2}-{N}-\left({N}-1\right)$
36 35 oveq1d ${⊢}{N}\in ℕ\to {\left({N}-1\right)}^{2}+{N}-1=\left({{N}}^{2}-{N}-\left({N}-1\right)\right)+{N}-1$
37 ax-1cn ${⊢}1\in ℂ$
38 subcl ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\to {N}-1\in ℂ$
39 23 37 38 sylancl ${⊢}{N}\in ℕ\to {N}-1\in ℂ$
40 32 39 npcand ${⊢}{N}\in ℕ\to \left({{N}}^{2}-{N}-\left({N}-1\right)\right)+{N}-1={{N}}^{2}-{N}$
41 36 40 eqtrd ${⊢}{N}\in ℕ\to {\left({N}-1\right)}^{2}+{N}-1={{N}}^{2}-{N}$
42 41 oveq1d ${⊢}{N}\in ℕ\to \frac{{\left({N}-1\right)}^{2}+{N}-1}{2}=\frac{{{N}}^{2}-{N}}{2}$
43 22 42 eqtrd ${⊢}{N}\in ℕ\to \sum _{{k}=1}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$
44 20 43 eqtrd ${⊢}{N}\in ℕ\to 0+\sum _{{k}=0+1}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$
45 9 44 eqtrd ${⊢}{N}\in ℕ\to \sum _{{k}=0}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$
46 oveq1 ${⊢}{N}=0\to {N}-1=0-1$
47 46 oveq2d ${⊢}{N}=0\to \left(0\dots {N}-1\right)=\left(0\dots 0-1\right)$
48 0re ${⊢}0\in ℝ$
49 ltm1 ${⊢}0\in ℝ\to 0-1<0$
50 48 49 ax-mp ${⊢}0-1<0$
51 0z ${⊢}0\in ℤ$
52 peano2zm ${⊢}0\in ℤ\to 0-1\in ℤ$
53 51 52 ax-mp ${⊢}0-1\in ℤ$
54 fzn ${⊢}\left(0\in ℤ\wedge 0-1\in ℤ\right)\to \left(0-1<0↔\left(0\dots 0-1\right)=\varnothing \right)$
55 51 53 54 mp2an ${⊢}0-1<0↔\left(0\dots 0-1\right)=\varnothing$
56 50 55 mpbi ${⊢}\left(0\dots 0-1\right)=\varnothing$
57 47 56 eqtrdi ${⊢}{N}=0\to \left(0\dots {N}-1\right)=\varnothing$
58 57 sumeq1d ${⊢}{N}=0\to \sum _{{k}=0}^{{N}-1}{k}=\sum _{{k}\in \varnothing }{k}$
59 sum0 ${⊢}\sum _{{k}\in \varnothing }{k}=0$
60 58 59 eqtrdi ${⊢}{N}=0\to \sum _{{k}=0}^{{N}-1}{k}=0$
61 sq0i ${⊢}{N}=0\to {{N}}^{2}=0$
62 id ${⊢}{N}=0\to {N}=0$
63 61 62 oveq12d ${⊢}{N}=0\to {{N}}^{2}-{N}=0-0$
64 0m0e0 ${⊢}0-0=0$
65 63 64 eqtrdi ${⊢}{N}=0\to {{N}}^{2}-{N}=0$
66 65 oveq1d ${⊢}{N}=0\to \frac{{{N}}^{2}-{N}}{2}=\frac{0}{2}$
67 2cn ${⊢}2\in ℂ$
68 2ne0 ${⊢}2\ne 0$
69 67 68 div0i ${⊢}\frac{0}{2}=0$
70 66 69 eqtrdi ${⊢}{N}=0\to \frac{{{N}}^{2}-{N}}{2}=0$
71 60 70 eqtr4d ${⊢}{N}=0\to \sum _{{k}=0}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$
72 45 71 jaoi ${⊢}\left({N}\in ℕ\vee {N}=0\right)\to \sum _{{k}=0}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$
73 1 72 sylbi ${⊢}{N}\in {ℕ}_{0}\to \sum _{{k}=0}^{{N}-1}{k}=\frac{{{N}}^{2}-{N}}{2}$