Metamath Proof Explorer

Theorem mnfle

Description: Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion mnfle 
|- ( A e. RR* -> -oo <_ A )

Proof

Step Hyp Ref Expression
1 nltmnf 
 |-  ( A e. RR* -> -. A < -oo )
2 mnfxr 
 |-  -oo e. RR*
3 xrlenlt 
 |-  ( ( -oo e. RR* /\ A e. RR* ) -> ( -oo <_ A <-> -. A < -oo ) )
4 2 3 mpan 
 |-  ( A e. RR* -> ( -oo <_ A <-> -. A < -oo ) )
5 1 4 mpbird 
 |-  ( A e. RR* -> -oo <_ A )