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

Theorem mnfxr 10691
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 10671 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 10687 . . . . . 6 +∞ ∈ V
32pwex 5249 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2889 . . . 4 -∞ ∈ V
54prid2 4662 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 4107 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 10672 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2892 1 -∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  Vcvv 3444  cun 3882  𝒫 cpw 4500  {cpr 4530  cr 10529  +∞cpnf 10665  -∞cmnf 10666  *cxr 10667
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-pow 5234  ax-un 7445  ax-cnex 10586
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-pw 4502  df-sn 4529  df-pr 4531  df-uni 4804  df-pnf 10670  df-mnf 10671  df-xr 10672
This theorem is referenced by:  elxr  12503  xrltnr  12506  mnflt  12510  mnfltpnf  12513  nltmnf  12516  mnfle  12521  xrltnsym  12522  ngtmnft  12551  xlemnf  12552  xrre2  12555  xrre3  12556  ge0gtmnf  12557  xnegex  12593  xnegcl  12598  xltnegi  12601  xaddval  12608  xaddf  12609  xmulval  12610  xaddmnf1  12613  xaddmnf2  12614  pnfaddmnf  12615  mnfaddpnf  12616  xlt2add  12645  xsubge0  12646  xmulneg1  12654  xmulf  12657  xmulmnf2  12662  xmulpnf1n  12663  xadddilem  12679  xadddi2  12682  xrsupsslem  12692  xrinfmsslem  12693  xrub  12697  supxrmnf  12702  xrsup0  12708  supxrre  12712  infxrre  12721  reltxrnmnf  12727  infmremnf  12728  elioc2  12792  elico2  12793  elicc2  12794  ioomax  12804  iccmax  12805  elioomnf  12826  unirnioo  12831  difreicc  12866  resup  13234  sgnmnf  14449  caucvgrlem  15024  xrsnsgrp  20130  xrsdsreclblem  20140  leordtvallem2  21819  leordtval2  21820  lecldbas  21827  pnfnei  21828  mnfnei  21829  icopnfcld  23376  iocmnfcld  23377  blssioo  23403  tgioo  23404  xrtgioo  23414  reconnlem1  23434  reconnlem2  23435  bndth  23566  ovolunnul  24107  ovoliunlem1  24109  ovoliun  24112  ovolicopnf  24131  voliunlem3  24159  volsup  24163  ioombl1lem2  24166  ioombl  24172  volivth  24214  mbfdm  24233  ismbfd  24246  mbfmax  24256  ismbf3d  24261  itg2seq  24349  itg2monolem2  24358  dvferm1lem  24590  dvferm2lem  24592  mdegcl  24673  plypf1  24812  ellogdm  25233  logdmnrp  25235  dvloglem  25242  dvlog2lem  25246  atans2  25520  ressatans  25523  xrinfm  30507  supxrnemnf  30522  xrdifh  30532  xrge00  30723  tpr2rico  31263  esumcvgsum  31455  dya2iocbrsiga  31641  dya2icobrsiga  31642  orvclteel  31838  icorempo  34763  iooelexlt  34774  itg2gt0cn  35105  asindmre  35133  dvasin  35134  dvacos  35135  areacirclem4  35141  areacirclem5  35142  rfcnpre4  41650  xrge0nemnfd  41951  supxrgere  41952  supxrgelem  41956  supxrge  41957  infrpge  41970  infxr  41986  infxrunb2  41987  infleinflem2  41990  infleinf  41991  xrralrecnnge  42013  supminfxr2  42095  xrpnf  42112  eliocre  42133  icoopn  42149  icomnfinre  42176  ressiocsup  42178  ressioosup  42179  preimaiocmnf  42185  limciccioolb  42250  limsupre  42270  limcresioolb  42272  limcleqr  42273  limsup0  42323  liminflbuz2  42444  liminfpnfuz  42445  liminflimsupxrre  42446  xlimmnfvlem2  42462  xlimliminflimsup  42491  icccncfext  42516  itgsubsticclem  42604  fourierdlem32  42768  fourierdlem46  42781  fourierdlem48  42783  fourierdlem49  42784  fourierdlem74  42809  fourierdlem87  42822  fourierdlem88  42823  fourierdlem95  42830  fourierdlem103  42838  fourierdlem104  42839  fourierdlem113  42848  fouriersw  42860  etransclem18  42881  etransclem46  42909  ioorrnopnxrlem  42935  gsumge0cl  42997  sge0pr  43020  sge0ssre  43023  hspdifhsp  43242  hspmbllem2  43253  pimltmnf2  43323  pimiooltgt  43333  preimaicomnf  43334  pimdecfgtioc  43337  pimincfltioc  43338  pimdecfgtioo  43339  pimincfltioo  43340  incsmflem  43362  decsmflem  43386  smfres  43409  smfsuplem1  43429  smfsuplem2  43430
  Copyright terms: Public domain W3C validator