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

Theorem mnfxr 11414
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  |- -oo  e.  RR*

Proof of Theorem mnfxr
StepHypRef Expression
1 df-mnf 9678 . . . . 5  |- -oo  =  ~P +oo
2 pnfex 11413 . . . . . 6  |- +oo  e.  _V
32pwex 4586 . . . . 5  |-  ~P +oo  e.  _V
41, 3eqeltri 2525 . . . 4  |- -oo  e.  _V
54prid2 4081 . . 3  |- -oo  e.  { +oo , -oo }
6 elun2 3602 . . 3  |-  ( -oo  e.  { +oo , -oo }  -> -oo  e.  ( RR  u.  { +oo , -oo } ) )
75, 6ax-mp 5 . 2  |- -oo  e.  ( RR  u.  { +oo , -oo } )
8 df-xr 9679 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
97, 8eleqtrri 2528 1  |- -oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1887   _Vcvv 3045    u. cun 3402   ~Pcpw 3951   {cpr 3970   RRcr 9538   +oocpnf 9672   -oocmnf 9673   RR*cxr 9674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-pow 4581  ax-un 6583  ax-cnex 9595
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-v 3047  df-un 3409  df-in 3411  df-ss 3418  df-pw 3953  df-sn 3969  df-pr 3971  df-uni 4199  df-pnf 9677  df-mnf 9678  df-xr 9679
This theorem is referenced by:  elxr  11416  xrltnr  11421  mnflt  11425  mnfltpnf  11428  nltmnf  11431  mnfle  11435  xrltnsym  11436  ngtmnft  11462  xrre2  11465  xrre3  11466  ge0gtmnf  11467  xnegex  11501  xnegcl  11506  xltnegi  11509  xaddval  11516  xaddf  11517  xmulval  11518  xaddmnf1  11521  xaddmnf2  11522  pnfaddmnf  11523  mnfaddpnf  11524  xlt2add  11546  xsubge0  11547  xmulneg1  11555  xmulf  11558  xmulmnf2  11563  xmulpnf1n  11564  xadddilem  11580  xadddi2  11583  xrsupsslem  11592  xrinfmsslem  11593  xrub  11597  supxrmnf  11603  xrsup0  11609  supxrre  11613  infxrre  11622  infmxrreOLD  11626  reltxrnmnf  11632  infmremnf  11633  elioc2  11697  elico2  11698  elicc2  11699  ioomax  11709  iccmax  11710  elioomnf  11729  unirnioo  11734  xrge0neqmnf  11737  difreicc  11764  resup  12094  sgnmnf  13158  caucvgrlem  13736  caucvgrlemOLD  13737  xrsnsgrp  19004  xrsdsreclblem  19014  leordtvallem2  20227  leordtval2  20228  lecldbas  20235  pnfnei  20236  mnfnei  20237  icopnfcld  21788  iocmnfcld  21789  blssioo  21813  tgioo  21814  xrtgioo  21824  reconnlem1  21844  reconnlem2  21845  bndth  21986  ovolunnul  22453  ovoliunlem1  22455  ovoliun  22458  ovolicopnf  22478  voliunlem3  22505  volsup  22509  ioombl1lem2  22512  ioombl  22518  volivth  22565  mbfdm  22584  ismbfd  22596  mbfmax  22605  ismbf3d  22610  itg2seq  22700  itg2monolem2  22709  dvferm1lem  22936  dvferm2lem  22938  mdegcl  23018  plypf1  23166  ellogdm  23584  logdmnrp  23586  dvloglem  23593  dvlog2lem  23597  atans2  23857  ressatans  23860  xlemnf  28328  xrinfm  28333  xrinfmOLD  28334  supxrnemnf  28354  xrdifh  28362  xrge00  28448  tpr2rico  28718  esumcvgsum  28909  dya2iocbrsiga  29097  dya2icobrsiga  29098  orvclteel  29305  icorempt2  31754  iooelexlt  31765  itg2gt0cn  31997  asindmre  32027  dvasin  32028  dvacos  32029  areacirclem4  32035  areacirclem5  32036  rfcnpre4  37355  xrge0nemnfd  37555  supxrgere  37556  supxrgelem  37560  supxrge  37561  infrpge  37574  eliocre  37609  icoopn  37626  limciccioolb  37701  limsupre  37721  limsupreOLD  37722  limcresioolb  37724  limcleqr  37725  icccncfext  37765  itgsubsticclem  37852  fourierdlem32  38002  fourierdlem46  38016  fourierdlem48  38018  fourierdlem49  38019  fourierdlem74  38044  fourierdlem87  38057  fourierdlem88  38058  fourierdlem95  38065  fourierdlem103  38073  fourierdlem104  38074  fourierdlem113  38083  fouriersw  38095  etransclem18  38117  etransclem46  38145  gsumge0cl  38213  sge0pr  38236  sge0ssre  38239  hspdifhsp  38438  hspmbllem2  38449
  Copyright terms: Public domain W3C validator