Metamath Proof Explorer

Theorem renepnf

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

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

Proof

Step Hyp Ref Expression
1 pnfnre 
 |-  +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 )