Metamath Proof Explorer

Theorem mnfnre

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

Ref Expression
Assertion mnfnre 
|- -oo e/ RR

Proof

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