Metamath Proof Explorer

Theorem renemnf

Description: No real equals minus infinity. (Contributed by NM, 14-Oct-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion renemnf 
|- ( A e. RR -> A =/= -oo )

Proof

Step Hyp Ref Expression
1 mnfnre 
 |-  -oo e/ RR
2 1 neli 
 |-  -. -oo e. RR
3 eleq1 
 |-  ( A = -oo -> ( A e. RR <-> -oo e. RR ) )
4 2 3 mtbiri 
 |-  ( A = -oo -> -. A e. RR )
5 4 necon2ai 
 |-  ( A e. RR -> A =/= -oo )