Metamath Proof Explorer


Theorem xrge0le

Description: The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018)

Ref Expression
Assertion xrge0le =𝑠*𝑠0+∞

Proof

Step Hyp Ref Expression
1 ovex 0+∞V
2 eqid 𝑠*𝑠0+∞=𝑠*𝑠0+∞
3 xrsle =𝑠*
4 2 3 ressle 0+∞V=𝑠*𝑠0+∞
5 1 4 ax-mp =𝑠*𝑠0+∞