Theorem arisum2 12010

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

Assertion

Ref	Expression
arisum2	|- ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )

Distinct variable group:   k, N

Proof of Theorem arisum2

Step	Hyp	Ref	Expression
1		elnn0 9371	. 2 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		nnm1nn0 9410	. . . . . 6 |- ( N e. NN -> ( N - 1 ) e. NN0 )
3		nn0uz 9757	. . . . . 6 |- NN0 = ( ZZ>= ` 0 )
4	2, 3	eleqtrdi 2322	. . . . 5 |- ( N e. NN -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
5		elfznn0 10310	. . . . . . 7 |- ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
6	5	adantl 277	. . . . . 6 |- ( ( N e. NN /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. NN0 )
7	6	nn0cnd 9424	. . . . 5 |- ( ( N e. NN /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. CC )
8		id 19	. . . . 5 |- ( k = 0 -> k = 0 )
9	4, 7, 8	fsum1p 11929	. . . 4 |- ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k ) )
10		1e0p1 9619	. . . . . . . . 9 |- 1 = ( 0 + 1 )
11	10	oveq1i 6011	. . . . . . . 8 |- ( 1 ... ( N - 1 ) ) = ( ( 0 + 1 ) ... ( N - 1 ) )
12	11	sumeq1i 11874	. . . . . . 7 |- sum_ k e. ( 1 ... ( N - 1 ) ) k = sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k
13	12	oveq2i 6012	. . . . . 6 |- ( 0 + sum_ k e. ( 1 ... ( N - 1 ) ) k ) = ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k )
14		1zzd 9473	. . . . . . . . 9 |- ( N e. NN -> 1 e. ZZ )
15	2	nn0zd 9567	. . . . . . . . 9 |- ( N e. NN -> ( N - 1 ) e. ZZ )
16	14, 15	fzfigd 10653	. . . . . . . 8 |- ( N e. NN -> ( 1 ... ( N - 1 ) ) e. Fin )
17		elfznn 10250	. . . . . . . . . 10 |- ( k e. ( 1 ... ( N - 1 ) ) -> k e. NN )
18	17	adantl 277	. . . . . . . . 9 |- ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. NN )
19	18	nncnd 9124	. . . . . . . 8 |- ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. CC )
20	16, 19	fsumcl 11911	. . . . . . 7 |- ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k e. CC )
21	20	addlidd 8296	. . . . . 6 |- ( N e. NN -> ( 0 + sum_ k e. ( 1 ... ( N - 1 ) ) k ) = sum_ k e. ( 1 ... ( N - 1 ) ) k )
22	13, 21	eqtr3id 2276	. . . . 5 |- ( N e. NN -> ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k ) = sum_ k e. ( 1 ... ( N - 1 ) ) k )
23		arisum 12009	. . . . . . 7 |- ( ( N - 1 ) e. NN0 -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) )
24	2, 23	syl 14	. . . . . 6 |- ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) )
25		nncn 9118	. . . . . . . . . . . . . 14 |- ( N e. NN -> N e. CC )
26	25	2timesd 9354	. . . . . . . . . . . . 13 |- ( N e. NN -> ( 2 x. N ) = ( N + N ) )
27	26	oveq2d 6017	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( N ^ 2 ) - ( 2 x. N ) ) = ( ( N ^ 2 ) - ( N + N ) ) )
28	25	sqcld 10893	. . . . . . . . . . . . 13 |- ( N e. NN -> ( N ^ 2 ) e. CC )
29	28, 25, 25	subsub4d 8488	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( ( N ^ 2 ) - N ) - N ) = ( ( N ^ 2 ) - ( N + N ) ) )
30	27, 29	eqtr4d 2265	. . . . . . . . . . 11 |- ( N e. NN -> ( ( N ^ 2 ) - ( 2 x. N ) ) = ( ( ( N ^ 2 ) - N ) - N ) )
31	30	oveq1d 6016	. . . . . . . . . 10 |- ( N e. NN -> ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) = ( ( ( ( N ^ 2 ) - N ) - N ) + 1 ) )
32		binom2sub1 10876	. . . . . . . . . . 11 |- ( N e. CC -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) )
33	25, 32	syl 14	. . . . . . . . . 10 |- ( N e. NN -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) )
34	28, 25	subcld 8457	. . . . . . . . . . 11 |- ( N e. NN -> ( ( N ^ 2 ) - N ) e. CC )
35		1cnd 8162	. . . . . . . . . . 11 |- ( N e. NN -> 1 e. CC )
36	34, 25, 35	subsubd 8485	. . . . . . . . . 10 |- ( N e. NN -> ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) = ( ( ( ( N ^ 2 ) - N ) - N ) + 1 ) )
37	31, 33, 36	3eqtr4d 2272	. . . . . . . . 9 |- ( N e. NN -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) )
38	37	oveq1d 6016	. . . . . . . 8 |- ( N e. NN -> ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) = ( ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) + ( N - 1 ) ) )
39		ax-1cn 8092	. . . . . . . . . 10 |- 1 e. CC
40		subcl 8345	. . . . . . . . . 10 |- ( ( N e. CC /\ 1 e. CC ) -> ( N - 1 ) e. CC )
41	25, 39, 40	sylancl 413	. . . . . . . . 9 |- ( N e. NN -> ( N - 1 ) e. CC )
42	34, 41	npcand 8461	. . . . . . . 8 |- ( N e. NN -> ( ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) + ( N - 1 ) ) = ( ( N ^ 2 ) - N ) )
43	38, 42	eqtrd 2262	. . . . . . 7 |- ( N e. NN -> ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) = ( ( N ^ 2 ) - N ) )
44	43	oveq1d 6016	. . . . . 6 |- ( N e. NN -> ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) = ( ( ( N ^ 2 ) - N ) / 2 ) )
45	24, 44	eqtrd 2262	. . . . 5 |- ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
46	22, 45	eqtrd 2262	. . . 4 |- ( N e. NN -> ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k ) = ( ( ( N ^ 2 ) - N ) / 2 ) )
47	9, 46	eqtrd 2262	. . 3 |- ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
48		oveq1 6008	. . . . . . . 8 |- ( N = 0 -> ( N - 1 ) = ( 0 - 1 ) )
49	48	oveq2d 6017	. . . . . . 7 |- ( N = 0 -> ( 0 ... ( N - 1 ) ) = ( 0 ... ( 0 - 1 ) ) )
50		0re 8146	. . . . . . . . 9 |- 0 e. RR
51		ltm1 8993	. . . . . . . . 9 |- ( 0 e. RR -> ( 0 - 1 ) < 0 )
52	50, 51	ax-mp 5	. . . . . . . 8 |- ( 0 - 1 ) < 0
53		0z 9457	. . . . . . . . 9 |- 0 e. ZZ
54		peano2zm 9484	. . . . . . . . . 10 |- ( 0 e. ZZ -> ( 0 - 1 ) e. ZZ )
55	53, 54	ax-mp 5	. . . . . . . . 9 |- ( 0 - 1 ) e. ZZ
56		fzn 10238	. . . . . . . . 9 |- ( ( 0 e. ZZ /\ ( 0 - 1 ) e. ZZ ) -> ( ( 0 - 1 ) < 0 <-> ( 0 ... ( 0 - 1 ) ) = (/) ) )
57	53, 55, 56	mp2an 426	. . . . . . . 8 |- ( ( 0 - 1 ) < 0 <-> ( 0 ... ( 0 - 1 ) ) = (/) )
58	52, 57	mpbi 145	. . . . . . 7 |- ( 0 ... ( 0 - 1 ) ) = (/)
59	49, 58	eqtrdi 2278	. . . . . 6 |- ( N = 0 -> ( 0 ... ( N - 1 ) ) = (/) )
60	59	sumeq1d 11877	. . . . 5 |- ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = sum_ k e. (/) k )
61		sum0 11899	. . . . 5 |- sum_ k e. (/) k = 0
62	60, 61	eqtrdi 2278	. . . 4 |- ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = 0 )
63		sq0i 10853	. . . . . . . 8 |- ( N = 0 -> ( N ^ 2 ) = 0 )
64		id 19	. . . . . . . 8 |- ( N = 0 -> N = 0 )
65	63, 64	oveq12d 6019	. . . . . . 7 |- ( N = 0 -> ( ( N ^ 2 ) - N ) = ( 0 - 0 ) )
66		0m0e0 9222	. . . . . . 7 |- ( 0 - 0 ) = 0
67	65, 66	eqtrdi 2278	. . . . . 6 |- ( N = 0 -> ( ( N ^ 2 ) - N ) = 0 )
68	67	oveq1d 6016	. . . . 5 |- ( N = 0 -> ( ( ( N ^ 2 ) - N ) / 2 ) = ( 0 / 2 ) )
69		2cn 9181	. . . . . 6 |- 2 e. CC
70		2ap0 9203	. . . . . 6 |- 2 # 0
71	69, 70	div0api 8893	. . . . 5 |- ( 0 / 2 ) = 0
72	68, 71	eqtrdi 2278	. . . 4 |- ( N = 0 -> ( ( ( N ^ 2 ) - N ) / 2 ) = 0 )
73	62, 72	eqtr4d 2265	. . 3 |- ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
74	47, 73	jaoi 721	. 2 |- ( ( N e. NN \/ N = 0 ) -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
75	1, 74	sylbi 121	1 |- ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 713   = wceq 1395   e. wcel 2200   (/)c0 3491   class class class wbr 4083   ` cfv 5318  (class class class)co 6001   CCcc 7997   RRcr 7998   0cc0 7999   1c1 8000   + caddc 8002   x. cmul 8004   < clt 8181   - cmin 8317   / cdiv 8819   NNcn 9110   2c2 9161   NN0cn0 9369   ZZcz 9446   ZZ>=cuz 9722   ...cfz 10204   ^cexp 10760   sum_csu 11864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4199  ax-sep 4202  ax-nul 4210  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-iinf 4680  ax-cnex 8090  ax-resscn 8091  ax-1cn 8092  ax-1re 8093  ax-icn 8094  ax-addcl 8095  ax-addrcl 8096  ax-mulcl 8097  ax-mulrcl 8098  ax-addcom 8099  ax-mulcom 8100  ax-addass 8101  ax-mulass 8102  ax-distr 8103  ax-i2m1 8104  ax-0lt1 8105  ax-1rid 8106  ax-0id 8107  ax-rnegex 8108  ax-precex 8109  ax-cnre 8110  ax-pre-ltirr 8111  ax-pre-ltwlin 8112  ax-pre-lttrn 8113  ax-pre-apti 8114  ax-pre-ltadd 8115  ax-pre-mulgt0 8116  ax-pre-mulext 8117  ax-arch 8118  ax-caucvg 8119

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-iun 3967  df-br 4084  df-opab 4146  df-mpt 4147  df-tr 4183  df-id 4384  df-po 4387  df-iso 4388  df-iord 4457  df-on 4459  df-ilim 4460  df-suc 4462  df-iom 4683  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-isom 5327  df-riota 5954  df-ov 6004  df-oprab 6005  df-mpo 6006  df-1st 6286  df-2nd 6287  df-recs 6451  df-irdg 6516  df-frec 6537  df-1o 6562  df-oadd 6566  df-er 6680  df-en 6888  df-dom 6889  df-fin 6890  df-pnf 8183  df-mnf 8184  df-xr 8185  df-ltxr 8186  df-le 8187  df-sub 8319  df-neg 8320  df-reap 8722  df-ap 8729  df-div 8820  df-inn 9111  df-2 9169  df-3 9170  df-4 9171  df-n0 9370  df-z 9447  df-uz 9723  df-q 9815  df-rp 9850  df-fz 10205  df-fzo 10339  df-seqfrec 10670  df-exp 10761  df-fac 10948  df-bc 10970  df-ihash 10998  df-cj 11353  df-re 11354  df-im 11355  df-rsqrt 11509  df-abs 11510  df-clim 11790  df-sumdc 11865

This theorem is referenced by: (None)