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

Theorem pnfnemnf 10459
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 10455 . . . 4  |-  +oo  e.  RR*
2 pwne 4177 . . . 4  |-  (  +oo  e.  RR*  ->  ~P  +oo  =/=  +oo )
31, 2ax-mp 8 . . 3  |-  ~P  +oo  =/=  +oo
43necomi 2528 . 2  |-  +oo  =/=  ~P 
+oo
5 df-mnf 8870 . 2  |-  -oo  =  ~P  +oo
64, 5neeqtrri 2469 1  |-  +oo  =/=  -oo
Colors of variables: wff set class
Syntax hints:    e. wcel 1684    =/= wne 2446   ~Pcpw 3625    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866
This theorem is referenced by:  xrnemnf  10460  xrnepnf  10461  xrltnr  10462  pnfnlt  10467  nltmnf  10468  xnegmnf  10537  xaddpnf1  10553  xaddmnf1  10555  xaddmnf2  10556  mnfaddpnf  10558  xaddnemnf  10561  xaddnepnf  10562  xmullem2  10585  xadddilem  10614  resup  10971  xrge0iifhom  23319  esumpr2  23439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-pow 4188  ax-un 4512  ax-cnex 8793
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-rex 2549  df-rab 2552  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-pw 3627  df-sn 3646  df-pr 3647  df-uni 3828  df-pnf 8869  df-mnf 8870  df-xr 8871
  Copyright terms: Public domain W3C validator