Theorem sge0lefimpt

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0lefimpt.xph	|- F/ x ph
	sge0lefimpt.a	|- ( ph -> A e. V )
	sge0lefimpt.b	|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
	sge0lefimpt.c	|- ( ph -> C e. RR* )
Assertion	sge0lefimpt	|- ( ph -> ( ( sum^ ` ( x e. A |-> B ) ) <_ C <-> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. y |-> B ) ) <_ C ) )

Proof

Step	Hyp	Ref	Expression
1		sge0lefimpt.xph	|- F/ x ph
2		sge0lefimpt.a	|- ( ph -> A e. V )
3		sge0lefimpt.b	|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
4		sge0lefimpt.c	|- ( ph -> C e. RR* )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	1 3 5	fmptdf	|- ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
7	2 6 4	sge0lefi	|- ( ph -> ( ( sum^ ` ( x e. A |-> B ) ) <_ C <-> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( ( x e. A |-> B ) |` y ) ) <_ C ) )
8		elpwinss	|- ( y e. ( ~P A i^i Fin ) -> y C_ A )
9	8	resmptd	|- ( y e. ( ~P A i^i Fin ) -> ( ( x e. A |-> B ) |` y ) = ( x e. y |-> B ) )
10	9	fveq2d	|- ( y e. ( ~P A i^i Fin ) -> ( sum^ ` ( ( x e. A |-> B ) |` y ) ) = ( sum^ ` ( x e. y |-> B ) ) )
11	10	breq1d	|- ( y e. ( ~P A i^i Fin ) -> ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) <_ C <-> ( sum^ ` ( x e. y |-> B ) ) <_ C ) )
12	11	ralbiia	|- ( A. y e. ( ~P A i^i Fin ) ( sum^ ` ( ( x e. A |-> B ) |` y ) ) <_ C <-> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. y |-> B ) ) <_ C )
13	12	a1i	|- ( ph -> ( A. y e. ( ~P A i^i Fin ) ( sum^ ` ( ( x e. A |-> B ) |` y ) ) <_ C <-> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. y |-> B ) ) <_ C ) )
14	7 13	bitrd	|- ( ph -> ( ( sum^ ` ( x e. A |-> B ) ) <_ C <-> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. y |-> B ) ) <_ C ) )