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 {\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	2timesd	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N+N$$
25	24	oveq2d	$$⊢N\in \mathbb{N}\to N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^2-\left(N+N\right)$$
26	23	sqcld	$$⊢N\in \mathbb{N}\to N^2\in ℂ$$
27	26 23 23	subsub4d	$$⊢N\in \mathbb{N}\to N^2-N-N=N^2-\left(N+N\right)$$
28	25 27	eqtr4d	$$⊢N\in \mathbb{N}\to N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^2-N-N$$
29	28	oveq1d	$$⊢N\in \mathbb{N}\to N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=\left(N^2-N\right)-N+1$$
30		binom2sub1	$$⊢N\in ℂ\to {\left(N-1\right)}^2=N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
31	23 30	syl	$$⊢N\in \mathbb{N}\to {\left(N-1\right)}^2=N^2-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
32	26 23	subcld	$$⊢N\in \mathbb{N}\to N^2-N\in ℂ$$
33		1cnd	$$⊢N\in \mathbb{N}\to 1\in ℂ$$
34	32 23 33	subsubd	$$⊢N\in \mathbb{N}\to N^2-N-\left(N-1\right)=\left(N^2-N\right)-N+1$$
35	29 31 34	3eqtr4d	$$⊢N\in \mathbb{N}\to {\left(N-1\right)}^2=N^2-N-\left(N-1\right)$$
36	35	oveq1d	$$⊢N\in \mathbb{N}\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 \mathbb{N}\to N-1\in ℂ$$
40	32 39	npcand	$$⊢N\in \mathbb{N}\to \left(N^2-N-\left(N-1\right)\right)+N-1=N^2-N$$
41	36 40	eqtrd	$$⊢N\in \mathbb{N}\to {\left(N-1\right)}^2+N-1=N^2-N$$
42	41	oveq1d	$$⊢N\in \mathbb{N}\to \frac{{\left(N-1\right)}^2+N-1}{2}=\frac{N^2-N}{2}$$
43	22 42	eqtrd	$$⊢N\in \mathbb{N}\to \sum _{k=1}^{N-1}k=\frac{N^2-N}{2}$$
44	20 43	eqtrd	$$⊢N\in \mathbb{N}\to 0+\sum _{k=0+1}^{N-1}k=\frac{N^2-N}{2}$$
45	9 44	eqtrd	$$⊢N\in \mathbb{N}\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 \mathbb{Z}$$
52		peano2zm	$$⊢0\in \mathbb{Z}\to 0-1\in \mathbb{Z}$$
53	51 52	ax-mp	$$⊢0-1\in \mathbb{Z}$$
54		fzn	$$⊢\left(0\in \mathbb{Z}\wedge 0-1\in \mathbb{Z}\right)\to \left(0-1<0\leftrightarrow \left(0\dots 0-1\right)=\varnothing \right)$$
55	51 53 54	mp2an	$$⊢0-1<0\leftrightarrow \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 \mathbb{N}\vee N=0\right)\to \sum _{k=0}^{N-1}k=\frac{N^2-N}{2}$$
73	1 72	sylbi	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=0}^{N-1}k=\frac{N^2-N}{2}$$