Description: A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fge0iccre.1 | ||
fge0iccre.2 | |||
Assertion | fge0iccre |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fge0iccre.1 | ||
2 | fge0iccre.2 | ||
3 | 1 2 | fge0iccico | |
4 | rge0ssre | ||
5 | 4 | a1i | |
6 | 3 5 | fssd |