Metamath Proof Explorer

Theorem sge0rnbnd

Description: The range used in the definition of sum^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0rnbnd.x 
|- ( ph -> X e. V )
sge0rnbnd.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0rnbnd.re 
|- ( ph -> ( sum^ ` F ) e. RR )
Assertion 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 )

Proof

Step Hyp Ref Expression
1 sge0rnbnd.x 
 |-  ( ph -> X e. V )
2 sge0rnbnd.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0rnbnd.re 
 |-  ( ph -> ( sum^ ` F ) e. RR )
4 simpl 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ph )
5 vex 
 |-  w e. _V
6 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 ) )
7 6 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 ) ) )
8 5 7 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 ) )
9 8 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 ) )
10 9 adantl 
 |-  ( ( 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 ) )
11 simp3 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ w = sum_ y e. x ( F ` y ) ) -> w = sum_ y e. x ( F ` y ) )
12 1 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> X e. V )
13 2 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
14 1 2 3 sge0rern 
 |-  ( ph -> -. +oo e. ran F )
15 14 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> -. +oo e. ran F )
16 13 15 fge0iccico 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,) +oo ) )
17 elpwinss 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
18 17 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
19 elinel2 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. Fin )
20 19 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
21 12 16 18 20 fsumlesge0 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) <_ ( sum^ ` F ) )
22 21 3adant3 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ w = sum_ y e. x ( F ` y ) ) -> sum_ y e. x ( F ` y ) <_ ( sum^ ` F ) )
23 11 22 eqbrtrd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ w = sum_ y e. x ( F ` y ) ) -> w <_ ( sum^ ` F ) )
24 23 3exp 
 |-  ( ph -> ( x e. ( ~P X i^i Fin ) -> ( w = sum_ y e. x ( F ` y ) -> w <_ ( sum^ ` F ) ) ) )
25 24 rexlimdv 
 |-  ( ph -> ( E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) -> w <_ ( sum^ ` F ) ) )
26 4 10 25 sylc 
 |-  ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> w <_ ( sum^ ` F ) )
27 26 ralrimiva 
 |-  ( ph -> A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ ( sum^ ` F ) )
28 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 )
29 3 27 28 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 )