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

Theorem pnfxr 10684
Description: Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
Assertion
Ref Expression
pnfxr +∞ ∈ ℝ*

Proof of Theorem pnfxr
StepHypRef Expression
1 ssun2 4153 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 pnfex 10683 . . . 4 +∞ ∈ V
32prid1 4697 . . 3 +∞ ∈ {+∞, -∞}
41, 3sselii 3968 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
5 df-xr 10668 . 2 * = (ℝ ∪ {+∞, -∞})
64, 5eleqtrri 2917 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  cun 3938  {cpr 4566  cr 10525  +∞cpnf 10661  -∞cmnf 10662  *cxr 10663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-pow 5263  ax-un 7451  ax-cnex 10582
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-v 3502  df-un 3945  df-in 3947  df-ss 3956  df-pw 4544  df-sn 4565  df-pr 4567  df-uni 4838  df-pnf 10666  df-xr 10668
This theorem is referenced by:  pnfnemnf  10685  xnn0xr  11961  xrltnr  12504  ltpnf  12505  mnfltpnf  12511  pnfnlt  12513  pnfge  12515  nltpnft  12547  xgepnf  12548  xrre  12552  xrre2  12553  xnegcl  12596  xaddf  12607  xaddpnf1  12609  xaddpnf2  12610  pnfaddmnf  12613  mnfaddpnf  12614  xaddass2  12633  xlt2add  12643  xsubge0  12644  xmulneg1  12652  xmulf  12655  xmulpnf1  12657  xmulpnf2  12658  xmulmnf1  12659  xmulpnf1n  12661  xlemul1a  12671  xadddilem  12677  xadddi2  12680  xrsupsslem  12690  xrinfmsslem  12691  supxrpnf  12701  supxrunb1  12702  supxrunb2  12703  supxrbnd  12711  xrinf0  12721  elicore  12779  elioc2  12789  elico2  12790  elicc2  12791  ioomax  12801  iccmax  12802  ioopos  12803  elioopnf  12821  elicopnf  12823  unirnioo  12827  xrge0neqmnf  12830  elxrge0  12835  difreicc  12860  xnn0xrge0  12881  ioopnfsup  13222  icopnfsup  13223  xrsup  13226  hashbnd  13686  hashnnn0genn0  13693  hashxrcl  13708  hashdomi  13731  sgnpnf  14442  rexico  14703  limsupgre  14828  rlim3  14845  fprodge0  15337  fprodge1  15339  pcxcl  16187  pc2dvds  16205  pcadd  16215  ramxrcl  16343  ramubcl  16344  xrsnsgrp  20497  xrsdsreclblem  20507  rge0srg  20532  leordtvallem1  21734  leordtval2  21736  lecldbas  21743  pnfnei  21744  mnfnei  21745  xblpnfps  22920  xblpnf  22921  xblss2ps  22926  blssec  22960  blpnfctr  22961  nmoix  23253  icopnfcld  23291  iocmnfcld  23292  xrtgioo  23329  reconnlem1  23349  xrge0tsms  23357  metdstri  23374  iccpnfcnv  23463  ovolf  23998  ovolicopnf  24040  ovolre  24041  volsup  24072  ioombl1lem4  24077  icombl1  24079  icombl  24080  ioombl  24081  uniioombllem1  24097  mbfdm  24142  ismbfd  24155  mbfmax  24165  ismbf3d  24170  itg2ge0  24251  lhop2  24527  dvfsumlem2  24539  dvfsumrlim  24543  dvfsumrlim2  24544  taylfvallem1  24860  taylfval  24862  tayl0  24865  radcnvcl  24920  radcnvle  24923  psercnlem1  24928  logccv  25159  rlimcnp  25457  rlimcnp2  25458  xrlimcnp  25460  logfacbnd3  25713  chebbnd1  25962  chebbnd2  25967  dchrisumlem3  25981  log2sumbnd  26034  pntpbnd1  26076  pntibndlem2  26081  pntlemb  26087  pntleme  26098  pnt  26104  upgrfi  26790  topnfbey  28162  isblo3i  28492  xrge0infss  30397  dfrp2  30404  xrdifh  30416  hashxpe  30442  elxrge02  30522  xdivpnfrp  30523  xrge0addass  30591  xrge0addgt0  30592  xrge0adddir  30593  xrge0npcan  30595  fsumrp0cl  30596  xrge0tsmsd  30606  pnfinf  30726  xrnarchi  30727  xrge0slmod  30831  unitssxrge0  31029  tpr2rico  31041  xrge0iifcnv  31062  xrge0iifiso  31064  xrge0iifhom  31066  xrge0mulc1cn  31070  pnfneige0  31080  lmxrge0  31081  esumle  31203  esumlef  31207  esumcst  31208  esumpr2  31212  esumpinfval  31218  esumpinfsum  31222  esumpcvgval  31223  hashf2  31229  esumcvg  31231  esumcvgsum  31233  voliune  31374  volfiniune  31375  ddemeas  31381  sxbrsigalem0  31415  sxbrsigalem2  31430  oms0  31441  sibfinima  31483  sitmcl  31495  probmeasb  31574  orvcgteel  31611  dstfrvclim1  31621  signsply0  31707  chtvalz  31786  hgt750lemf  31810  iooelexlt  34512  mbfposadd  34806  itg2addnclem2  34811  ftc1anclem5  34838  asindmre  34844  dvasin  34845  dvacos  34846  dvconstbi  40531  rfcnpre3  41155  absfico  41346  xadd0ge  41453  xrgepnfd  41464  xrge0nemnfd  41465  supxrgere  41466  supxrgelem  41470  supxrge  41471  xralrple2  41487  infxr  41500  infleinflem2  41504  xrralrecnnge  41527  infxrpnf  41586  xrpnf  41627  iocopn  41661  pnfel0pnf  41669  ge0xrre  41672  ge0lere  41673  ressiooinf  41698  uzinico  41701  uzubioo  41708  fsumge0cl  41719  limcicciooub  41783  limsupre  41787  limcresiooub  41788  limcleqr  41790  limsupresre  41842  limsupresico  41846  limsuppnfdlem  41847  limsuppnflem  41856  limsupmnflem  41866  liminfresico  41917  limsup10exlem  41918  liminflelimsuplem  41921  liminflelimsupuz  41931  limsupub2  41958  liminflbuz2  41961  liminflimsupxrre  41963  xlimpnfvlem2  41983  xlimliminflimsup  42008  icccncfext  42035  iblsplit  42116  itgsubsticclem  42125  fourierdlem31  42289  fourierdlem33  42291  fourierdlem46  42303  fourierdlem47  42304  fourierdlem48  42305  fourierdlem49  42306  fourierdlem65  42322  fourierdlem73  42330  fourierdlem75  42332  fourierdlem85  42342  fourierdlem88  42345  fourierdlem95  42352  fourierdlem97  42354  fourierdlem103  42360  fourierdlem104  42361  fourierdlem107  42364  fourierdlem109  42366  fourierdlem111  42368  fourierdlem112  42369  fourierdlem113  42370  fouriersw  42382  ioorrnopnxrlem  42457  sge0val  42514  fge0iccico  42518  gsumge0cl  42519  sge0sn  42527  sge0tsms  42528  sge0cl  42529  sge0f1o  42530  sge0ge0  42532  sge0repnf  42534  sge0fsum  42535  sge0pr  42542  sge0prle  42549  sge0split  42557  sge0p1  42562  sge0iunmptlemre  42563  sge0rpcpnf  42569  sge0rernmpt  42570  sge0isum  42575  sge0ad2en  42579  sge0xaddlem1  42581  sge0xaddlem2  42582  sge0uzfsumgt  42592  sge0seq  42594  sge0reuz  42595  voliunsge0lem  42620  meage0  42623  meassre  42625  meaiuninclem  42628  omessre  42658  omeiunltfirp  42667  carageniuncllem2  42670  carageniuncl  42671  omege0  42681  hoiprodcl  42695  hoicvrrex  42704  ovnpnfelsup  42707  ovnlerp  42710  ovnf  42711  ovn0lem  42713  ovnsubaddlem1  42718  hoiprodcl3  42728  hoidmvcl  42730  sge0hsphoire  42737  hoidmv1lelem1  42739  hoidmv1lelem2  42740  hoidmv1lelem3  42741  hoidmv1le  42742  hoidmvlelem1  42743  hoidmvlelem4  42746  hoidmvlelem5  42747  ovnhoilem1  42749  volicorege0  42785  ovolval5lem1  42800  pimgtpnf2  42851  pimiooltgt  42855  smfliminflem  42970  rrxsphere  44567  itscnhlinecirc02p  44604
  Copyright terms: Public domain W3C validator