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

Theorem pnfxr 11143
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 4132 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 pnfex 11142 . . . 4 +∞ ∈ V
32prid1 4722 . . 3 +∞ ∈ {+∞, -∞}
41, 3sselii 3940 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
5 df-xr 11127 . 2 * = (ℝ ∪ {+∞, -∞})
64, 5eleqtrri 2838 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  cun 3907  {cpr 4587  cr 10984  +∞cpnf 11120  -∞cmnf 11121  *cxr 11122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-sep 5255  ax-pow 5319  ax-un 7663  ax-cnex 11041
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-un 3914  df-in 3916  df-ss 3926  df-pw 4561  df-sn 4586  df-pr 4588  df-uni 4865  df-pnf 11125  df-xr 11127
This theorem is referenced by:  pnfnemnf  11144  xnn0xr  12424  xrltnr  12969  ltpnf  12970  mnfltpnf  12976  pnfnlt  12978  pnfge  12980  nltpnft  13012  xgepnf  13013  xrre  13017  xrre2  13018  xnegcl  13061  xaddf  13072  xaddpnf1  13074  xaddpnf2  13075  pnfaddmnf  13078  mnfaddpnf  13079  xaddass2  13098  xlt2add  13108  xsubge0  13109  xmulneg1  13117  xmulf  13120  xmulpnf1  13122  xmulpnf2  13123  xmulmnf1  13124  xmulpnf1n  13126  xlemul1a  13136  xadddilem  13142  xadddi2  13145  xrsupsslem  13155  xrinfmsslem  13156  supxrpnf  13166  supxrunb1  13167  supxrunb2  13168  supxrbnd  13176  xrinf0  13186  dfrp2  13242  elicore  13245  elioc2  13256  elico2  13257  elicc2  13258  ioomax  13268  iccmax  13269  ioopos  13270  elioopnf  13289  elicopnf  13291  unirnioo  13295  xrge0neqmnf  13298  elxrge0  13303  difreicc  13330  xnn0xrge0  13352  ioopnfsup  13698  icopnfsup  13699  xrsup  13702  hashbnd  14164  hashnnn0genn0  14171  hashxrcl  14185  hashdomi  14208  sgnpnf  14912  rexico  15173  limsupgre  15298  rlim3  15315  fprodge0  15811  fprodge1  15813  pcxcl  16668  pc2dvds  16686  pcadd  16696  ramxrcl  16824  ramubcl  16825  xrsnsgrp  20757  xrsdsreclblem  20767  rge0srg  20792  leordtvallem1  22484  leordtval2  22486  lecldbas  22493  pnfnei  22494  mnfnei  22495  xblpnfps  23671  xblpnf  23672  xblss2ps  23677  blssec  23711  blpnfctr  23712  nmoix  24016  icopnfcld  24054  iocmnfcld  24055  xrtgioo  24092  reconnlem1  24112  xrge0tsms  24120  metdstri  24137  iccpnfcnv  24230  ovolf  24769  ovolicopnf  24811  ovolre  24812  volsup  24843  ioombl1lem4  24848  icombl1  24850  icombl  24851  ioombl  24852  uniioombllem1  24868  mbfdm  24913  ismbfd  24926  mbfmax  24936  ismbf3d  24941  itg2ge0  25023  lhop2  25302  dvfsumlem2  25314  dvfsumrlim  25318  dvfsumrlim2  25319  taylfvallem1  25639  taylfval  25641  tayl0  25644  radcnvcl  25699  radcnvle  25702  psercnlem1  25707  logccv  25941  rlimcnp  26238  rlimcnp2  26239  xrlimcnp  26241  logfacbnd3  26494  chebbnd1  26743  chebbnd2  26748  dchrisumlem3  26762  log2sumbnd  26815  pntpbnd1  26857  pntibndlem2  26862  pntlemb  26868  pntleme  26879  pnt  26885  upgrfi  27841  topnfbey  29212  isblo3i  29542  xrge0infss  31460  xrdifh  31478  hashxpe  31504  elxrge02  31583  xdivpnfrp  31584  xrge0addass  31676  xrge0addgt0  31677  xrge0adddir  31678  xrge0npcan  31680  fsumrp0cl  31681  xrge0tsmsd  31694  pnfinf  31814  xrnarchi  31815  xrge0slmod  31934  unitssxrge0  32255  tpr2rico  32267  xrge0iifcnv  32288  xrge0iifiso  32290  xrge0iifhom  32292  xrge0mulc1cn  32296  pnfneige0  32306  lmxrge0  32307  esumle  32431  esumlef  32435  esumcst  32436  esumpr2  32440  esumpinfval  32446  esumpinfsum  32450  esumpcvgval  32451  hashf2  32457  esumcvg  32459  esumcvgsum  32461  voliune  32602  volfiniune  32603  ddemeas  32609  sxbrsigalem0  32645  sxbrsigalem2  32660  oms0  32671  sibfinima  32713  sitmcl  32725  probmeasb  32804  orvcgteel  32841  dstfrvclim1  32851  signsply0  32937  chtvalz  33016  hgt750lemf  33040  iooelexlt  35729  mbfposadd  36021  itg2addnclem2  36026  ftc1anclem5  36051  asindmre  36057  dvasin  36058  dvacos  36059  aks4d1p1p6  40426  dvconstbi  42379  rfcnpre3  43003  absfico  43197  xadd0ge  43312  xrgepnfd  43323  xrge0nemnfd  43324  supxrgere  43325  supxrgelem  43329  supxrge  43330  xralrple2  43346  infxr  43359  infleinflem2  43363  xrralrecnnge  43383  infxrpnf  43439  xrpnf  43479  iocopn  43512  pnfel0pnf  43520  ge0xrre  43523  ge0lere  43524  ressiooinf  43549  uzinico  43552  uzubioo  43559  fsumge0cl  43568  limcicciooub  43632  limsupre  43636  limcresiooub  43637  limcleqr  43639  limsupresre  43691  limsupresico  43695  limsuppnfdlem  43696  limsuppnflem  43705  limsupmnflem  43715  liminfresico  43766  limsup10exlem  43767  liminflelimsuplem  43770  liminflelimsupuz  43780  limsupub2  43807  liminflbuz2  43810  liminflimsupxrre  43812  xlimpnfvlem2  43832  xlimliminflimsup  43857  icccncfext  43882  iblsplit  43961  itgsubsticclem  43970  fourierdlem31  44133  fourierdlem33  44135  fourierdlem46  44147  fourierdlem47  44148  fourierdlem48  44149  fourierdlem49  44150  fourierdlem65  44166  fourierdlem73  44174  fourierdlem75  44176  fourierdlem85  44186  fourierdlem88  44189  fourierdlem95  44196  fourierdlem97  44198  fourierdlem103  44204  fourierdlem104  44205  fourierdlem107  44208  fourierdlem109  44210  fourierdlem111  44212  fourierdlem112  44213  fourierdlem113  44214  fouriersw  44226  ioorrnopnxrlem  44301  sge0val  44361  fge0iccico  44365  gsumge0cl  44366  sge0sn  44374  sge0tsms  44375  sge0cl  44376  sge0f1o  44377  sge0ge0  44379  sge0repnf  44381  sge0fsum  44382  sge0pr  44389  sge0prle  44396  sge0split  44404  sge0p1  44409  sge0iunmptlemre  44410  sge0rpcpnf  44416  sge0rernmpt  44417  sge0isum  44422  sge0ad2en  44426  sge0xaddlem1  44428  sge0xaddlem2  44429  sge0uzfsumgt  44439  sge0seq  44441  sge0reuz  44442  voliunsge0lem  44467  meage0  44470  meassre  44472  meaiuninclem  44475  omessre  44505  omeiunltfirp  44514  carageniuncllem2  44517  carageniuncl  44518  omege0  44528  hoiprodcl  44542  hoicvrrex  44551  ovnpnfelsup  44554  ovnlerp  44557  ovnf  44558  ovn0lem  44560  ovnsubaddlem1  44565  hoiprodcl3  44575  hoidmvcl  44577  sge0hsphoire  44584  hoidmv1lelem1  44586  hoidmv1lelem2  44587  hoidmv1lelem3  44588  hoidmv1le  44589  hoidmvlelem1  44590  hoidmvlelem4  44593  hoidmvlelem5  44594  ovnhoilem1  44596  volicorege0  44632  ovolval5lem1  44647  pimgtpnf2f  44700  pimiooltgt  44705  smfliminflem  44825  rrxsphere  46584  itscnhlinecirc02p  46621
  Copyright terms: Public domain W3C validator