Metamath Proof Explorer


Theorem rge0ssre

Description: Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018) (Proof shortened by AV, 8-Sep-2019)

Ref Expression
Assertion rge0ssre 0+∞

Proof

Step Hyp Ref Expression
1 elrege0 x0+∞x0x
2 1 simplbi x0+∞x
3 2 ssriv 0+∞