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

Theorem pnfnemnf 10709
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 10705 . . . 4  |-  +oo  e.  RR*
2 pwne 4358 . . . 4  |-  (  +oo  e.  RR*  ->  ~P  +oo  =/=  +oo )
31, 2ax-mp 8 . . 3  |-  ~P  +oo  =/=  +oo
43necomi 2680 . 2  |-  +oo  =/=  ~P 
+oo
5 df-mnf 9115 . 2  |-  -oo  =  ~P  +oo
64, 5neeqtrri 2621 1  |-  +oo  =/=  -oo
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    =/= wne 2598   ~Pcpw 3791    +oocpnf 9109    -oocmnf 9110   RR*cxr 9111
This theorem is referenced by:  xrnemnf  10710  xrnepnf  10711  xrltnr  10712  pnfnlt  10717  nltmnf  10718  xnegmnf  10788  xaddpnf1  10804  xaddmnf1  10806  xaddmnf2  10807  mnfaddpnf  10809  xaddnemnf  10812  xaddnepnf  10813  xmullem2  10836  xadddilem  10865  resup  11240  hashnemnf  11620  xrge0iifhom  24315  esumpr2  24450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-pow 4369  ax-un 4693  ax-cnex 9038
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-rex 2703  df-rab 2706  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-pw 3793  df-sn 3812  df-pr 3813  df-uni 4008  df-pnf 9114  df-mnf 9115  df-xr 9116
  Copyright terms: Public domain W3C validator