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 15768

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 12386	. 2 ⊢ (𝑁 ∈ ℕ₀ ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nnm1nn0 12425	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
3		nn0uz 12777	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleqtrdi 2838	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ_≥‘0))
5		elfznn0 13523	. . . . . . 7 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
6	5	adantl 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ₀)
7	6	nn0cnd 12447	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ)
8		id 22	. . . . 5 ⊢ (𝑘 = 0 → 𝑘 = 0)
9	4, 7, 8	fsum1p 15660	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘))
10		1e0p1 12633	. . . . . . . . 9 ⊢ 1 = (0 + 1)
11	10	oveq1i 7359	. . . . . . . 8 ⊢ (1...(𝑁 − 1)) = ((0 + 1)...(𝑁 − 1))
12	11	sumeq1i 15604	. . . . . . 7 ⊢ Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘
13	12	oveq2i 7360	. . . . . 6 ⊢ (0 + Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘)
14		fzfid 13880	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (1...(𝑁 − 1)) ∈ Fin)
15		elfznn 13456	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
16	15	adantl 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ)
17	16	nncnd 12144	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℂ)
18	14, 17	fsumcl 15640	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 ∈ ℂ)
19	18	addlidd 11317	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (0 + Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘)
20	13, 19	eqtr3id 2778	. . . . 5 ⊢ (𝑁 ∈ ℕ → (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘)
21		arisum 15767	. . . . . . 7 ⊢ ((𝑁 − 1) ∈ ℕ₀ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2))
22	2, 21	syl 17	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2))
23		nncn 12136	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
24	23	2timesd 12367	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) = (𝑁 + 𝑁))
25	24	oveq2d 7365	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 · 𝑁)) = ((𝑁↑2) − (𝑁 + 𝑁)))
26	23	sqcld 14051	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈ ℂ)
27	26, 23, 23	subsub4d 11506	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − 𝑁) = ((𝑁↑2) − (𝑁 + 𝑁)))
28	25, 27	eqtr4d 2767	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 · 𝑁)) = (((𝑁↑2) − 𝑁) − 𝑁))
29	28	oveq1d 7364	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − (2 · 𝑁)) + 1) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1))
30		binom2sub1 14128	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 · 𝑁)) + 1))
31	23, 30	syl 17	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 · 𝑁)) + 1))
32	26, 23	subcld 11475	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − 𝑁) ∈ ℂ)
33		1cnd 11110	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
34	32, 23, 33	subsubd 11503	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1))
35	29, 31, 34	3eqtr4d 2774	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − 𝑁) − (𝑁 − 1)))
36	35	oveq1d 7364	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1)))
37		ax-1cn 11067	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
38		subcl 11362	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 − 1) ∈ ℂ)
39	23, 37, 38	sylancl 586	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
40	32, 39	npcand 11479	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁))
41	36, 40	eqtrd 2764	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁))
42	41	oveq1d 7364	. . . . . 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 7356	. . . . . . . 8 ⊢ (𝑁 = 0 → (𝑁 − 1) = (0 − 1))
47	46	oveq2d 7365	. . . . . . 7 ⊢ (𝑁 = 0 → (0...(𝑁 − 1)) = (0...(0 − 1)))
48		0re 11117	. . . . . . . . 9 ⊢ 0 ∈ ℝ
49		ltm1 11966	. . . . . . . . 9 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
50	48, 49	ax-mp 5	. . . . . . . 8 ⊢ (0 − 1) < 0
51		0z 12482	. . . . . . . . 9 ⊢ 0 ∈ ℤ
52		peano2zm 12518	. . . . . . . . . 10 ⊢ (0 ∈ ℤ → (0 − 1) ∈ ℤ)
53	51, 52	ax-mp 5	. . . . . . . . 9 ⊢ (0 − 1) ∈ ℤ
54		fzn 13443	. . . . . . . . 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 15607	. . . . 5 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ∅ 𝑘)
59		sum0 15628	. . . . 5 ⊢ Σ𝑘 ∈ ∅ 𝑘 = 0
60	58, 59	eqtrdi 2780	. . . 4 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = 0)
61		sq0i 14100	. . . . . . . 8 ⊢ (𝑁 = 0 → (𝑁↑2) = 0)
62		id 22	. . . . . . . 8 ⊢ (𝑁 = 0 → 𝑁 = 0)
63	61, 62	oveq12d 7367	. . . . . . 7 ⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = (0 − 0))
64		0m0e0 12243	. . . . . . 7 ⊢ (0 − 0) = 0
65	63, 64	eqtrdi 2780	. . . . . 6 ⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = 0)
66	65	oveq1d 7364	. . . . 5 ⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = (0 / 2))
67		2cn 12203	. . . . . 6 ⊢ 2 ∈ ℂ
68		2ne0 12232	. . . . . 6 ⊢ 2 ≠ 0
69	67, 68	div0i 11858	. . . . 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 4284 class class class wbr 5092 ‘cfv 6482 (class class class)co 7349 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 − cmin 11347 / cdiv 11777 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 ℤcz 12471 ℤ_≥cuz 12735 ...cfz 13410 ↑cexp 13968 Σcsu 15593

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 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

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 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-z 12472 df-uz 12736 df-rp 12894 df-fz 13411 df-fzo 13558 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594

This theorem is referenced by: birthdaylem3 26861

W3C validator