Metamath Proof Explorer

Theorem xlemnf

Description: An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 xrlenlt 
 |-  ( ( A e. RR* /\ -oo e. RR* ) -> ( A <_ -oo <-> -. -oo < A ) )
3 1 2 mpan2 
 |-  ( A e. RR* -> ( A <_ -oo <-> -. -oo < A ) )
4 ngtmnft 
 |-  ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
5 3 4 bitr4d 
 |-  ( A e. RR* -> ( A <_ -oo <-> A = -oo ) )