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

Theorem pnfnemnf 10475
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 10471 . . . 4  |-  +oo  e.  RR*
2 pwne 4193 . . . 4  |-  (  +oo  e.  RR*  ->  ~P  +oo  =/=  +oo )
31, 2ax-mp 8 . . 3  |-  ~P  +oo  =/=  +oo
43necomi 2541 . 2  |-  +oo  =/=  ~P 
+oo
5 df-mnf 8886 . 2  |-  -oo  =  ~P  +oo
64, 5neeqtrri 2482 1  |-  +oo  =/=  -oo
Colors of variables: wff set class
Syntax hints:    e. wcel 1696    =/= wne 2459   ~Pcpw 3638    +oocpnf 8880    -oocmnf 8881   RR*cxr 8882
This theorem is referenced by:  xrnemnf  10476  xrnepnf  10477  xrltnr  10478  pnfnlt  10483  nltmnf  10484  xnegmnf  10553  xaddpnf1  10569  xaddmnf1  10571  xaddmnf2  10572  mnfaddpnf  10574  xaddnemnf  10577  xaddnepnf  10578  xmullem2  10601  xadddilem  10630  resup  10987  xrge0iifhom  23334  esumpr2  23454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-pow 4204  ax-un 4528  ax-cnex 8809
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-rex 2562  df-rab 2565  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-pw 3640  df-sn 3659  df-pr 3660  df-uni 3844  df-pnf 8885  df-mnf 8886  df-xr 8887
  Copyright terms: Public domain W3C validator