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

Theorem mnfxr 9975
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 9956 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 9972 . . . . . 6 +∞ ∈ V
32pwex 4774 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2684 . . . 4 -∞ ∈ V
54prid2 4242 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 3743 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 9957 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2687 1 -∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  Vcvv 3173  cun 3538  𝒫 cpw 4108  {cpr 4127  cr 9814  +∞cpnf 9950  -∞cmnf 9951  *cxr 9952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-pow 4769  ax-un 6847  ax-cnex 9871
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-pw 4110  df-sn 4126  df-pr 4128  df-uni 4373  df-pnf 9955  df-mnf 9956  df-xr 9957
This theorem is referenced by:  elxr  11826  xrltnr  11829  mnflt  11833  mnfltpnf  11836  nltmnf  11839  mnfle  11845  xrltnsym  11846  ngtmnft  11872  xrre2  11875  xrre3  11876  ge0gtmnf  11877  xnegex  11913  xnegcl  11918  xltnegi  11921  xaddval  11928  xaddf  11929  xmulval  11930  xaddmnf1  11933  xaddmnf2  11934  pnfaddmnf  11935  mnfaddpnf  11936  xlt2add  11962  xsubge0  11963  xmulneg1  11971  xmulf  11974  xmulmnf2  11979  xmulpnf1n  11980  xadddilem  11996  xadddi2  11999  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrmnf  12019  xrsup0  12025  supxrre  12029  infxrre  12038  reltxrnmnf  12043  infmremnf  12044  elioc2  12107  elico2  12108  elicc2  12109  ioomax  12119  iccmax  12120  elioomnf  12139  unirnioo  12144  xrge0neqmnf  12147  difreicc  12175  resup  12528  sgnmnf  13683  caucvgrlem  14251  xrsnsgrp  19601  xrsdsreclblem  19611  leordtvallem2  20825  leordtval2  20826  lecldbas  20833  pnfnei  20834  mnfnei  20835  icopnfcld  22381  iocmnfcld  22382  blssioo  22406  tgioo  22407  xrtgioo  22417  reconnlem1  22437  reconnlem2  22438  bndth  22565  ovolunnul  23075  ovoliunlem1  23077  ovoliun  23080  ovolicopnf  23099  voliunlem3  23127  volsup  23131  ioombl1lem2  23134  ioombl  23140  volivth  23181  mbfdm  23201  ismbfd  23213  mbfmax  23222  ismbf3d  23227  itg2seq  23315  itg2monolem2  23324  dvferm1lem  23551  dvferm2lem  23553  mdegcl  23633  plypf1  23772  ellogdm  24185  logdmnrp  24187  dvloglem  24194  dvlog2lem  24198  atans2  24458  ressatans  24461  xlemnf  28905  xrinfm  28909  supxrnemnf  28924  xrdifh  28932  xrge00  29017  tpr2rico  29286  esumcvgsum  29477  dya2iocbrsiga  29664  dya2icobrsiga  29665  orvclteel  29861  icorempt2  32375  iooelexlt  32386  itg2gt0cn  32635  asindmre  32665  dvasin  32666  dvacos  32667  areacirclem4  32673  areacirclem5  32674  rfcnpre4  38216  xrge0nemnfd  38489  supxrgere  38490  supxrgelem  38494  supxrge  38495  infrpge  38508  infxr  38524  infxrunb2  38525  infleinflem2  38528  infleinf  38529  xrralrecnnge  38554  eliocre  38581  icoopn  38598  icomnfinre  38626  ressiocsup  38628  ressioosup  38629  limciccioolb  38688  limsupre  38708  limcresioolb  38710  limcleqr  38711  icccncfext  38773  itgsubsticclem  38867  fourierdlem32  39032  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem74  39073  fourierdlem87  39086  fourierdlem88  39087  fourierdlem95  39094  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  fouriersw  39124  etransclem18  39145  etransclem46  39173  ioorrnopnxrlem  39202  gsumge0cl  39264  sge0pr  39287  sge0ssre  39290  hspdifhsp  39506  hspmbllem2  39517  pimltmnf2  39588  pimiooltgt  39598  preimaicomnf  39599  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  incsmflem  39628  decsmflem  39652  smfres  39675
  Copyright terms: Public domain W3C validator