arisum2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > arisum2		Structured version Visualization version GIF version

Theorem arisum2 15803

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

**Assertion**
Ref	Expression
arisum2	⊢ (𝑁 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2))

Distinct variable group: 𝑘,𝑁

**Proof of Theorem arisum2**
Step	Hyp	Ref	Expression
1		elnn0 12420	. 2 ⊢ (𝑁 ∈ ℕ₀ ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nnm1nn0 12459	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
3		nn0uz 12811	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleqtrdi 2838	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ_≥‘0))
5		elfznn0 13557	. . . . . . 7 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
6	5	adantl 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ₀)
7	6	nn0cnd 12481	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
8		id 22	. . . . 5 ⊢ (𝑘 = 0 → 𝑘 = 0)
9	4, 7, 8	fsum1p 15695	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘))
10		1e0p1 12667	. . . . . . . . 9 ⊢ 1 = (0 + 1)
11	10	oveq1i 7379	. . . . . . . 8 ⊢ (1...(𝑁 − 1)) = ((0 + 1)...(𝑁 − 1))
12	11	sumeq1i 15639	. . . . . . 7 ⊢ Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘
13	12	oveq2i 7380	. . . . . 6 ⊢ (0 + Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘)
14		fzfid 13914	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (1...(𝑁 − 1)) ∈ Fin)
15		elfznn 13490	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
16	15	adantl 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ)
17	16	nncnd 12178	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℂ)
18	14, 17	fsumcl 15675	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 ∈ ℂ)
19	18	addlidd 11351	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (0 + Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘)
20	13, 19	eqtr3id 2778	. . . . 5 ⊢ (𝑁 ∈ ℕ → (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘)
21		arisum 15802	. . . . . . 7 ⊢ ((𝑁 − 1) ∈ ℕ₀ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2))
22	2, 21	syl 17	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2))
23		nncn 12170	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
24	23	2timesd 12401	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) = (𝑁 + 𝑁))
25	24	oveq2d 7385	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 · 𝑁)) = ((𝑁↑2) − (𝑁 + 𝑁)))
26	23	sqcld 14085	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈ ℂ)
27	26, 23, 23	subsub4d 11540	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − 𝑁) = ((𝑁↑2) − (𝑁 + 𝑁)))
28	25, 27	eqtr4d 2767	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 · 𝑁)) = (((𝑁↑2) − 𝑁) − 𝑁))
29	28	oveq1d 7384	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − (2 · 𝑁)) + 1) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1))
30		binom2sub1 14162	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 · 𝑁)) + 1))
31	23, 30	syl 17	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 · 𝑁)) + 1))
32	26, 23	subcld 11509	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − 𝑁) ∈ ℂ)
33		1cnd 11145	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
34	32, 23, 33	subsubd 11537	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1))
35	29, 31, 34	3eqtr4d 2774	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − 𝑁) − (𝑁 − 1)))
36	35	oveq1d 7384	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1)))
37		ax-1cn 11102	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
38		subcl 11396	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 − 1) ∈ ℂ)
39	23, 37, 38	sylancl 586	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
40	32, 39	npcand 11513	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁))
41	36, 40	eqtrd 2764	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁))
42	41	oveq1d 7384	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2) = (((𝑁↑2) − 𝑁) / 2))
43	22, 42	eqtrd 2764	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2))
44	20, 43	eqtrd 2764	. . . 4 ⊢ (𝑁 ∈ ℕ → (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘) = (((𝑁↑2) − 𝑁) / 2))
45	9, 44	eqtrd 2764	. . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2))
46		oveq1 7376	. . . . . . . 8 ⊢ (𝑁 = 0 → (𝑁 − 1) = (0 − 1))
47	46	oveq2d 7385	. . . . . . 7 ⊢ (𝑁 = 0 → (0...(𝑁 − 1)) = (0...(0 − 1)))
48		0re 11152	. . . . . . . . 9 ⊢ 0 ∈ ℝ
49		ltm1 12000	. . . . . . . . 9 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
50	48, 49	ax-mp 5	. . . . . . . 8 ⊢ (0 − 1) < 0
51		0z 12516	. . . . . . . . 9 ⊢ 0 ∈ ℤ
52		peano2zm 12552	. . . . . . . . . 10 ⊢ (0 ∈ ℤ → (0 − 1) ∈ ℤ)
53	51, 52	ax-mp 5	. . . . . . . . 9 ⊢ (0 − 1) ∈ ℤ
54		fzn 13477	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) < 0 ↔ (0...(0 − 1)) = ∅))
55	51, 53, 54	mp2an 692	. . . . . . . 8 ⊢ ((0 − 1) < 0 ↔ (0...(0 − 1)) = ∅)
56	50, 55	mpbi 230	. . . . . . 7 ⊢ (0...(0 − 1)) = ∅
57	47, 56	eqtrdi 2780	. . . . . 6 ⊢ (𝑁 = 0 → (0...(𝑁 − 1)) = ∅)
58	57	sumeq1d 15642	. . . . 5 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ∅ 𝑘)
59		sum0 15663	. . . . 5 ⊢ Σ𝑘 ∈ ∅ 𝑘 = 0
60	58, 59	eqtrdi 2780	. . . 4 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = 0)
61		sq0i 14134	. . . . . . . 8 ⊢ (𝑁 = 0 → (𝑁↑2) = 0)
62		id 22	. . . . . . . 8 ⊢ (𝑁 = 0 → 𝑁 = 0)
63	61, 62	oveq12d 7387	. . . . . . 7 ⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = (0 − 0))
64		0m0e0 12277	. . . . . . 7 ⊢ (0 − 0) = 0
65	63, 64	eqtrdi 2780	. . . . . 6 ⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = 0)
66	65	oveq1d 7384	. . . . 5 ⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = (0 / 2))
67		2cn 12237	. . . . . 6 ⊢ 2 ∈ ℂ
68		2ne0 12266	. . . . . 6 ⊢ 2 ≠ 0
69	67, 68	div0i 11892	. . . . 5 ⊢ (0 / 2) = 0
70	66, 69	eqtrdi 2780	. . . 4 ⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = 0)
71	60, 70	eqtr4d 2767	. . 3 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2))
72	45, 71	jaoi 857	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2))
73	1, 72	sylbi 217	1 ⊢ (𝑁 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ∅c0 4292 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 ℂcc 11042 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 · cmul 11049 < clt 11184 − cmin 11381 / cdiv 11811 ℕcn 12162 2c2 12217 ℕ₀cn0 12418 ℤcz 12505 ℤ_≥cuz 12769 ...cfz 13444 ↑cexp 14002 Σcsu 15628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-rp 12928 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-fac 14215 df-bc 14244 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629

This theorem is referenced by: birthdaylem3 26839

W3C validator