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 kφ
sge0repnfmpt.a φAV
sge0repnfmpt.b φkAB0+∞
Assertion sge0repnfmpt φsum^kAB¬sum^kAB=+∞

Proof

Step Hyp Ref Expression
1 sge0repnfmpt.k kφ
2 sge0repnfmpt.a φAV
3 sge0repnfmpt.b φkAB0+∞
4 eqid kAB=kAB
5 1 3 4 fmptdf φkAB:A0+∞
6 2 5 sge0repnf φsum^kAB¬sum^kAB=+∞