Metamath Proof Explorer

Theorem sge0gerp

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 sge0gerp.x 
|- ( ph -> X e. V )
sge0gerp.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0gerp.a 
|- ( ph -> A e. RR* )
sge0gerp.z 
|- ( ( ph /\ x e. RR+ ) -> E. z e. ( ~P X i^i Fin ) A <_ ( ( sum^ ` ( F |` z ) ) +e x ) )
Assertion sge0gerp 
|- ( ph -> A <_ ( sum^ ` F ) )

Proof

Step Hyp Ref Expression
1 sge0gerp.x 
 |-  ( ph -> X e. V )
2 sge0gerp.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0gerp.a 
 |-  ( ph -> A e. RR* )
4 sge0gerp.z 
 |-  ( ( ph /\ x e. RR+ ) -> E. z e. ( ~P X i^i Fin ) A <_ ( ( sum^ ` ( F |` z ) ) +e x ) )
5 nfv 
 |-  F/ x ph
6 simpr 
 |-  ( ( ph /\ z e. ( ~P X i^i Fin ) ) -> z e. ( ~P X i^i Fin ) )
7 2 adantr 
 |-  ( ( ph /\ z e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
8 elinel1 
 |-  ( z e. ( ~P X i^i Fin ) -> z e. ~P X )
9 elpwi 
 |-  ( z e. ~P X -> z C_ X )
10 8 9 syl 
 |-  ( z e. ( ~P X i^i Fin ) -> z C_ X )
11 10 adantl 
 |-  ( ( ph /\ z e. ( ~P X i^i Fin ) ) -> z C_ X )
12 7 11 fssresd 
 |-  ( ( ph /\ z e. ( ~P X i^i Fin ) ) -> ( F |` z ) : z --> ( 0 [,] +oo ) )
13 6 12 sge0xrcl 
 |-  ( ( ph /\ z e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` z ) ) e. RR* )
14 13 ralrimiva 
 |-  ( ph -> A. z e. ( ~P X i^i Fin ) ( sum^ ` ( F |` z ) ) e. RR* )
15 eqid 
 |-  ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) = ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) )
16 15 rnmptss 
 |-  ( A. z e. ( ~P X i^i Fin ) ( sum^ ` ( F |` z ) ) e. RR* -> ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) C_ RR* )
17 14 16 syl 
 |-  ( ph -> ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) C_ RR* )
18 nfv 
 |-  F/ z ( ph /\ x e. RR+ )
19 nfmpt1 
 |-  F/_ z ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) )
20 19 nfrn 
 |-  F/_ z ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) )
21 nfv 
 |-  F/ z A <_ ( y +e x )
22 20 21 nfrexw 
 |-  F/ z E. y e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) A <_ ( y +e x )
23 id 
 |-  ( z e. ( ~P X i^i Fin ) -> z e. ( ~P X i^i Fin ) )
24 fvexd 
 |-  ( z e. ( ~P X i^i Fin ) -> ( sum^ ` ( F |` z ) ) e. _V )
25 15 elrnmpt1 
 |-  ( ( z e. ( ~P X i^i Fin ) /\ ( sum^ ` ( F |` z ) ) e. _V ) -> ( sum^ ` ( F |` z ) ) e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) )
26 23 24 25 syl2anc 
 |-  ( z e. ( ~P X i^i Fin ) -> ( sum^ ` ( F |` z ) ) e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) )
27 26 3ad2ant2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ z e. ( ~P X i^i Fin ) /\ A <_ ( ( sum^ ` ( F |` z ) ) +e x ) ) -> ( sum^ ` ( F |` z ) ) e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) )
28 simp3 
 |-  ( ( ( ph /\ x e. RR+ ) /\ z e. ( ~P X i^i Fin ) /\ A <_ ( ( sum^ ` ( F |` z ) ) +e x ) ) -> A <_ ( ( sum^ ` ( F |` z ) ) +e x ) )
29 nfv 
 |-  F/ y A <_ ( ( sum^ ` ( F |` z ) ) +e x )
30 oveq1 
 |-  ( y = ( sum^ ` ( F |` z ) ) -> ( y +e x ) = ( ( sum^ ` ( F |` z ) ) +e x ) )
31 30 breq2d 
 |-  ( y = ( sum^ ` ( F |` z ) ) -> ( A <_ ( y +e x ) <-> A <_ ( ( sum^ ` ( F |` z ) ) +e x ) ) )
32 29 31 rspce 
 |-  ( ( ( sum^ ` ( F |` z ) ) e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) /\ A <_ ( ( sum^ ` ( F |` z ) ) +e x ) ) -> E. y e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) A <_ ( y +e x ) )
33 27 28 32 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ z e. ( ~P X i^i Fin ) /\ A <_ ( ( sum^ ` ( F |` z ) ) +e x ) ) -> E. y e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) A <_ ( y +e x ) )
34 33 3exp 
 |-  ( ( ph /\ x e. RR+ ) -> ( z e. ( ~P X i^i Fin ) -> ( A <_ ( ( sum^ ` ( F |` z ) ) +e x ) -> E. y e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) A <_ ( y +e x ) ) ) )
35 18 22 34 rexlimd 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. z e. ( ~P X i^i Fin ) A <_ ( ( sum^ ` ( F |` z ) ) +e x ) -> E. y e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) A <_ ( y +e x ) ) )
36 4 35 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) A <_ ( y +e x ) )
37 5 17 3 36 supxrge 
 |-  ( ph -> A <_ sup ( ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) , RR* , < ) )
38 1 2 sge0sup 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) , RR* , < ) )
39 38 eqcomd 
 |-  ( ph -> sup ( ran ( z e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` z ) ) ) , RR* , < ) = ( sum^ ` F ) )
40 37 39 breqtrd 
 |-  ( ph -> A <_ ( sum^ ` F ) )