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) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
3		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
4	2 3	eleqtrdi	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{Z}}_{\ge 0}$$
5		elfznn0	$$⊢k\in \left(0\dots N-1\right)\to k\in {\mathbb{N}}_0$$
6	5	adantl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(0\dots N-1\right)\right)\to k\in {\mathbb{N}}_0$$
7	6	nn0cnd	$$⊢\left(N\in \mathbb{N}\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 \mathbb{N}\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 \mathbb{N}\to \left(1\dots N-1\right)\in \mathrm{Fin}$$
15		elfznn	$$⊢k\in \left(1\dots N-1\right)\to k\in \mathbb{N}$$
16	15	adantl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N-1\right)\right)\to k\in \mathbb{N}$$
17	16	nncnd	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N-1\right)\right)\to k\in ℂ$$
18	14 17	fsumcl	$$⊢N\in \mathbb{N}\to \sum _{k=1}^{N-1}k\in ℂ$$
19	18	addlidd	$$⊢N\in \mathbb{N}\to 0+\sum _{k=1}^{N-1}k=\sum _{k=1}^{N-1}k$$
20	13 19	eqtr3id	$$⊢N\in \mathbb{N}\to 0+\sum _{k=0+1}^{N-1}k=\sum _{k=1}^{N-1}k$$
21		arisum	$$⊢N-1\in {\mathbb{N}}_0\to \sum _{k=1}^{N-1}k=\frac{{\left(N-1\right)}^2+N-1}{2}$$
22	2 21	syl	$$⊢N\in \mathbb{N}\to \sum _{k=1}^{N-1}k=\frac{{\left(N-1\right)}^2+N-1}{2}$$
23		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
24	23	sqcld	$$⊢N\in \mathbb{N}\to N^2\in ℂ$$
25	24 23	subcld	$$⊢N\in \mathbb{N}\to N^2-N\in ℂ$$
26	2	nn0cnd	$$⊢N\in \mathbb{N}\to N-1\in ℂ$$
27	23	2timesd	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N+N$$
28	27	oveq2d	$$⊢N\in \mathbb{N}\to N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^2-\left(N+N\right)$$
29	24 23 23	subsub4d	$$⊢N\in \mathbb{N}\to N^2-N-N=N^2-\left(N+N\right)$$
30	28 29	eqtr4d	$$⊢N\in \mathbb{N}\to N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^2-N-N$$
31	30	oveq1d	$$⊢N\in \mathbb{N}\to N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=\left(N^2-N\right)-N+1$$
32		binom2sub1	$$⊢N\in ℂ\to {\left(N-1\right)}^2=N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
33	23 32	syl	$$⊢N\in \mathbb{N}\to {\left(N-1\right)}^2=N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
34		1cnd	$$⊢N\in \mathbb{N}\to 1\in ℂ$$
35	25 23 34	subsubd	$$⊢N\in \mathbb{N}\to N^2-N-\left(N-1\right)=\left(N^2-N\right)-N+1$$
36	31 33 35	3eqtr4d	$$⊢N\in \mathbb{N}\to {\left(N-1\right)}^2=N^2-N-\left(N-1\right)$$
37	25 26 36	mvrrsubd	$$⊢N\in \mathbb{N}\to {\left(N-1\right)}^2+N-1=N^2-N$$
38	37	oveq1d	$$⊢N\in \mathbb{N}\to \frac{{\left(N-1\right)}^2+N-1}{2}=\frac{N^2-N}{2}$$
39	22 38	eqtrd	$$⊢N\in \mathbb{N}\to \sum _{k=1}^{N-1}k=\frac{N^2-N}{2}$$
40	9 20 39	3eqtrd	$$⊢N\in \mathbb{N}\to \sum _{k=0}^{N-1}k=\frac{N^2-N}{2}$$
41		oveq1	$$⊢N=0\to N-1=0-1$$
42	41	oveq2d	$$⊢N=0\to \left(0\dots N-1\right)=\left(0\dots 0-1\right)$$
43		fz00m1	$$⊢\left(0\dots 0-1\right)=\varnothing$$
44	42 43	eqtrdi	$$⊢N=0\to \left(0\dots N-1\right)=\varnothing$$
45	44	sumeq1d	$$⊢N=0\to \sum _{k=0}^{N-1}k=\sum _{k\in \varnothing }k$$
46		sum0	$$⊢\sum _{k\in \varnothing }k=0$$
47	45 46	eqtrdi	$$⊢N=0\to \sum _{k=0}^{N-1}k=0$$
48		sq0i	$$⊢N=0\to N^2=0$$
49		id	$$⊢N=0\to N=0$$
50	48 49	oveq12d	$$⊢N=0\to N^2-N=0-0$$
51		0m0e0	$$⊢0-0=0$$
52	50 51	eqtrdi	$$⊢N=0\to N^2-N=0$$
53	52	oveq1d	$$⊢N=0\to \frac{N^2-N}{2}=\frac{0}{2}$$
54		2cn	$$⊢2\in ℂ$$
55		2ne0	$$⊢2\ne 0$$
56	54 55	div0i	$$⊢\frac{0}{2}=0$$
57	53 56	eqtrdi	$$⊢N=0\to \frac{N^2-N}{2}=0$$
58	47 57	eqtr4d	$$⊢N=0\to \sum _{k=0}^{N-1}k=\frac{N^2-N}{2}$$
59	40 58	jaoi	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \sum _{k=0}^{N-1}k=\frac{N^2-N}{2}$$
60	1 59	sylbi	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=0}^{N-1}k=\frac{N^2-N}{2}$$