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

Theorem mnfxr 11314
Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
Assertion
Ref Expression
mnfxr  |- -oo  e.  RR*

Proof of Theorem mnfxr
StepHypRef Expression
1 df-mnf 9622 . . . . 5  |- -oo  =  ~P +oo
2 pnfex 11313 . . . . . 6  |- +oo  e.  _V
32pwex 4625 . . . . 5  |-  ~P +oo  e.  _V
41, 3eqeltri 2546 . . . 4  |- -oo  e.  _V
54prid2 4131 . . 3  |- -oo  e.  { +oo , -oo }
6 elun2 3667 . . 3  |-  ( -oo  e.  { +oo , -oo }  -> -oo  e.  ( RR  u.  { +oo , -oo } ) )
75, 6ax-mp 5 . 2  |- -oo  e.  ( RR  u.  { +oo , -oo } )
8 df-xr 9623 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
97, 8eleqtrri 2549 1  |- -oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   _Vcvv 3108    u. cun 3469   ~Pcpw 4005   {cpr 4024   RRcr 9482   +oocpnf 9616   -oocmnf 9617   RR*cxr 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-pow 4620  ax-un 6569  ax-cnex 9539
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815  df-v 3110  df-un 3476  df-in 3478  df-ss 3485  df-pw 4007  df-sn 4023  df-pr 4025  df-uni 4241  df-pnf 9621  df-mnf 9622  df-xr 9623
This theorem is referenced by:  elxr  11316  xrltnr  11321  mnflt  11324  mnfltpnf  11326  nltmnf  11329  mnfle  11333  xrltnsym  11334  ngtmnft  11359  xrre2  11362  xrre3  11363  ge0gtmnf  11364  xnegex  11398  xnegcl  11403  xltnegi  11406  xaddval  11413  xaddf  11414  xmulval  11415  xaddmnf1  11418  xaddmnf2  11419  pnfaddmnf  11420  mnfaddpnf  11421  xlt2add  11443  xsubge0  11444  xmulneg1  11452  xmulf  11455  xmulmnf2  11460  xmulpnf1n  11461  xadddilem  11477  xadddi2  11480  xrsupsslem  11489  xrinfmsslem  11490  xrub  11494  supxrmnf  11500  xrsup0  11506  supxrre  11510  infmxrre  11518  elioc2  11578  elico2  11579  elicc2  11580  ioomax  11590  iccmax  11591  elioomnf  11610  unirnioo  11615  difreicc  11643  resup  11952  sgnmnf  12880  caucvgrlem  13446  xrsdsreclblem  18227  leordtvallem2  19473  leordtval2  19474  lecldbas  19481  pnfnei  19482  mnfnei  19483  icopnfcld  21005  iocmnfcld  21006  blssioo  21030  tgioo  21031  xrtgioo  21041  reconnlem1  21061  reconnlem2  21062  bndth  21188  ovolunnul  21641  ovoliunlem1  21643  ovoliun  21646  ovolicopnf  21665  voliunlem3  21692  volsup  21696  ioombl1lem2  21699  ioombl  21705  volivth  21746  mbfdm  21765  ismbfd  21777  mbfmax  21786  ismbf3d  21791  itg2seq  21879  itg2monolem2  21888  dvferm1lem  22115  dvferm2lem  22117  mdegcl  22199  plypf1  22339  ellogdm  22743  logdmnrp  22745  dvloglem  22752  dvlog2lem  22756  atans2  22985  ressatans  22988  xlemnf  27227  xrinfm  27231  supxrnemnf  27239  xrdifh  27247  xrge00  27324  xrge0neqmnf  27329  tpr2rico  27518  xrge0iifcnv  27539  esumfsupre  27705  esumpfinvallem  27708  esumpcvgval  27712  esumcvg  27720  dya2iocbrsiga  27874  dya2icobrsiga  27875  orvclteel  28039  itg2gt0cn  29636  asindmre  29668  dvasin  29669  dvacos  29670  areacirclem4  29676  areacirclem5  29677  rfcnpre4  30944  eliocre  31068  icoopn  31086  limciccioolb  31120  limsupre  31140  limcresioolb  31142  limcleqr  31143  icccncfext  31183  cncfiooicclem1  31189  itgsubsticclem  31250  fourierdlem32  31396  fourierdlem46  31410  fourierdlem48  31412  fourierdlem49  31413  fourierdlem74  31438  fourierdlem87  31451  fourierdlem88  31452  fourierdlem95  31459  fourierdlem103  31467  fourierdlem104  31468  fourierdlem113  31477  fouriersw  31489
  Copyright terms: Public domain W3C validator