Metamath Proof Explorer

Theorem sge0gerpmpt

Description: The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 sge0gerpmpt.xph 
 |-  F/ x ph
2 sge0gerpmpt.a 
 |-  ( ph -> A e. V )
3 sge0gerpmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
4 sge0gerpmpt.c 
 |-  ( ph -> C e. RR* )
5 sge0gerpmpt.rp 
 |-  ( ( ph /\ y e. RR+ ) -> E. z e. ( ~P A i^i Fin ) C <_ ( ( sum^ ` ( x e. z |-> B ) ) +e y ) )
6 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
7 1 3 6 fmptdf 
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
8 elpwinss 
 |-  ( z e. ( ~P A i^i Fin ) -> z C_ A )
9 8 resmptd 
 |-  ( z e. ( ~P A i^i Fin ) -> ( ( x e. A |-> B ) |` z ) = ( x e. z |-> B ) )
10 9 eqcomd 
 |-  ( z e. ( ~P A i^i Fin ) -> ( x e. z |-> B ) = ( ( x e. A |-> B ) |` z ) )
11 10 fveq2d 
 |-  ( z e. ( ~P A i^i Fin ) -> ( sum^ ` ( x e. z |-> B ) ) = ( sum^ ` ( ( x e. A |-> B ) |` z ) ) )
12 11 oveq1d 
 |-  ( z e. ( ~P A i^i Fin ) -> ( ( sum^ ` ( x e. z |-> B ) ) +e y ) = ( ( sum^ ` ( ( x e. A |-> B ) |` z ) ) +e y ) )
13 12 breq2d 
 |-  ( z e. ( ~P A i^i Fin ) -> ( C <_ ( ( sum^ ` ( x e. z |-> B ) ) +e y ) <-> C <_ ( ( sum^ ` ( ( x e. A |-> B ) |` z ) ) +e y ) ) )
14 13 biimpd 
 |-  ( z e. ( ~P A i^i Fin ) -> ( C <_ ( ( sum^ ` ( x e. z |-> B ) ) +e y ) -> C <_ ( ( sum^ ` ( ( x e. A |-> B ) |` z ) ) +e y ) ) )
15 14 adantl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ z e. ( ~P A i^i Fin ) ) -> ( C <_ ( ( sum^ ` ( x e. z |-> B ) ) +e y ) -> C <_ ( ( sum^ ` ( ( x e. A |-> B ) |` z ) ) +e y ) ) )
16 15 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. z e. ( ~P A i^i Fin ) C <_ ( ( sum^ ` ( x e. z |-> B ) ) +e y ) -> E. z e. ( ~P A i^i Fin ) C <_ ( ( sum^ ` ( ( x e. A |-> B ) |` z ) ) +e y ) ) )
17 5 16 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. z e. ( ~P A i^i Fin ) C <_ ( ( sum^ ` ( ( x e. A |-> B ) |` z ) ) +e y ) )
18 2 7 4 17 sge0gerp 
 |-  ( ph -> C <_ ( sum^ ` ( x e. A |-> B ) ) )