Metamath Proof Explorer

Theorem mnflt

Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion mnflt 
|- ( A e. RR -> -oo < A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  -oo = -oo
2 olc 
 |-  ( ( -oo = -oo /\ A e. RR ) -> ( ( -oo e. RR /\ A = +oo ) \/ ( -oo = -oo /\ A e. RR ) ) )
3 1 2 mpan 
 |-  ( A e. RR -> ( ( -oo e. RR /\ A = +oo ) \/ ( -oo = -oo /\ A e. RR ) ) )
4 3 olcd 
 |-  ( A e. RR -> ( ( ( ( -oo e. RR /\ A e. RR ) /\ -oo
5 mnfxr 
 |-  -oo e. RR*
6 rexr 
 |-  ( A e. RR -> A e. RR* )
7 ltxr 
 |-  ( ( -oo e. RR* /\ A e. RR* ) -> ( -oo < A <-> ( ( ( ( -oo e. RR /\ A e. RR ) /\ -oo
8 5 6 7 sylancr 
 |-  ( A e. RR -> ( -oo < A <-> ( ( ( ( -oo e. RR /\ A e. RR ) /\ -oo
9 4 8 mpbird 
 |-  ( A e. RR -> -oo < A )