Metamath Proof Explorer


Theorem xrge0ge0

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

Ref Expression
Assertion xrge0ge0 A 0 +∞ 0 A

Proof

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