esumval - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > esumval		Structured version Visualization version GIF version

Theorem esumval 34380

Description: Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.)

**Hypotheses**
Ref	Expression
esumval.p	⊢ Ⅎ𝑘𝜑
esumval.0	⊢ Ⅎ𝑘𝐴
esumval.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
esumval.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
esumval.3	⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶)

**Assertion**
Ref	Expression
esumval	⊢ (𝜑 → Σ^𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < ))

Distinct variable groups: 𝑥,𝑘 𝑥,𝐴 𝜑,𝑥 𝑥,𝐵 Allowed substitution hints: 𝜑(𝑘) 𝐴(𝑘) 𝐵(𝑘) 𝐶(𝑥,𝑘) 𝑉(𝑥,𝑘)

**Proof of Theorem esumval**
Step	Hyp	Ref	Expression
1		df-esum 34362	. . 3 ⊢ Σ^𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ^_𝑠 ↾_s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))
2		eqid 2769	. . . . 5 ⊢ (ℝ^_𝑠 ↾_s (0[,]+∞)) = (ℝ^_𝑠 ↾_s (0[,]+∞))
3		esumval.1	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		esumval.p	. . . . . 6 ⊢ Ⅎ𝑘𝜑
5		esumval.0	. . . . . 6 ⊢ Ⅎ𝑘𝐴
6		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑘(0[,]+∞)
7		esumval.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
8		eqid 2769	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
9	4, 5, 6, 7, 8	fmptdF 32941	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
10		inss1 4197	. . . . . . . . . . . . . 14 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
11	10	sseli 3941	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴)
12	11	elpwid 4576	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴)
13	12	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ 𝐴)
14		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝑥
15	5, 14	resmptf 6042	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥) = (𝑘 ∈ 𝑥 ↦ 𝐵))
16	13, 15	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥) = (𝑘 ∈ 𝑥 ↦ 𝐵))
17	16	oveq2d 7427	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ 𝑥 ↦ 𝐵)))
18		esumval.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶)
19	17, 18	eqtr2d 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐶 = ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥)))
20	19	mpteq2dva 5208	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥))))
21	20	rneqd 5929	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥))))
22	21	supeq1d 9405	. . . . 5 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < ) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑥))), ℝ^*, < ))
23	2, 3, 9, 22	xrge0tsmsd 33333	. . . 4 ⊢ (𝜑 → ((ℝ^_𝑠 ↾_s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) = {sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < )})
24	23	unieqd 4889	. . 3 ⊢ (𝜑 → ∪ ((ℝ^_𝑠 ↾_s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) = ∪ {sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < )})
25	1, 24	eqtrid 2816	. 2 ⊢ (𝜑 → Σ^𝑘 ∈ 𝐴𝐵 = ∪ {sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < )})
26		xrltso 13165	. . . 4 ⊢ < Or ℝ^*
27	26	supex 9423	. . 3 ⊢ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^*, < ) ∈ V
28	27	unisn 4895	. 2 ⊢ ∪ {sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < )} = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < )
29	25, 28	eqtrdi 2820	1 ⊢ (𝜑 → Σ^𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ^, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 Ⅎwnf 1810 ∈ wcel 2149 Ⅎwnfc 2916 ∩ cin 3912 ⊆ wss 3913 𝒫 cpw 4567 {csn 4594 ∪ cuni 4876 ↦ cmpt 5196 ran crn 5663 ↾ cres 5664 (class class class)co 7411 Fincfn 8942 supcsup 9399 0cc0 11099 +∞cpnf 11239 ℝ^*cxr 11241 < clt 11242 [,]cicc 13374 ↾_s cress 17289 Σ_g cgsu 17492 ℝ^*_𝑠cxrs 17553 tsums ctsu 24251 Σ^*cesum 34361

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-fi 9370 df-sup 9401 df-inf 9402 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-z 12591 df-dec 12711 df-uz 12862 df-q 12972 df-xadd 13137 df-ioo 13375 df-ioc 13376 df-ico 13377 df-icc 13378 df-fz 13535 df-fzo 13682 df-seq 14037 df-hash 14366 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-tset 17328 df-ple 17329 df-ds 17331 df-rest 17474 df-topn 17475 df-0g 17493 df-gsum 17494 df-topgen 17495 df-ordt 17554 df-xrs 17555 df-mre 17637 df-mrc 17638 df-acs 17640 df-ps 18621 df-tsr 18622 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-submnd 18841 df-cntz 19386 df-cmn 19851 df-fbas 21487 df-fg 21488 df-top 23019 df-topon 23036 df-topsp 23058 df-bases 23071 df-ntr 23145 df-nei 23223 df-cn 23352 df-haus 23440 df-fil 23971 df-fm 24063 df-flim 24064 df-flf 24065 df-tsms 24252 df-esum 34362

This theorem is referenced by: esumel 34381 esumnul 34382 esum0 34383 gsumesum 34393 esumlub 34394 esumcst 34397 esumpcvgval 34412 esumcvg 34420 esum2d 34427

W3C validator