Description: The of nonnegative extended reals is a real number if and only if it is not +oo . (Contributed by Glauco Siliprandi, 21-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0repnfmpt.k | |- F/ k ph |
|
sge0repnfmpt.a | |- ( ph -> A e. V ) |
||
sge0repnfmpt.b | |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) ) |
||
Assertion | sge0repnfmpt | |- ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) e. RR <-> -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0repnfmpt.k | |- F/ k ph |
|
2 | sge0repnfmpt.a | |- ( ph -> A e. V ) |
|
3 | sge0repnfmpt.b | |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) ) |
|
4 | eqid | |- ( k e. A |-> B ) = ( k e. A |-> B ) |
|
5 | 1 3 4 | fmptdf | |- ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) ) |
6 | 2 5 | sge0repnf | |- ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) e. RR <-> -. ( sum^ ` ( k e. A |-> B ) ) = +oo ) ) |