Metamath Proof Explorer

Theorem sge0supre

Description: If the arbitrary sum of nonnegative extended reals is real, then it is the supremum (in the real numbers) of finite subsums. Similar to sge0sup , but here we can use sup with respect to RR instead of RR* . (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 sge0supre.x 
 |-  ( ph -> X e. V )
2 sge0supre.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0supre.re 
 |-  ( ph -> ( sum^ ` F ) e. RR )
4 1 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> X e. V )
5 2 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
6 simpr 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
7 4 5 6 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = +oo )
8 1 2 sge0repnf 
 |-  ( ph -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
9 3 8 mpbid 
 |-  ( ph -> -. ( sum^ ` F ) = +oo )
10 9 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> -. ( sum^ ` F ) = +oo )
11 7 10 pm2.65da 
 |-  ( ph -> -. +oo e. ran F )
12 2 11 fge0iccico 
 |-  ( ph -> F : X --> ( 0 [,) +oo ) )
13 1 12 sge0reval 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
14 12 sge0rnre 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
15 sge0rnn0 
 |-  ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/)
16 15 a1i 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/) )
17 simpr 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
18 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 ) )
19 18 elrnmpt 
 |-  ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> ( 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 adantl 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ( 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 ) ) )
21 17 20 mpbid 
 |-  ( ( ph /\ 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 ) )
22 simp3 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ w = sum_ y e. x ( F ` y ) ) -> w = sum_ y e. x ( F ` y ) )
23 ressxr 
 |-  RR C_ RR*
24 23 a1i 
 |-  ( ph -> RR C_ RR* )
25 14 24 sstrd 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
26 25 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
27 id 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. ( ~P X i^i Fin ) )
28 sumex 
 |-  sum_ y e. x ( F ` y ) e. _V
29 28 a1i 
 |-  ( x e. ( ~P X i^i Fin ) -> sum_ y e. x ( F ` y ) e. _V )
30 18 elrnmpt1 
 |-  ( ( x e. ( ~P X i^i Fin ) /\ sum_ y e. x ( F ` y ) e. _V ) -> sum_ y e. x ( F ` y ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
31 27 29 30 syl2anc 
 |-  ( x e. ( ~P X i^i Fin ) -> sum_ y e. x ( F ` y ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
32 31 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
33 supxrub 
 |-  ( ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* /\ sum_ y e. x ( F ` y ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> sum_ y e. x ( F ` y ) <_ sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
34 26 32 33 syl2anc 
 |-  ( ( ph /\ 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* , < ) )
35 13 eqcomd 
 |-  ( ph -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = ( sum^ ` F ) )
36 35 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = ( sum^ ` F ) )
37 34 36 breqtrd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) <_ ( sum^ ` F ) )
38 37 3adant3 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ w = sum_ y e. x ( F ` y ) ) -> sum_ y e. x ( F ` y ) <_ ( sum^ ` F ) )
39 22 38 eqbrtrd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ w = sum_ y e. x ( F ` y ) ) -> w <_ ( sum^ ` F ) )
40 39 3exp 
 |-  ( ph -> ( x e. ( ~P X i^i Fin ) -> ( w = sum_ y e. x ( F ` y ) -> w <_ ( sum^ ` F ) ) ) )
41 40 rexlimdv 
 |-  ( ph -> ( E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) -> w <_ ( sum^ ` F ) ) )
42 41 adantr 
 |-  ( ( ph /\ 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 ) -> w <_ ( sum^ ` F ) ) )
43 21 42 mpd 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> w <_ ( sum^ ` F ) )
44 43 ralrimiva 
 |-  ( ph -> A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ ( sum^ ` F ) )
45 brralrspcev 
 |-  ( ( ( sum^ ` F ) e. RR /\ A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ ( sum^ ` F ) ) -> E. z e. RR A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ z )
46 3 44 45 syl2anc 
 |-  ( ph -> E. z e. RR A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ z )
47 supxrre 
 |-  ( ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR /\ ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/) /\ E. z e. RR A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ z ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
48 14 16 46 47 syl3anc 
 |-  ( ph -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
49 13 48 eqtrd 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )