Metamath Proof Explorer

Theorem sge0ltfirp

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

Ref Expression
Hypotheses sge0ltfirp.x 
|- ( ph -> X e. V )
sge0ltfirp.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0ltfirp.y 
|- ( ph -> Y e. RR+ )
sge0ltfirp.re 
|- ( ph -> ( sum^ ` F ) e. RR )
Assertion sge0ltfirp 
|- ( ph -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )

Proof

Step Hyp Ref Expression
1 sge0ltfirp.x 
 |-  ( ph -> X e. V )
2 sge0ltfirp.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0ltfirp.y 
 |-  ( ph -> Y e. RR+ )
4 sge0ltfirp.re 
 |-  ( ph -> ( sum^ ` F ) e. RR )
5 1 2 4 sge0rern 
 |-  ( ph -> -. +oo e. ran F )
6 2 5 fge0iccico 
 |-  ( ph -> F : X --> ( 0 [,) +oo ) )
7 6 sge0rnre 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
8 sge0rnn0 
 |-  ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/)
9 8 a1i 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/) )
10 1 2 4 sge0rnbnd 
 |-  ( ph -> E. z e. RR A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ z )
11 7 9 10 3 suprltrp 
 |-  ( ph -> E. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w )
12 nfv 
 |-  F/ w ph
13 nfv 
 |-  F/ w E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y )
14 simp1 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> ph )
15 vex 
 |-  w e. _V
16 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
17 16 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) ) )
18 15 17 ax-mp 
 |-  ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) )
19 18 birani 
 |-  ( ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) )
20 nfmpt1 
 |-  F/_ x ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
21 20 nfrn 
 |-  F/_ x ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
22 nfcv 
 |-  F/_ x RR
23 nfcv 
 |-  F/_ x <
24 21 22 23 nfsup 
 |-  F/_ x sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < )
25 nfcv 
 |-  F/_ x -
26 nfcv 
 |-  F/_ x Y
27 24 25 26 nfov 
 |-  F/_ x ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y )
28 nfcv 
 |-  F/_ x w
29 27 23 28 nfbr 
 |-  F/ x ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w
30 simpl 
 |-  ( ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w /\ w = sum_ y e. x ( F ` y ) ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w )
31 simpr 
 |-  ( ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w /\ w = sum_ y e. x ( F ` y ) ) -> w = sum_ y e. x ( F ` y ) )
32 30 31 breqtrd 
 |-  ( ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w /\ w = sum_ y e. x ( F ` y ) ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) )
33 32 ex 
 |-  ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> ( w = sum_ y e. x ( F ` y ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) )
34 33 a1d 
 |-  ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> ( x e. ( ~P X i^i Fin ) -> ( w = sum_ y e. x ( F ` y ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) ) )
35 29 34 reximdai 
 |-  ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> ( E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) )
36 35 adantl 
 |-  ( ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> ( E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) )
37 19 36 mpd 
 |-  ( ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) )
38 37 3adant1 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) )
39 simpl 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ph /\ x e. ( ~P X i^i Fin ) ) )
40 1 2 4 sge0supre 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
41 40 oveq1d 
 |-  ( ph -> ( ( sum^ ` F ) - Y ) = ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) )
42 41 adantr 
 |-  ( ( ph /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) = ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) )
43 simpr 
 |-  ( ( ph /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) )
44 42 43 eqbrtrd 
 |-  ( ( ph /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) )
45 44 adantlr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) )
46 simpr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) )
47 4 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` F ) e. RR )
48 3 rpred 
 |-  ( ph -> Y e. RR )
49 48 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> Y e. RR )
50 elinel2 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. Fin )
51 50 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
52 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
53 6 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,) +oo ) )
54 53 adantr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> F : X --> ( 0 [,) +oo ) )
55 elpwinss 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
56 55 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
57 56 sselda 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X )
58 54 57 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
59 52 58 sselid 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
60 51 59 fsumrecl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) e. RR )
61 47 49 60 ltsubaddd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) <-> ( sum^ ` F ) < ( sum_ y e. x ( F ` y ) + Y ) ) )
62 61 adantr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) <-> ( sum^ ` F ) < ( sum_ y e. x ( F ` y ) + Y ) ) )
63 46 62 mpbid 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( sum_ y e. x ( F ` y ) + Y ) )
64 53 56 fssresd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,) +oo ) )
65 51 64 sge0fsum 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) = sum_ y e. x ( ( F |` x ) ` y ) )
66 fvres 
 |-  ( y e. x -> ( ( F |` x ) ` y ) = ( F ` y ) )
67 66 sumeq2i 
 |-  sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y )
68 67 a1i 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y ) )
69 65 68 eqtr2d 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum^ ` ( F |` x ) ) )
70 69 oveq1d 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum_ y e. x ( F ` y ) + Y ) = ( ( sum^ ` ( F |` x ) ) + Y ) )
71 70 adantr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum_ y e. x ( F ` y ) + Y ) = ( ( sum^ ` ( F |` x ) ) + Y ) )
72 63 71 breqtrd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )
73 39 45 72 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )
74 73 ex 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) )
75 74 reximdva 
 |-  ( ph -> ( E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) )
76 75 imp 
 |-  ( ( ph /\ E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )
77 14 38 76 syl2anc 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )
78 77 3exp 
 |-  ( ph -> ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) ) )
79 12 13 78 rexlimd 
 |-  ( ph -> ( E. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) )
80 11 79 mpd 
 |-  ( ph -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )