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 biimpi 
 |-  ( 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 ) )
20 19 adantr 
 |-  ( ( 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 ) )
21 nfmpt1 
 |-  F/_ x ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
22 21 nfrn 
 |-  F/_ x ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
23 nfcv 
 |-  F/_ x RR
24 nfcv 
 |-  F/_ x <
25 22 23 24 nfsup 
 |-  F/_ x sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < )
26 nfcv 
 |-  F/_ x -
27 nfcv 
 |-  F/_ x Y
28 25 26 27 nfov 
 |-  F/_ x ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y )
29 nfcv 
 |-  F/_ x w
30 28 24 29 nfbr 
 |-  F/ x ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w
31 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 )
32 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 ) )
33 31 32 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 ) )
34 33 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 ) ) )
35 34 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 ) ) ) )
36 30 35 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 ) ) )
37 36 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 ) ) )
38 20 37 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 ) )
39 38 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 ) )
40 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 ) ) )
41 1 2 4 sge0supre 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
42 41 oveq1d 
 |-  ( ph -> ( ( sum^ ` F ) - Y ) = ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) )
43 42 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 ) )
44 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 ) )
45 43 44 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 ) )
46 45 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 ) )
47 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 ) )
48 4 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` F ) e. RR )
49 3 rpred 
 |-  ( ph -> Y e. RR )
50 49 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> Y e. RR )
51 elinel2 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. Fin )
52 51 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
53 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
54 6 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,) +oo ) )
55 54 adantr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> F : X --> ( 0 [,) +oo ) )
56 elpwinss 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
57 56 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
58 57 sselda 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X )
59 55 58 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
60 53 59 sselid 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
61 52 60 fsumrecl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) e. RR )
62 48 50 61 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 ) ) )
63 62 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 ) ) )
64 47 63 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 ) )
65 54 57 fssresd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,) +oo ) )
66 52 65 sge0fsum 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) = sum_ y e. x ( ( F |` x ) ` y ) )
67 fvres 
 |-  ( y e. x -> ( ( F |` x ) ` y ) = ( F ` y ) )
68 67 sumeq2i 
 |-  sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y )
69 68 a1i 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y ) )
70 66 69 eqtr2d 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum^ ` ( F |` x ) ) )
71 70 oveq1d 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum_ y e. x ( F ` y ) + Y ) = ( ( sum^ ` ( F |` x ) ) + Y ) )
72 71 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 ) )
73 64 72 breqtrd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )
74 40 46 73 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 ) )
75 74 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 ) ) )
76 75 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 ) ) )
77 76 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 ) )
78 14 39 77 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 ) )
79 78 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 ) ) ) )
80 12 13 79 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 ) ) )
81 11 80 mpd 
 |-  ( ph -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) )