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 ffvelrnd
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
60 53 59 sseldi
 |-  ( ( ( 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 ) )