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 )