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 | |
|
sge0repnfmpt.a | |
||
sge0repnfmpt.b | |
||
Assertion | sge0repnfmpt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0repnfmpt.k | |
|
2 | sge0repnfmpt.a | |
|
3 | sge0repnfmpt.b | |
|
4 | eqid | |
|
5 | 1 3 4 | fmptdf | |
6 | 2 5 | sge0repnf | |