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

Theorem mnfxr 11348
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 9648 . . . . 5  |- -oo  =  ~P +oo
2 pnfex 11347 . . . . . 6  |- +oo  e.  _V
32pwex 4639 . . . . 5  |-  ~P +oo  e.  _V
41, 3eqeltri 2541 . . . 4  |- -oo  e.  _V
54prid2 4141 . . 3  |- -oo  e.  { +oo , -oo }
6 elun2 3668 . . 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 9649 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
97, 8eleqtrri 2544 1  |- -oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1819   _Vcvv 3109    u. cun 3469   ~Pcpw 4015   {cpr 4034   RRcr 9508   +oocpnf 9642   -oocmnf 9643   RR*cxr 9644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-pow 4634  ax-un 6591  ax-cnex 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3476  df-in 3478  df-ss 3485  df-pw 4017  df-sn 4033  df-pr 4035  df-uni 4252  df-pnf 9647  df-mnf 9648  df-xr 9649
This theorem is referenced by:  elxr  11350  xrltnr  11355  mnflt  11358  mnfltpnf  11360  nltmnf  11363  mnfle  11367  xrltnsym  11368  ngtmnft  11393  xrre2  11396  xrre3  11397  ge0gtmnf  11398  xnegex  11432  xnegcl  11437  xltnegi  11440  xaddval  11447  xaddf  11448  xmulval  11449  xaddmnf1  11452  xaddmnf2  11453  pnfaddmnf  11454  mnfaddpnf  11455  xlt2add  11477  xsubge0  11478  xmulneg1  11486  xmulf  11489  xmulmnf2  11494  xmulpnf1n  11495  xadddilem  11511  xadddi2  11514  xrsupsslem  11523  xrinfmsslem  11524  xrub  11528  supxrmnf  11534  xrsup0  11540  supxrre  11544  infmxrre  11552  elioc2  11612  elico2  11613  elicc2  11614  ioomax  11624  iccmax  11625  elioomnf  11644  unirnioo  11649  difreicc  11677  resup  11996  sgnmnf  12939  caucvgrlem  13506  xrsnsgrp  18580  xrsdsreclblem  18590  leordtvallem2  19838  leordtval2  19839  lecldbas  19846  pnfnei  19847  mnfnei  19848  icopnfcld  21400  iocmnfcld  21401  blssioo  21425  tgioo  21426  xrtgioo  21436  reconnlem1  21456  reconnlem2  21457  bndth  21583  ovolunnul  22036  ovoliunlem1  22038  ovoliun  22041  ovolicopnf  22060  voliunlem3  22087  volsup  22091  ioombl1lem2  22094  ioombl  22100  volivth  22141  mbfdm  22160  ismbfd  22172  mbfmax  22181  ismbf3d  22186  itg2seq  22274  itg2monolem2  22283  dvferm1lem  22510  dvferm2lem  22512  mdegcl  22594  plypf1  22734  ellogdm  23145  logdmnrp  23147  dvloglem  23154  dvlog2lem  23158  atans2  23387  ressatans  23390  xlemnf  27721  xrinfm  27725  supxrnemnf  27735  xrdifh  27743  xrge00  27826  xrge0neqmnf  27831  tpr2rico  28047  esumcvgsum  28250  dya2iocbrsiga  28407  dya2icobrsiga  28408  orvclteel  28586  itg2gt0cn  30232  asindmre  30264  dvasin  30265  dvacos  30266  areacirclem4  30272  areacirclem5  30273  rfcnpre4  31570  eliocre  31708  icoopn  31726  limciccioolb  31788  limsupre  31808  limcresioolb  31810  limcleqr  31811  icccncfext  31851  itgsubsticclem  31935  fourierdlem32  32082  fourierdlem46  32096  fourierdlem48  32098  fourierdlem49  32099  fourierdlem74  32124  fourierdlem87  32137  fourierdlem88  32138  fourierdlem95  32145  fourierdlem103  32153  fourierdlem104  32154  fourierdlem113  32163  fouriersw  32175  etransclem18  32196  etransclem46  32224
  Copyright terms: Public domain W3C validator