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

Theorem mnfxr 11376
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 9661 . . . . 5  |- -oo  =  ~P +oo
2 pnfex 11375 . . . . . 6  |- +oo  e.  _V
32pwex 4577 . . . . 5  |-  ~P +oo  e.  _V
41, 3eqeltri 2486 . . . 4  |- -oo  e.  _V
54prid2 4081 . . 3  |- -oo  e.  { +oo , -oo }
6 elun2 3611 . . 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 9662 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
97, 8eleqtrri 2489 1  |- -oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842   _Vcvv 3059    u. cun 3412   ~Pcpw 3955   {cpr 3974   RRcr 9521   +oocpnf 9655   -oocmnf 9656   RR*cxr 9657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-pow 4572  ax-un 6574  ax-cnex 9578
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2760  df-v 3061  df-un 3419  df-in 3421  df-ss 3428  df-pw 3957  df-sn 3973  df-pr 3975  df-uni 4192  df-pnf 9660  df-mnf 9661  df-xr 9662
This theorem is referenced by:  elxr  11378  xrltnr  11383  mnflt  11386  mnfltpnf  11388  nltmnf  11391  mnfle  11395  xrltnsym  11396  ngtmnft  11421  xrre2  11424  xrre3  11425  ge0gtmnf  11426  xnegex  11460  xnegcl  11465  xltnegi  11468  xaddval  11475  xaddf  11476  xmulval  11477  xaddmnf1  11480  xaddmnf2  11481  pnfaddmnf  11482  mnfaddpnf  11483  xlt2add  11505  xsubge0  11506  xmulneg1  11514  xmulf  11517  xmulmnf2  11522  xmulpnf1n  11523  xadddilem  11539  xadddi2  11542  xrsupsslem  11551  xrinfmsslem  11552  xrub  11556  supxrmnf  11562  xrsup0  11568  supxrre  11572  infmxrre  11580  elioc2  11641  elico2  11642  elicc2  11643  ioomax  11653  iccmax  11654  elioomnf  11673  unirnioo  11678  difreicc  11706  resup  12032  sgnmnf  13077  caucvgrlem  13644  xrsnsgrp  18774  xrsdsreclblem  18784  leordtvallem2  20005  leordtval2  20006  lecldbas  20013  pnfnei  20014  mnfnei  20015  icopnfcld  21567  iocmnfcld  21568  blssioo  21592  tgioo  21593  xrtgioo  21603  reconnlem1  21623  reconnlem2  21624  bndth  21750  ovolunnul  22203  ovoliunlem1  22205  ovoliun  22208  ovolicopnf  22227  voliunlem3  22254  volsup  22258  ioombl1lem2  22261  ioombl  22267  volivth  22308  mbfdm  22327  ismbfd  22339  mbfmax  22348  ismbf3d  22353  itg2seq  22441  itg2monolem2  22450  dvferm1lem  22677  dvferm2lem  22679  mdegcl  22761  plypf1  22901  ellogdm  23314  logdmnrp  23316  dvloglem  23323  dvlog2lem  23327  atans2  23587  ressatans  23590  xlemnf  28012  xrinfm  28016  supxrnemnf  28031  xrdifh  28039  xrge00  28126  xrge0neqmnf  28131  tpr2rico  28347  esumcvgsum  28535  dya2iocbrsiga  28723  dya2icobrsiga  28724  orvclteel  28917  icorempt2  31268  iooelexlt  31279  itg2gt0cn  31443  asindmre  31473  dvasin  31474  dvacos  31475  areacirclem4  31481  areacirclem5  31482  rfcnpre4  36789  eliocre  36915  icoopn  36933  limciccioolb  36995  limsupre  37015  limcresioolb  37017  limcleqr  37018  icccncfext  37058  itgsubsticclem  37142  fourierdlem32  37289  fourierdlem46  37303  fourierdlem48  37305  fourierdlem49  37306  fourierdlem74  37331  fourierdlem87  37344  fourierdlem88  37345  fourierdlem95  37352  fourierdlem103  37360  fourierdlem104  37361  fourierdlem113  37370  fouriersw  37382  etransclem18  37403  etransclem46  37431
  Copyright terms: Public domain W3C validator