Metamath Proof Explorer

Theorem sge0lefi

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lefi.1 
|- ( ph -> X e. V )
sge0lefi.2 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0lefi.3 
|- ( ph -> A e. RR* )
Assertion sge0lefi 
|- ( ph -> ( ( sum^ ` F ) <_ A <-> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) )

Proof

Step Hyp Ref Expression
1 sge0lefi.1 
 |-  ( ph -> X e. V )
2 sge0lefi.2 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0lefi.3 
 |-  ( ph -> A e. RR* )
4 simpr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. ( ~P X i^i Fin ) )
5 2 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
6 elpwinss 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
7 6 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
8 5 7 fssresd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,] +oo ) )
9 4 8 sge0xrcl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) e. RR* )
10 9 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` F ) <_ A ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) e. RR* )
11 1 2 sge0xrcl 
 |-  ( ph -> ( sum^ ` F ) e. RR* )
12 11 ad2antrr 
 |-  ( ( ( ph /\ ( sum^ ` F ) <_ A ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` F ) e. RR* )
13 3 ad2antrr 
 |-  ( ( ( ph /\ ( sum^ ` F ) <_ A ) /\ x e. ( ~P X i^i Fin ) ) -> A e. RR* )
14 1 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> X e. V )
15 14 5 sge0less 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) <_ ( sum^ ` F ) )
16 15 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` F ) <_ A ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) <_ ( sum^ ` F ) )
17 simplr 
 |-  ( ( ( ph /\ ( sum^ ` F ) <_ A ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` F ) <_ A )
18 10 12 13 16 17 xrletrd 
 |-  ( ( ( ph /\ ( sum^ ` F ) <_ A ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) <_ A )
19 18 ralrimiva 
 |-  ( ( ph /\ ( sum^ ` F ) <_ A ) -> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A )
20 19 ex 
 |-  ( ph -> ( ( sum^ ` F ) <_ A -> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) )
21 1 2 sge0sup 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )
22 21 adantr 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )
23 vex 
 |-  y e. _V
24 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) = ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
25 24 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) <-> E. x e. ( ~P X i^i Fin ) y = ( sum^ ` ( F |` x ) ) ) )
26 23 25 ax-mp 
 |-  ( y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) <-> E. x e. ( ~P X i^i Fin ) y = ( sum^ ` ( F |` x ) ) )
27 26 biimpi 
 |-  ( y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) -> E. x e. ( ~P X i^i Fin ) y = ( sum^ ` ( F |` x ) ) )
28 27 adantl 
 |-  ( ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) /\ y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) -> E. x e. ( ~P X i^i Fin ) y = ( sum^ ` ( F |` x ) ) )
29 nfv 
 |-  F/ x ph
30 nfra1 
 |-  F/ x A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A
31 29 30 nfan 
 |-  F/ x ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A )
32 nfcv 
 |-  F/_ x y
33 nfmpt1 
 |-  F/_ x ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
34 33 nfrn 
 |-  F/_ x ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
35 32 34 nfel 
 |-  F/ x y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
36 31 35 nfan 
 |-  F/ x ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) /\ y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) )
37 nfv 
 |-  F/ x y <_ A
38 simp3 
 |-  ( ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A /\ x e. ( ~P X i^i Fin ) /\ y = ( sum^ ` ( F |` x ) ) ) -> y = ( sum^ ` ( F |` x ) ) )
39 rspa 
 |-  ( ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) <_ A )
40 39 3adant3 
 |-  ( ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A /\ x e. ( ~P X i^i Fin ) /\ y = ( sum^ ` ( F |` x ) ) ) -> ( sum^ ` ( F |` x ) ) <_ A )
41 38 40 eqbrtrd 
 |-  ( ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A /\ x e. ( ~P X i^i Fin ) /\ y = ( sum^ ` ( F |` x ) ) ) -> y <_ A )
42 41 3adant1l 
 |-  ( ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) /\ x e. ( ~P X i^i Fin ) /\ y = ( sum^ ` ( F |` x ) ) ) -> y <_ A )
43 42 3exp 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> ( x e. ( ~P X i^i Fin ) -> ( y = ( sum^ ` ( F |` x ) ) -> y <_ A ) ) )
44 43 adantr 
 |-  ( ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) /\ y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) -> ( x e. ( ~P X i^i Fin ) -> ( y = ( sum^ ` ( F |` x ) ) -> y <_ A ) ) )
45 36 37 44 rexlimd 
 |-  ( ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) /\ y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) -> ( E. x e. ( ~P X i^i Fin ) y = ( sum^ ` ( F |` x ) ) -> y <_ A ) )
46 28 45 mpd 
 |-  ( ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) /\ y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) -> y <_ A )
47 46 ralrimiva 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> A. y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y <_ A )
48 9 ralrimiva 
 |-  ( ph -> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) e. RR* )
49 24 rnmptss 
 |-  ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) e. RR* -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
50 48 49 syl 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
51 50 adantr 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
52 3 adantr 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> A e. RR* )
53 supxrleub 
 |-  ( ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* /\ A e. RR* ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) <_ A <-> A. y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y <_ A ) )
54 51 52 53 syl2anc 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) <_ A <-> A. y e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y <_ A ) )
55 47 54 mpbird 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) <_ A )
56 22 55 eqbrtrd 
 |-  ( ( ph /\ A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) -> ( sum^ ` F ) <_ A )
57 56 ex 
 |-  ( ph -> ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A -> ( sum^ ` F ) <_ A ) )
58 20 57 impbid 
 |-  ( ph -> ( ( sum^ ` F ) <_ A <-> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) <_ A ) )