Metamath Proof Explorer

Theorem sge0ltfirpmpt

Description: If the extended sum of nonnegative reals is not +oo , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypotheses	sge0ltfirpmpt.xph	\|- F/ x ph
		sge0ltfirpmpt.a	\|- ( ph -> A e. V )
		sge0ltfirpmpt.b	\|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
		sge0ltfirpmpt.rp	\|- ( ph -> Y e. RR+ )
		sge0ltfirpmpt.re	\|- ( ph -> ( sum^ ` ( x e. A \|-> B ) ) e. RR )
	Assertion	sge0ltfirpmpt	\|- ( ph -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) )

Proof

Step	Hyp	Ref	Expression
1		sge0ltfirpmpt.xph	\|- F/ x ph
2		sge0ltfirpmpt.a	\|- ( ph -> A e. V )
3		sge0ltfirpmpt.b	\|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
4		sge0ltfirpmpt.rp	\|- ( ph -> Y e. RR+ )
5		sge0ltfirpmpt.re	\|- ( ph -> ( sum^ ` ( x e. A \|-> B ) ) e. RR )
6		eqid	\|- ( x e. A \|-> B ) = ( x e. A \|-> B )
7	1 3 6	fmptdf	\|- ( ph -> ( x e. A \|-> B ) : A --> ( 0 [,] +oo ) )
8	2 7 4 5	sge0ltfirp	\|- ( ph -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) )
9		simpr	\|- ( ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) ) -> ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) )
10		elpwinss	\|- ( y e. ( ~P A i^i Fin ) -> y C_ A )
11	10	resmptd	\|- ( y e. ( ~P A i^i Fin ) -> ( ( x e. A \|-> B ) \|` y ) = ( x e. y \|-> B ) )
12	11	fveq2d	\|- ( y e. ( ~P A i^i Fin ) -> ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) = ( sum^ ` ( x e. y \|-> B ) ) )
13	12	oveq1d	\|- ( y e. ( ~P A i^i Fin ) -> ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) = ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) )
14	13	adantr	\|- ( ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) ) -> ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) = ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) )
15	9 14	breqtrd	\|- ( ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) ) -> ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) )
16	15	ex	\|- ( y e. ( ~P A i^i Fin ) -> ( ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) -> ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) ) )
17	16	reximia	\|- ( E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) )
18	17	a1i	\|- ( ph -> ( E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( ( x e. A \|-> B ) \|` y ) ) + Y ) -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) ) )
19	8 18	mpd	\|- ( ph -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A \|-> B ) ) < ( ( sum^ ` ( x e. y \|-> B ) ) + Y ) )