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

Theorem mnfxr 11415
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 9679 . . . . 5  |- -oo  =  ~P +oo
2 pnfex 11414 . . . . . 6  |- +oo  e.  _V
32pwex 4604 . . . . 5  |-  ~P +oo  e.  _V
41, 3eqeltri 2506 . . . 4  |- -oo  e.  _V
54prid2 4106 . . 3  |- -oo  e.  { +oo , -oo }
6 elun2 3634 . . 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 9680 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
97, 8eleqtrri 2509 1  |- -oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   _Vcvv 3081    u. cun 3434   ~Pcpw 3979   {cpr 3998   RRcr 9539   +oocpnf 9673   -oocmnf 9674   RR*cxr 9675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-pow 4599  ax-un 6594  ax-cnex 9596
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rex 2781  df-v 3083  df-un 3441  df-in 3443  df-ss 3450  df-pw 3981  df-sn 3997  df-pr 3999  df-uni 4217  df-pnf 9678  df-mnf 9679  df-xr 9680
This theorem is referenced by:  elxr  11417  xrltnr  11422  mnflt  11426  mnfltpnf  11429  nltmnf  11432  mnfle  11436  xrltnsym  11437  ngtmnft  11463  xrre2  11466  xrre3  11467  ge0gtmnf  11468  xnegex  11502  xnegcl  11507  xltnegi  11510  xaddval  11517  xaddf  11518  xmulval  11519  xaddmnf1  11522  xaddmnf2  11523  pnfaddmnf  11524  mnfaddpnf  11525  xlt2add  11547  xsubge0  11548  xmulneg1  11556  xmulf  11559  xmulmnf2  11564  xmulpnf1n  11565  xadddilem  11581  xadddi2  11584  xrsupsslem  11593  xrinfmsslem  11594  xrub  11598  supxrmnf  11604  xrsup0  11610  supxrre  11614  infxrre  11623  infmxrreOLD  11627  reltxrnmnf  11633  infmremnf  11634  elioc2  11698  elico2  11699  elicc2  11700  ioomax  11710  iccmax  11711  elioomnf  11730  unirnioo  11735  xrge0neqmnf  11738  difreicc  11765  resup  12094  sgnmnf  13147  caucvgrlem  13724  caucvgrlemOLD  13725  xrsnsgrp  18992  xrsdsreclblem  19002  leordtvallem2  20214  leordtval2  20215  lecldbas  20222  pnfnei  20223  mnfnei  20224  icopnfcld  21775  iocmnfcld  21776  blssioo  21800  tgioo  21801  xrtgioo  21811  reconnlem1  21831  reconnlem2  21832  bndth  21973  ovolunnul  22440  ovoliunlem1  22442  ovoliun  22445  ovolicopnf  22465  voliunlem3  22492  volsup  22496  ioombl1lem2  22499  ioombl  22505  volivth  22552  mbfdm  22571  ismbfd  22583  mbfmax  22592  ismbf3d  22597  itg2seq  22687  itg2monolem2  22696  dvferm1lem  22923  dvferm2lem  22925  mdegcl  23005  plypf1  23153  ellogdm  23571  logdmnrp  23573  dvloglem  23580  dvlog2lem  23584  atans2  23844  ressatans  23847  xlemnf  28322  xrinfm  28327  xrinfmOLD  28328  supxrnemnf  28348  xrdifh  28356  xrge00  28443  tpr2rico  28714  esumcvgsum  28905  dya2iocbrsiga  29093  dya2icobrsiga  29094  orvclteel  29301  icorempt2  31695  iooelexlt  31706  itg2gt0cn  31911  asindmre  31941  dvasin  31942  dvacos  31943  areacirclem4  31949  areacirclem5  31950  rfcnpre4  37216  xrge0nemnfd  37397  supxrgere  37398  supxrgelem  37402  supxrge  37403  infrpge  37416  eliocre  37440  icoopn  37457  limciccioolb  37521  limsupre  37541  limsupreOLD  37542  limcresioolb  37544  limcleqr  37545  icccncfext  37585  itgsubsticclem  37672  fourierdlem32  37822  fourierdlem46  37836  fourierdlem48  37838  fourierdlem49  37839  fourierdlem74  37864  fourierdlem87  37877  fourierdlem88  37878  fourierdlem95  37885  fourierdlem103  37893  fourierdlem104  37894  fourierdlem113  37903  fouriersw  37915  etransclem18  37937  etransclem46  37965  gsumge0cl  38001  sge0pr  38024  sge0ssre  38027
  Copyright terms: Public domain W3C validator