Metamath Proof Explorer

Theorem pnfnemnf

Description: Plus and minus infinity are different elements of RR* . (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion pnfnemnf 
|- +oo =/= -oo

Proof

Step Hyp Ref Expression
1 pnfxr 
 |-  +oo e. RR*
2 pwne 
 |-  ( +oo e. RR* -> ~P +oo =/= +oo )
3 1 2 ax-mp 
 |-  ~P +oo =/= +oo
4 3 necomi 
 |-  +oo =/= ~P +oo
5 df-mnf 
 |-  -oo = ~P +oo
6 4 5 neeqtrri 
 |-  +oo =/= -oo