Metamath Proof Explorer


Theorem sge0repnfmpt

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 ) )

Proof

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 ) )