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

Theorem mnfxr 11211
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 -∞ ∈ ℝ*

Proof of Theorem mnfxr
StepHypRef Expression
1 df-mnf 11191 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 11207 . . . . . 6 +∞ ∈ V
32pwex 5335 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2834 . . . 4 -∞ ∈ V
54prid2 4724 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 4137 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 11192 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2837 1 -∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3445  cun 3908  𝒫 cpw 4560  {cpr 4588  cr 11049  +∞cpnf 11185  -∞cmnf 11186  *cxr 11187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-pow 5320  ax-un 7671  ax-cnex 11106
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-un 3915  df-in 3917  df-ss 3927  df-pw 4562  df-sn 4587  df-pr 4589  df-uni 4866  df-pnf 11190  df-mnf 11191  df-xr 11192
This theorem is referenced by:  elxr  13036  xrltnr  13039  mnflt  13043  mnfltpnf  13046  nltmnf  13049  mnfle  13054  xrltnsym  13055  ngtmnft  13084  xlemnf  13085  xrre2  13088  xrre3  13089  ge0gtmnf  13090  xnegex  13126  xnegcl  13131  xltnegi  13134  xaddval  13141  xaddf  13142  xmulval  13143  xaddmnf1  13146  xaddmnf2  13147  pnfaddmnf  13148  mnfaddpnf  13149  xlt2add  13178  xsubge0  13179  xmulneg1  13187  xmulf  13190  xmulmnf2  13195  xmulpnf1n  13196  xadddilem  13212  xadddi2  13215  xrsupsslem  13225  xrinfmsslem  13226  xrub  13230  supxrmnf  13235  xrsup0  13241  supxrre  13245  infxrre  13254  reltxrnmnf  13260  infmremnf  13261  elioc2  13326  elico2  13327  elicc2  13328  ioomax  13338  iccmax  13339  elioomnf  13360  unirnioo  13365  difreicc  13400  resup  13771  sgnmnf  14979  caucvgrlem  15556  xrsnsgrp  20831  xrsdsreclblem  20841  leordtvallem2  22560  leordtval2  22561  lecldbas  22568  pnfnei  22569  mnfnei  22570  icopnfcld  24129  iocmnfcld  24130  blssioo  24156  tgioo  24157  xrtgioo  24167  reconnlem1  24187  reconnlem2  24188  bndth  24319  ovolunnul  24862  ovoliunlem1  24864  ovoliun  24867  ovolicopnf  24886  voliunlem3  24914  volsup  24918  ioombl1lem2  24921  ioombl  24927  volivth  24969  mbfdm  24988  ismbfd  25001  mbfmax  25011  ismbf3d  25016  itg2seq  25105  itg2monolem2  25114  dvferm1lem  25346  dvferm2lem  25348  mdegcl  25432  plypf1  25571  ellogdm  25992  logdmnrp  25994  dvloglem  26001  dvlog2lem  26005  atans2  26279  ressatans  26282  xrinfm  31654  supxrnemnf  31668  xrdifh  31678  xrge00  31872  tpr2rico  32484  esumcvgsum  32678  dya2iocbrsiga  32866  dya2icobrsiga  32867  orvclteel  33063  icorempo  35813  iooelexlt  35824  itg2gt0cn  36124  asindmre  36152  dvasin  36153  dvacos  36154  areacirclem4  36160  areacirclem5  36161  rfcnpre4  43221  xrge0nemnfd  43542  supxrgere  43543  supxrgelem  43547  supxrge  43548  infrpge  43561  infxr  43577  infxrunb2  43578  infleinflem2  43581  infleinf  43582  xrralrecnnge  43601  supminfxr2  43680  xrpnf  43697  eliocre  43719  icoopn  43735  icomnfinre  43762  ressiocsup  43764  ressioosup  43765  preimaiocmnf  43771  limciccioolb  43834  limsupre  43854  limcresioolb  43856  limcleqr  43857  limsup0  43907  liminflbuz2  44028  liminfpnfuz  44029  liminflimsupxrre  44030  xlimmnfvlem2  44046  xlimliminflimsup  44075  icccncfext  44100  itgsubsticclem  44188  fourierdlem32  44352  fourierdlem46  44365  fourierdlem48  44367  fourierdlem49  44368  fourierdlem74  44393  fourierdlem87  44406  fourierdlem88  44407  fourierdlem95  44414  fourierdlem103  44422  fourierdlem104  44423  fourierdlem113  44432  fouriersw  44444  etransclem18  44465  etransclem46  44493  ioorrnopnxrlem  44519  gsumge0cl  44584  sge0pr  44607  sge0ssre  44610  hspdifhsp  44829  hspmbllem2  44840  pimltmnf2f  44910  pimiooltgt  44923  preimaicomnf  44924  pimdecfgtioc  44928  pimincfltioc  44929  pimdecfgtioo  44930  pimincfltioo  44931  incsmflem  44954  decsmflem  44979  smfres  45003  smfsuplem1  45024  smfsuplem2  45025
  Copyright terms: Public domain W3C validator