Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | sge0vald.x | |- ( ph -> X e. V ) |
|
| sge0vald.f | |- ( ph -> F : X --> ( 0 [,] +oo ) ) |
||
| Assertion | sge0vald | |- ( ph -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sge0vald.x | |- ( ph -> X e. V ) |
|
| 2 | sge0vald.f | |- ( ph -> F : X --> ( 0 [,] +oo ) ) |
|
| 3 | sge0val | |- ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) ) |
|
| 4 | 1 2 3 | syl2anc | |- ( ph -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) ) |