Metamath Proof Explorer


Theorem xrge0ge0

Description: A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion xrge0ge0 A0+∞0A

Proof

Step Hyp Ref Expression
1 elxrge0 A0+∞A*0A
2 1 biimpi A0+∞A*0A
3 2 simprd A0+∞0A