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

Theorem mnfxr 10048
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 10029 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 10045 . . . . . 6 +∞ ∈ V
32pwex 4813 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2694 . . . 4 -∞ ∈ V
54prid2 4273 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 3764 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 10030 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2697 1 -∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3189  cun 3557  𝒫 cpw 4135  {cpr 4155  cr 9887  +∞cpnf 10023  -∞cmnf 10024  *cxr 10025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-pow 4808  ax-un 6909  ax-cnex 9944
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-v 3191  df-un 3564  df-in 3566  df-ss 3573  df-pw 4137  df-sn 4154  df-pr 4156  df-uni 4408  df-pnf 10028  df-mnf 10029  df-xr 10030
This theorem is referenced by:  elxr  11902  xrltnr  11905  mnflt  11909  mnfltpnf  11912  nltmnf  11915  mnfle  11921  xrltnsym  11922  ngtmnft  11949  xrre2  11952  xrre3  11953  ge0gtmnf  11954  xnegex  11990  xnegcl  11995  xltnegi  11998  xaddval  12005  xaddf  12006  xmulval  12007  xaddmnf1  12010  xaddmnf2  12011  pnfaddmnf  12012  mnfaddpnf  12013  xlt2add  12041  xsubge0  12042  xmulneg1  12050  xmulf  12053  xmulmnf2  12058  xmulpnf1n  12059  xadddilem  12075  xadddi2  12078  xrsupsslem  12088  xrinfmsslem  12089  xrub  12093  supxrmnf  12098  xrsup0  12104  supxrre  12108  infxrre  12117  reltxrnmnf  12122  infmremnf  12123  elioc2  12186  elico2  12187  elicc2  12188  ioomax  12198  iccmax  12199  elioomnf  12218  unirnioo  12223  xrge0neqmnf  12226  difreicc  12254  resup  12614  sgnmnf  13777  caucvgrlem  14345  xrsnsgrp  19714  xrsdsreclblem  19724  leordtvallem2  20938  leordtval2  20939  lecldbas  20946  pnfnei  20947  mnfnei  20948  icopnfcld  22494  iocmnfcld  22495  blssioo  22521  tgioo  22522  xrtgioo  22532  reconnlem1  22552  reconnlem2  22553  bndth  22680  ovolunnul  23191  ovoliunlem1  23193  ovoliun  23196  ovolicopnf  23215  voliunlem3  23243  volsup  23247  ioombl1lem2  23250  ioombl  23256  volivth  23298  mbfdm  23318  ismbfd  23330  mbfmax  23339  ismbf3d  23344  itg2seq  23432  itg2monolem2  23441  dvferm1lem  23668  dvferm2lem  23670  mdegcl  23750  plypf1  23889  ellogdm  24302  logdmnrp  24304  dvloglem  24311  dvlog2lem  24315  atans2  24575  ressatans  24578  xlemnf  29382  xrinfm  29386  supxrnemnf  29401  xrdifh  29409  xrge00  29495  tpr2rico  29764  esumcvgsum  29955  dya2iocbrsiga  30142  dya2icobrsiga  30143  orvclteel  30339  icorempt2  32866  iooelexlt  32877  itg2gt0cn  33132  asindmre  33162  dvasin  33163  dvacos  33164  areacirclem4  33170  areacirclem5  33171  rfcnpre4  38711  xrge0nemnfd  39043  supxrgere  39044  supxrgelem  39048  supxrge  39049  infrpge  39062  infxr  39078  infxrunb2  39079  infleinflem2  39082  infleinf  39083  xrralrecnnge  39108  eliocre  39176  icoopn  39193  icomnfinre  39221  ressiocsup  39223  ressioosup  39224  preimaiocmnf  39230  limciccioolb  39285  limsupre  39305  limcresioolb  39307  limcleqr  39308  limsup0  39358  icccncfext  39431  itgsubsticclem  39524  fourierdlem32  39689  fourierdlem46  39702  fourierdlem48  39704  fourierdlem49  39705  fourierdlem74  39730  fourierdlem87  39743  fourierdlem88  39744  fourierdlem95  39751  fourierdlem103  39759  fourierdlem104  39760  fourierdlem113  39769  fouriersw  39781  etransclem18  39802  etransclem46  39830  ioorrnopnxrlem  39859  gsumge0cl  39921  sge0pr  39944  sge0ssre  39947  hspdifhsp  40163  hspmbllem2  40174  pimltmnf2  40244  pimiooltgt  40254  preimaicomnf  40255  pimdecfgtioc  40258  pimincfltioc  40259  pimdecfgtioo  40260  pimincfltioo  40261  incsmflem  40283  decsmflem  40307  smfres  40330  smfsuplem1  40350  smfsuplem2  40351
  Copyright terms: Public domain W3C validator