Theorem esumpinfval 28401

Description: The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017.)

Hypotheses

Ref	Expression
esumpinfval.0	|- F/ k ph
esumpinfval.1	|- ( ph -> A e. V )
esumpinfval.2	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumpinfval.3	|- ( ph -> E. k e. A B = +oo )

Assertion

Ref	Expression
esumpinfval	|- ( ph -> Σ* k e. A B = +oo )

Distinct variable groups:   A, k   k, V

Allowed substitution hints:   ph( k)   B( k)

Proof of Theorem esumpinfval

Step	Hyp	Ref	Expression
1		iccssxr 11576	. . 3 |- ( 0 [,] +oo ) C_ RR*
2		esumpinfval.1	. . . 4 |- ( ph -> A e. V )
3		esumpinfval.0	. . . . 5 |- F/ k ph
4		esumpinfval.2	. . . . . 6 |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
5	4	ex 432	. . . . 5 |- ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
6	3, 5	ralrimi 2801	. . . 4 |- ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
7		nfcv 2562	. . . . 5 |- F/_ k A
8	7	esumcl 28358	. . . 4 |- ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> Σ* k e. A B e. ( 0 [,] +oo ) )
9	2, 6, 8	syl2anc 659	. . 3 |- ( ph -> Σ* k e. A B e. ( 0 [,] +oo ) )
10	1, 9	sseldi 3437	. 2 |- ( ph -> Σ* k e. A B e. RR* )
11		nfrab1 2985	. . . . 5 |- F/_ k { k e. A | B = +oo }
12		ssrab2 3521	. . . . . 6 |- { k e. A | B = +oo } C_ A
13	12	a1i 11	. . . . 5 |- ( ph -> { k e. A | B = +oo } C_ A )
14		0xr 9588	. . . . . . . 8 |- 0 e. RR*
15		pnfxr 11290	. . . . . . . 8 |- +oo e. RR*
16		0lepnf 11309	. . . . . . . 8 |- 0 <_ +oo
17		ubicc2 11606	. . . . . . . 8 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
18	14, 15, 16, 17	mp3an 1324	. . . . . . 7 |- +oo e. ( 0 [,] +oo )
19	18	a1i 11	. . . . . 6 |- ( ( ( ph /\ k e. A ) /\ B = +oo ) -> +oo e. ( 0 [,] +oo ) )
20		0e0iccpnf 11600	. . . . . . 7 |- 0 e. ( 0 [,] +oo )
21	20	a1i 11	. . . . . 6 |- ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> 0 e. ( 0 [,] +oo ) )
22	19, 21	ifclda 3914	. . . . 5 |- ( ( ph /\ k e. A ) -> if ( B = +oo , +oo , 0 ) e. ( 0 [,] +oo ) )
23		eldif 3421	. . . . . . . 8 |- ( k e. ( A \ { k e. A | B = +oo } ) <-> ( k e. A /\ -. k e. { k e. A | B = +oo } ) )
24		rabid 2981	. . . . . . . . . 10 |- ( k e. { k e. A | B = +oo } <-> ( k e. A /\ B = +oo ) )
25	24	simplbi2 623	. . . . . . . . 9 |- ( k e. A -> ( B = +oo -> k e. { k e. A | B = +oo } ) )
26	25	con3dimp 439	. . . . . . . 8 |- ( ( k e. A /\ -. k e. { k e. A | B = +oo } ) -> -. B = +oo )
27	23, 26	sylbi 195	. . . . . . 7 |- ( k e. ( A \ { k e. A | B = +oo } ) -> -. B = +oo )
28	27	adantl 464	. . . . . 6 |- ( ( ph /\ k e. ( A \ { k e. A | B = +oo } ) ) -> -. B = +oo )
29	28	iffalsed 3893	. . . . 5 |- ( ( ph /\ k e. ( A \ { k e. A | B = +oo } ) ) -> if ( B = +oo , +oo , 0 ) = 0 )
30	3, 11, 7, 13, 2, 22, 29	esumss 28400	. . . 4 |- ( ph -> Σ* k e. { k e. A | B = +oo } if ( B = +oo , +oo , 0 ) = Σ* k e. A if ( B = +oo , +oo , 0 ) )
31		eqidd 2401	. . . . . 6 |- ( ph -> { k e. A | B = +oo } = { k e. A | B = +oo } )
32	24	simprbi 462	. . . . . . . 8 |- ( k e. { k e. A | B = +oo } -> B = +oo )
33	32	iftrued 3890	. . . . . . 7 |- ( k e. { k e. A | B = +oo } -> if ( B = +oo , +oo , 0 ) = +oo )
34	33	adantl 464	. . . . . 6 |- ( ( ph /\ k e. { k e. A | B = +oo } ) -> if ( B = +oo , +oo , 0 ) = +oo )
35	3, 31, 34	esumeq12dvaf 28359	. . . . 5 |- ( ph -> Σ* k e. { k e. A | B = +oo } if ( B = +oo , +oo , 0 ) = Σ* k e. { k e. A | B = +oo } +oo )
36	2, 13	ssexd 4538	. . . . . 6 |- ( ph -> { k e. A | B = +oo } e. _V )
37		nfcv 2562	. . . . . . 7 |- F/_ k +oo
38	11, 37	esumcst 28391	. . . . . 6 |- ( ( { k e. A | B = +oo } e. _V /\ +oo e. ( 0 [,] +oo ) ) -> Σ* k e. { k e. A | B = +oo } +oo = ( ( # ` { k e. A | B = +oo } ) xe +oo ) )
39	36, 18, 38	sylancl 660	. . . . 5 |- ( ph -> Σ* k e. { k e. A | B = +oo } +oo = ( ( # ` { k e. A | B = +oo } ) xe +oo ) )
40		hashxrcl 12381	. . . . . . 7 |- ( { k e. A | B = +oo } e. _V -> ( # ` { k e. A | B = +oo } ) e. RR* )
41	36, 40	syl 17	. . . . . 6 |- ( ph -> ( # ` { k e. A | B = +oo } ) e. RR* )
42		esumpinfval.3	. . . . . . . 8 |- ( ph -> E. k e. A B = +oo )
43		rabn0 3756	. . . . . . . 8 |- ( { k e. A | B = +oo } =/= (/) <-> E. k e. A B = +oo )
44	42, 43	sylibr 212	. . . . . . 7 |- ( ph -> { k e. A | B = +oo } =/= (/) )
45		hashgt0 12409	. . . . . . 7 |- ( ( { k e. A | B = +oo } e. _V /\ { k e. A | B = +oo } =/= (/) ) -> 0 < ( # ` { k e. A | B = +oo } ) )
46	36, 44, 45	syl2anc 659	. . . . . 6 |- ( ph -> 0 < ( # ` { k e. A | B = +oo } ) )
47		xmulpnf1 11435	. . . . . 6 |- ( ( ( # ` { k e. A | B = +oo } ) e. RR* /\ 0 < ( # ` { k e. A | B = +oo } ) ) -> ( ( # ` { k e. A | B = +oo } ) xe +oo ) = +oo )
48	41, 46, 47	syl2anc 659	. . . . 5 |- ( ph -> ( ( # ` { k e. A | B = +oo } ) xe +oo ) = +oo )
49	35, 39, 48	3eqtrd 2445	. . . 4 |- ( ph -> Σ* k e. { k e. A | B = +oo } if ( B = +oo , +oo , 0 ) = +oo )
50	30, 49	eqtr3d 2443	. . 3 |- ( ph -> Σ* k e. A if ( B = +oo , +oo , 0 ) = +oo )
51		breq1 4395	. . . . 5 |- ( +oo = if ( B = +oo , +oo , 0 ) -> ( +oo <_ B <-> if ( B = +oo , +oo , 0 ) <_ B ) )
52		breq1 4395	. . . . 5 |- ( 0 = if ( B = +oo , +oo , 0 ) -> ( 0 <_ B <-> if ( B = +oo , +oo , 0 ) <_ B ) )
53		pnfge 11308	. . . . . . . 8 |- ( +oo e. RR* -> +oo <_ +oo )
54	15, 53	ax-mp 5	. . . . . . 7 |- +oo <_ +oo
55		breq2 4396	. . . . . . 7 |- ( B = +oo -> ( +oo <_ B <-> +oo <_ +oo ) )
56	54, 55	mpbiri 233	. . . . . 6 |- ( B = +oo -> +oo <_ B )
57	56	adantl 464	. . . . 5 |- ( ( ( ph /\ k e. A ) /\ B = +oo ) -> +oo <_ B )
58	4	adantr 463	. . . . . 6 |- ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> B e. ( 0 [,] +oo ) )
59		iccgelb 11550	. . . . . . 7 |- ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,] +oo ) ) -> 0 <_ B )
60	14, 15, 59	mp3an12 1314	. . . . . 6 |- ( B e. ( 0 [,] +oo ) -> 0 <_ B )
61	58, 60	syl 17	. . . . 5 |- ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> 0 <_ B )
62	51, 52, 57, 61	ifbothda 3917	. . . 4 |- ( ( ph /\ k e. A ) -> if ( B = +oo , +oo , 0 ) <_ B )
63	3, 7, 2, 22, 4, 62	esumlef 28390	. . 3 |- ( ph -> Σ* k e. A if ( B = +oo , +oo , 0 ) <_ Σ* k e. A B )
64	50, 63	eqbrtrrd 4414	. 2 |- ( ph -> +oo <_ Σ* k e. A B )
65		xgepnf 27892	. . 3 |- (Σ* k e. A B e. RR* -> ( +oo <_ Σ* k e. A B <-> Σ* k e. A B = +oo ) )
66	65	biimpd 207	. 2 |- (Σ* k e. A B e. RR* -> ( +oo <_ Σ* k e. A B -> Σ* k e. A B = +oo ) )
67	10, 64, 66	sylc 59	1 |- ( ph -> Σ* k e. A B = +oo )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   = wceq 1403   F/wnf 1635   e. wcel 1840   =/= wne 2596   A.wral 2751   E.wrex 2752   {crab 2755   _Vcvv 3056   \ cdif 3408   C_ wss 3411   (/)c0 3735   ifcif 3882   class class class wbr 4392   ` cfv 5523  (class class class)co 6232   0cc0 9440   +oocpnf 9573   RR*cxr 9575   < clt 9576   <_ cle 9577   xecxmu 11286   [,]cicc 11501   #chash 12357  Σ^*cesum 28355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4569  ax-pr 4627  ax-un 6528  ax-inf2 8009  ax-cnex 9496  ax-resscn 9497  ax-1cn 9498  ax-icn 9499  ax-addcl 9500  ax-addrcl 9501  ax-mulcl 9502  ax-mulrcl 9503  ax-mulcom 9504  ax-addass 9505  ax-mulass 9506  ax-distr 9507  ax-i2m1 9508  ax-1ne0 9509  ax-1rid 9510  ax-rnegex 9511  ax-rrecex 9512  ax-cnre 9513  ax-pre-lttri 9514  ax-pre-lttrn 9515  ax-pre-ltadd 9516  ax-pre-mulgt0 9517  ax-pre-sup 9518  ax-addf 9519  ax-mulf 9520

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 973  df-3an 974  df-tru 1406  df-fal 1409  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-nel 2599  df-ral 2756  df-rex 2757  df-reu 2758  df-rmo 2759  df-rab 2760  df-v 3058  df-sbc 3275  df-csb 3371  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-pss 3427  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-tp 3974  df-op 3976  df-uni 4189  df-int 4225  df-iun 4270  df-iin 4271  df-br 4393  df-opab 4451  df-mpt 4452  df-tr 4487  df-eprel 4731  df-id 4735  df-po 4741  df-so 4742  df-fr 4779  df-se 4780  df-we 4781  df-ord 4822  df-on 4823  df-lim 4824  df-suc 4825  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-f1 5528  df-fo 5529  df-f1o 5530  df-fv 5531  df-isom 5532  df-riota 6194  df-ov 6235  df-oprab 6236  df-mpt2 6237  df-of 6475  df-om 6637  df-1st 6736  df-2nd 6737  df-supp 6855  df-recs 6997  df-rdg 7031  df-1o 7085  df-2o 7086  df-oadd 7089  df-er 7266  df-map 7377  df-pm 7378  df-ixp 7426  df-en 7473  df-dom 7474  df-sdom 7475  df-fin 7476  df-fsupp 7782  df-fi 7823  df-sup 7853  df-oi 7887  df-card 8270  df-cda 8498  df-pnf 9578  df-mnf 9579  df-xr 9580  df-ltxr 9581  df-le 9582  df-sub 9761  df-neg 9762  df-div 10166  df-nn 10495  df-2 10553  df-3 10554  df-4 10555  df-5 10556  df-6 10557  df-7 10558  df-8 10559  df-9 10560  df-10 10561  df-n0 10755  df-z 10824  df-dec 10938  df-uz 11044  df-q 11144  df-rp 11182  df-xneg 11287  df-xadd 11288  df-xmul 11289  df-ioo 11502  df-ioc 11503  df-ico 11504  df-icc 11505  df-fz 11642  df-fzo 11766  df-fl 11877  df-mod 11946  df-seq 12060  df-exp 12119  df-fac 12306  df-bc 12333  df-hash 12358  df-shft 12954  df-cj 12986  df-re 12987  df-im 12988  df-sqrt 13122  df-abs 13123  df-limsup 13348  df-clim 13365  df-rlim 13366  df-sum 13563  df-ef 13902  df-sin 13904  df-cos 13905  df-pi 13907  df-struct 14733  df-ndx 14734  df-slot 14735  df-base 14736  df-sets 14737  df-ress 14738  df-plusg 14812  df-mulr 14813  df-starv 14814  df-sca 14815  df-vsca 14816  df-ip 14817  df-tset 14818  df-ple 14819  df-ds 14821  df-unif 14822  df-hom 14823  df-cco 14824  df-rest 14927  df-topn 14928  df-0g 14946  df-gsum 14947  df-topgen 14948  df-pt 14949  df-prds 14952  df-ordt 15005  df-xrs 15006  df-qtop 15011  df-imas 15012  df-xps 15014  df-mre 15090  df-mrc 15091  df-acs 15093  df-ps 16044  df-tsr 16045  df-plusf 16085  df-mgm 16086  df-sgrp 16125  df-mnd 16135  df-mhm 16180  df-submnd 16181  df-grp 16271  df-minusg 16272  df-sbg 16273  df-mulg 16274  df-subg 16412  df-cntz 16569  df-cmn 17014  df-abl 17015  df-mgp 17352  df-ur 17364  df-ring 17410  df-cring 17411  df-subrg 17637  df-abv 17676  df-lmod 17724  df-scaf 17725  df-sra 18028  df-rgmod 18029  df-psmet 18621  df-xmet 18622  df-met 18623  df-bl 18624  df-mopn 18625  df-fbas 18626  df-fg 18627  df-cnfld 18631  df-top 19581  df-bases 19583  df-topon 19584  df-topsp 19585  df-cld 19702  df-ntr 19703  df-cls 19704  df-nei 19782  df-lp 19820  df-perf 19821  df-cn 19911  df-cnp 19912  df-haus 19999  df-tx 20245  df-hmeo 20438  df-fil 20529  df-fm 20621  df-flim 20622  df-flf 20623  df-tmd 20753  df-tgp 20754  df-tsms 20807  df-trg 20844  df-xms 21005  df-ms 21006  df-tms 21007  df-nm 21285  df-ngp 21286  df-nrg 21288  df-nlm 21289  df-ii 21563  df-cncf 21564  df-limc 22452  df-dv 22453  df-log 23126  df-esum 28356

This theorem is referenced by:  hasheuni  28413  esumcvg  28414  esumcvgre  28419  voliune  28559  volfiniune  28560