Metamath Proof Explorer

Theorem pnfnre

Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion pnfnre 
|- +oo e/ RR

Proof

Step Hyp Ref Expression
1 df-pnf 
 |-  +oo = ~P U. CC
2 pwuninel 
 |-  -. ~P U. CC e. CC
3 1 2 eqneltri 
 |-  -. +oo e. CC
4 recn 
 |-  ( +oo e. RR -> +oo e. CC )
5 3 4 mto 
 |-  -. +oo e. RR
6 5 nelir 
 |-  +oo e/ RR