esumlub

Description: The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017) (Proof shortened by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	esumlub.f	\|- F/ k ph
	esumlub.0	\|- ( ph -> A e. V )
	esumlub.1	\|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
	esumlub.2	\|- ( ph -> X e. RR* )
	esumlub.3	\|- ( ph -> X < sum* k e. A B )
Assertion	esumlub	\|- ( ph -> E. a e. ( ~P A i^i Fin ) X < sum* k e. a B )

Proof

Step	Hyp	Ref	Expression
1		esumlub.f	\|- F/ k ph
2		esumlub.0	\|- ( ph -> A e. V )
3		esumlub.1	\|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4		esumlub.2	\|- ( ph -> X e. RR* )
5		esumlub.3	\|- ( ph -> X < sum* k e. A B )
6		nfcv	\|- F/_ k A
7		eqidd	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) )
8	1 6 2 3 7	esumval	\|- ( ph -> sum* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) , RR , < ) )
9	8	breq2d	\|- ( ph -> ( X < sum* k e. A B <-> X < sup ( ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) , RR , < ) ) )
10		iccssxr	\|- ( 0 [,] +oo ) C_ RR*
11		xrge0base	\|- ( 0 [,] +oo ) = ( Base ` ( RR*s \|`s ( 0 [,] +oo ) ) )
12		xrge0cmn	\|- ( RR*s \|`s ( 0 [,] +oo ) ) e. CMnd
13	12	a1i	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( RR*s \|`s ( 0 [,] +oo ) ) e. CMnd )
14		inss2	\|- ( ~P A i^i Fin ) C_ Fin
15		simpr	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
16	14 15	sseldi	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
17		nfv	\|- F/ k x e. ( ~P A i^i Fin )
18	1 17	nfan	\|- F/ k ( ph /\ x e. ( ~P A i^i Fin ) )
19		simpll	\|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ph )
20		inss1	\|- ( ~P A i^i Fin ) C_ ~P A
21	20	sseli	\|- ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
22	21	ad2antlr	\|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> x e. ~P A )
23	22	elpwid	\|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> x C_ A )
24		simpr	\|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. x )
25	23 24	sseldd	\|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. A )
26	19 25 3	syl2anc	\|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> B e. ( 0 [,] +oo ) )
27	26	ex	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( k e. x -> B e. ( 0 [,] +oo ) ) )
28	18 27	ralrimi	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> A. k e. x B e. ( 0 [,] +oo ) )
29	11 13 16 28	gsummptcl	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) e. ( 0 [,] +oo ) )
30	10 29	sseldi	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) e. RR )
31	30	ralrimiva	\|- ( ph -> A. x e. ( ~P A i^i Fin ) ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) e. RR )
32		eqid	\|- ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) = ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) )
33	32	rnmptss	\|- ( A. x e. ( ~P A i^i Fin ) ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) e. RR -> ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) C_ RR )
34	31 33	syl	\|- ( ph -> ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) C_ RR )
35		supxrlub	\|- ( ( ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) C_ RR /\ X e. RR* ) -> ( X < sup ( ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) , RR , < ) <-> E. y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) X < y ) )
36	34 4 35	syl2anc	\|- ( ph -> ( X < sup ( ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) , RR , < ) <-> E. y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) X < y ) )
37	9 36	bitrd	\|- ( ph -> ( X < sum* k e. A B <-> E. y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) X < y ) )
38	5 37	mpbid	\|- ( ph -> E. y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) X < y )
39		ovex	\|- ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) e. _V
40	39	a1i	\|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) e. _V )
41		mpteq1	\|- ( x = a -> ( k e. x \|-> B ) = ( k e. a \|-> B ) )
42	41	oveq2d	\|- ( x = a -> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) )
43	42	cbvmptv	\|- ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) = ( a e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) )
44	43 39	elrnmpti	\|- ( y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) <-> E. a e. ( ~P A i^i Fin ) y = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) )
45	44	a1i	\|- ( ph -> ( y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) <-> E. a e. ( ~P A i^i Fin ) y = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) ) )
46		simpr	\|- ( ( ph /\ y = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) ) -> y = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) )
47	46	breq2d	\|- ( ( ph /\ y = ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) ) -> ( X < y <-> X < ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) ) )
48	40 45 47	rexxfr2d	\|- ( ph -> ( E. y e. ran ( x e. ( ~P A i^i Fin ) \|-> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. x \|-> B ) ) ) X < y <-> E. a e. ( ~P A i^i Fin ) X < ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) ) )
49	38 48	mpbid	\|- ( ph -> E. a e. ( ~P A i^i Fin ) X < ( ( RR*s \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) )
50		nfv	\|- F/ k a e. ( ~P A i^i Fin )
51	1 50	nfan	\|- F/ k ( ph /\ a e. ( ~P A i^i Fin ) )
52		simpr	\|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ( ~P A i^i Fin ) )
53	14 52	sseldi	\|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. Fin )
54		simpll	\|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> ph )
55	20	sseli	\|- ( a e. ( ~P A i^i Fin ) -> a e. ~P A )
56	55	ad2antlr	\|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> a e. ~P A )
57	56	elpwid	\|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> a C_ A )
58		simpr	\|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> k e. a )
59	57 58	sseldd	\|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> k e. A )
60	54 59 3	syl2anc	\|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ k e. a ) -> B e. ( 0 [,] +oo ) )
61	51 53 60	gsumesum	\|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) = sum k e. a B )
62	61	breq2d	\|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( X < ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) <-> X < sum k e. a B ) )
63	62	biimpd	\|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( X < ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) -> X < sum k e. a B ) )
64	63	reximdva	\|- ( ph -> ( E. a e. ( ~P A i^i Fin ) X < ( ( RRs \|`s ( 0 [,] +oo ) ) gsum ( k e. a \|-> B ) ) -> E. a e. ( ~P A i^i Fin ) X < sum k e. a B ) )
65	49 64	mpd	\|- ( ph -> E. a e. ( ~P A i^i Fin ) X < sum* k e. a B )

Metamath Proof Explorer

Theorem esumlub

Proof