MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pnfnemnf Unicode version

Theorem pnfnemnf 10642
Description: Plus and minus infinity are distinguished elements of 
RR*. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
pnfnemnf  |-  +oo  =/=  -oo

Proof of Theorem pnfnemnf
StepHypRef Expression
1 pnfxr 10638 . . . 4  |-  +oo  e.  RR*
2 pwne 4300 . . . 4  |-  (  +oo  e.  RR*  ->  ~P  +oo  =/=  +oo )
31, 2ax-mp 8 . . 3  |-  ~P  +oo  =/=  +oo
43necomi 2625 . 2  |-  +oo  =/=  ~P 
+oo
5 df-mnf 9049 . 2  |-  -oo  =  ~P  +oo
64, 5neeqtrri 2566 1  |-  +oo  =/=  -oo
Colors of variables: wff set class
Syntax hints:    e. wcel 1717    =/= wne 2543   ~Pcpw 3735    +oocpnf 9043    -oocmnf 9044   RR*cxr 9045
This theorem is referenced by:  xrnemnf  10643  xrnepnf  10644  xrltnr  10645  pnfnlt  10650  nltmnf  10651  xnegmnf  10721  xaddpnf1  10737  xaddmnf1  10739  xaddmnf2  10740  mnfaddpnf  10742  xaddnemnf  10745  xaddnepnf  10746  xmullem2  10769  xadddilem  10798  resup  11168  hashnemnf  11548  xrge0iifhom  24120  esumpr2  24247
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-pow 4311  ax-un 4634  ax-cnex 8972
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-nel 2546  df-rex 2648  df-rab 2651  df-v 2894  df-un 3261  df-in 3263  df-ss 3270  df-pw 3737  df-sn 3756  df-pr 3757  df-uni 3951  df-pnf 9048  df-mnf 9049  df-xr 9050
  Copyright terms: Public domain W3C validator