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

Theorem mnfxr 10134
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 10115 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 10131 . . . . . 6 +∞ ∈ V
32pwex 4878 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2726 . . . 4 -∞ ∈ V
54prid2 4330 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 3814 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 10116 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2729 1 -∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cun 3605  𝒫 cpw 4191  {cpr 4212  cr 9973  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-pow 4873  ax-un 6991  ax-cnex 10030
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-pw 4193  df-sn 4211  df-pr 4213  df-uni 4469  df-pnf 10114  df-mnf 10115  df-xr 10116
This theorem is referenced by:  elxr  11988  xrltnr  11991  mnflt  11995  mnfltpnf  11998  nltmnf  12001  mnfle  12007  xrltnsym  12008  ngtmnft  12035  xlemnf  12036  xrre2  12039  xrre3  12040  ge0gtmnf  12041  xnegex  12077  xnegcl  12082  xltnegi  12085  xaddval  12092  xaddf  12093  xmulval  12094  xaddmnf1  12097  xaddmnf2  12098  pnfaddmnf  12099  mnfaddpnf  12100  xlt2add  12128  xsubge0  12129  xmulneg1  12137  xmulf  12140  xmulmnf2  12145  xmulpnf1n  12146  xadddilem  12162  xadddi2  12165  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  supxrmnf  12185  xrsup0  12191  supxrre  12195  infxrre  12204  reltxrnmnf  12210  infmremnf  12211  elioc2  12274  elico2  12275  elicc2  12276  ioomax  12286  iccmax  12287  elioomnf  12306  unirnioo  12311  xrge0neqmnf  12314  difreicc  12342  resup  12706  sgnmnf  13879  caucvgrlem  14447  xrsnsgrp  19830  xrsdsreclblem  19840  leordtvallem2  21063  leordtval2  21064  lecldbas  21071  pnfnei  21072  mnfnei  21073  icopnfcld  22618  iocmnfcld  22619  blssioo  22645  tgioo  22646  xrtgioo  22656  reconnlem1  22676  reconnlem2  22677  bndth  22804  ovolunnul  23314  ovoliunlem1  23316  ovoliun  23319  ovolicopnf  23338  voliunlem3  23366  volsup  23370  ioombl1lem2  23373  ioombl  23379  volivth  23421  mbfdm  23440  ismbfd  23452  mbfmax  23461  ismbf3d  23466  itg2seq  23554  itg2monolem2  23563  dvferm1lem  23792  dvferm2lem  23794  mdegcl  23874  plypf1  24013  ellogdm  24430  logdmnrp  24432  dvloglem  24439  dvlog2lem  24443  atans2  24703  ressatans  24706  xrinfm  29647  supxrnemnf  29662  xrdifh  29670  xrge00  29814  tpr2rico  30086  esumcvgsum  30278  dya2iocbrsiga  30465  dya2icobrsiga  30466  orvclteel  30662  icorempt2  33329  iooelexlt  33340  itg2gt0cn  33595  asindmre  33625  dvasin  33626  dvacos  33627  areacirclem4  33633  areacirclem5  33634  rfcnpre4  39507  xrge0nemnfd  39861  supxrgere  39862  supxrgelem  39866  supxrge  39867  infrpge  39880  infxr  39896  infxrunb2  39897  infleinflem2  39900  infleinf  39901  xrralrecnnge  39926  supminfxr2  40012  xrpnf  40029  eliocre  40052  icoopn  40069  icomnfinre  40097  ressiocsup  40099  ressioosup  40100  preimaiocmnf  40106  limciccioolb  40171  limsupre  40191  limcresioolb  40193  limcleqr  40194  limsup0  40244  xlimmnfvlem2  40377  icccncfext  40418  itgsubsticclem  40509  fourierdlem32  40674  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem74  40715  fourierdlem87  40728  fourierdlem88  40729  fourierdlem95  40736  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  fouriersw  40766  etransclem18  40787  etransclem46  40815  ioorrnopnxrlem  40844  gsumge0cl  40906  sge0pr  40929  sge0ssre  40932  hspdifhsp  41151  hspmbllem2  41162  pimltmnf2  41232  pimiooltgt  41242  preimaicomnf  41243  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  incsmflem  41271  decsmflem  41295  smfres  41318  smfsuplem1  41338  smfsuplem2  41339
  Copyright terms: Public domain W3C validator