Description: The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0clmpt.xph | |- F/ x ph |
|
sge0clmpt.a | |- ( ph -> A e. V ) |
||
sge0clmpt.b | |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) ) |
||
Assertion | sge0clmpt | |- ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. ( 0 [,] +oo ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0clmpt.xph | |- F/ x ph |
|
2 | sge0clmpt.a | |- ( ph -> A e. V ) |
|
3 | sge0clmpt.b | |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) ) |
|
4 | eqid | |- ( x e. A |-> B ) = ( x e. A |-> B ) |
|
5 | 1 3 4 | fmptdf | |- ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) ) |
6 | 2 5 | sge0cl | |- ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. ( 0 [,] +oo ) ) |