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

Theorem mnfxr 11352
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 9652 . . . . 5
2 pnfex 11351 . . . . . 6
32pwex 4635 . . . . 5
41, 3eqeltri 2541 . . . 4
54prid2 4139 . . 3
6 elun2 3671 . . 3
75, 6ax-mp 5 . 2
8 df-xr 9653 . 2
97, 8eleqtrri 2544 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  u.cun 3473  ~Pcpw 4012  {cpr 4031   cr 9512   cpnf 9646   cmnf 9647   cxr 9648
This theorem is referenced by:  elxr  11354  xrltnr  11359  mnflt  11362  mnfltpnf  11364  nltmnf  11367  mnfle  11371  xrltnsym  11372  ngtmnft  11397  xrre2  11400  xrre3  11401  ge0gtmnf  11402  xnegex  11436  xnegcl  11441  xltnegi  11444  xaddval  11451  xaddf  11452  xmulval  11453  xaddmnf1  11456  xaddmnf2  11457  pnfaddmnf  11458  mnfaddpnf  11459  xlt2add  11481  xsubge0  11482  xmulneg1  11490  xmulf  11493  xmulmnf2  11498  xmulpnf1n  11499  xadddilem  11515  xadddi2  11518  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrmnf  11538  xrsup0  11544  supxrre  11548  infmxrre  11556  elioc2  11616  elico2  11617  elicc2  11618  ioomax  11628  iccmax  11629  elioomnf  11648  unirnioo  11653  difreicc  11681  resup  11994  sgnmnf  12928  caucvgrlem  13495  xrsnsgrp  18454  xrsdsreclblem  18464  leordtvallem2  19712  leordtval2  19713  lecldbas  19720  pnfnei  19721  mnfnei  19722  icopnfcld  21275  iocmnfcld  21276  blssioo  21300  tgioo  21301  xrtgioo  21311  reconnlem1  21331  reconnlem2  21332  bndth  21458  ovolunnul  21911  ovoliunlem1  21913  ovoliun  21916  ovolicopnf  21935  voliunlem3  21962  volsup  21966  ioombl1lem2  21969  ioombl  21975  volivth  22016  mbfdm  22035  ismbfd  22047  mbfmax  22056  ismbf3d  22061  itg2seq  22149  itg2monolem2  22158  dvferm1lem  22385  dvferm2lem  22387  mdegcl  22469  plypf1  22609  ellogdm  23020  logdmnrp  23022  dvloglem  23029  dvlog2lem  23033  atans2  23262  ressatans  23265  xlemnf  27571  xrinfm  27575  supxrnemnf  27583  xrdifh  27591  xrge00  27674  xrge0neqmnf  27679  tpr2rico  27894  dya2iocbrsiga  28246  dya2icobrsiga  28247  orvclteel  28411  itg2gt0cn  30070  asindmre  30102  dvasin  30103  dvacos  30104  areacirclem4  30110  areacirclem5  30111  rfcnpre4  31409  eliocre  31547  icoopn  31565  limciccioolb  31627  limsupre  31647  limcresioolb  31649  limcleqr  31650  icccncfext  31690  itgsubsticclem  31774  fourierdlem32  31921  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem74  31963  fourierdlem87  31976  fourierdlem88  31977  fourierdlem95  31984  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  fouriersw  32014  etransclem18  32035  etransclem46  32063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-pow 4630  ax-un 6592  ax-cnex 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-pw 4014  df-sn 4030  df-pr 4032  df-uni 4250  df-pnf 9651  df-mnf 9652  df-xr 9653
  Copyright terms: Public domain W3C validator