Metamath Proof Explorer

Theorem mnfltxr

Description: Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006)

Ref Expression
Assertion mnfltxr 
|- ( ( A e. RR \/ A = +oo ) -> -oo < A )

Proof

Step Hyp Ref Expression
1 mnflt 
 |-  ( A e. RR -> -oo < A )
2 mnfltpnf 
 |-  -oo < +oo
3 breq2 
 |-  ( A = +oo -> ( -oo < A <-> -oo < +oo ) )
4 2 3 mpbiri 
 |-  ( A = +oo -> -oo < A )
5 1 4 jaoi 
 |-  ( ( A e. RR \/ A = +oo ) -> -oo < A )