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  20756  xrsdsreclblem  20766  rge0srg  20791  leordtvallem1  22483  leordtval2  22485  lecldbas  22492  pnfnei  22493  mnfnei  22494  xblpnfps  23670  xblpnf  23671  xblss2ps  23676  blssec  23710  blpnfctr  23711  nmoix  24015  icopnfcld  24053  iocmnfcld  24054  xrtgioo  24091  reconnlem1  24111  xrge0tsms  24119  metdstri  24136  iccpnfcnv  24229  ovolf  24768  ovolicopnf  24810  ovolre  24811  volsup  24842  ioombl1lem4  24847  icombl1  24849  icombl  24850  ioombl  24851  uniioombllem1  24867  mbfdm  24912  ismbfd  24925  mbfmax  24935  ismbf3d  24940  itg2ge0  25022  lhop2  25301  dvfsumlem2  25313  dvfsumrlim  25317  dvfsumrlim2  25318  taylfvallem1  25638  taylfval  25640  tayl0  25643  radcnvcl  25698  radcnvle  25701  psercnlem1  25706  logccv  25940  rlimcnp  26237  rlimcnp2  26238  xrlimcnp  26240  logfacbnd3  26493  chebbnd1  26742  chebbnd2  26747  dchrisumlem3  26761  log2sumbnd  26814  pntpbnd1  26856  pntibndlem2  26861  pntlemb  26867  pntleme  26878  pnt  26884  upgrfi  27828  topnfbey  29199  isblo3i  29529  xrge0infss  31447  xrdifh  31465  hashxpe  31491  elxrge02  31570  xdivpnfrp  31571  xrge0addass  31663  xrge0addgt0  31664  xrge0adddir  31665  xrge0npcan  31667  fsumrp0cl  31668  xrge0tsmsd  31681  pnfinf  31801  xrnarchi  31802  xrge0slmod  31921  unitssxrge0  32242  tpr2rico  32254  xrge0iifcnv  32275  xrge0iifiso  32277  xrge0iifhom  32279  xrge0mulc1cn  32283  pnfneige0  32293  lmxrge0  32294  esumle  32418  esumlef  32422  esumcst  32423  esumpr2  32427  esumpinfval  32433  esumpinfsum  32437  esumpcvgval  32438  hashf2  32444  esumcvg  32446  esumcvgsum  32448  voliune  32589  volfiniune  32590  ddemeas  32596  sxbrsigalem0  32632  sxbrsigalem2  32647  oms0  32658  sibfinima  32700  sitmcl  32712  probmeasb  32791  orvcgteel  32828  dstfrvclim1  32838  signsply0  32924  chtvalz  33003  hgt750lemf  33027  iooelexlt  35719  mbfposadd  36011  itg2addnclem2  36016  ftc1anclem5  36041  asindmre  36047  dvasin  36048  dvacos  36049  aks4d1p1p6  40416  dvconstbi  42347  rfcnpre3  42971  absfico  43165  xadd0ge  43280  xrgepnfd  43291  xrge0nemnfd  43292  supxrgere  43293  supxrgelem  43297  supxrge  43298  xralrple2  43314  infxr  43327  infleinflem2  43331  xrralrecnnge  43351  infxrpnf  43407  xrpnf  43447  iocopn  43480  pnfel0pnf  43488  ge0xrre  43491  ge0lere  43492  ressiooinf  43517  uzinico  43520  uzubioo  43527  fsumge0cl  43536  limcicciooub  43600  limsupre  43604  limcresiooub  43605  limcleqr  43607  limsupresre  43659  limsupresico  43663  limsuppnfdlem  43664  limsuppnflem  43673  limsupmnflem  43683  liminfresico  43734  limsup10exlem  43735  liminflelimsuplem  43738  liminflelimsupuz  43748  limsupub2  43775  liminflbuz2  43778  liminflimsupxrre  43780  xlimpnfvlem2  43800  xlimliminflimsup  43825  icccncfext  43850  iblsplit  43929  itgsubsticclem  43938  fourierdlem31  44101  fourierdlem33  44103  fourierdlem46  44115  fourierdlem47  44116  fourierdlem48  44117  fourierdlem49  44118  fourierdlem65  44134  fourierdlem73  44142  fourierdlem75  44144  fourierdlem85  44154  fourierdlem88  44157  fourierdlem95  44164  fourierdlem97  44166  fourierdlem103  44172  fourierdlem104  44173  fourierdlem107  44176  fourierdlem109  44178  fourierdlem111  44180  fourierdlem112  44181  fourierdlem113  44182  fouriersw  44194  ioorrnopnxrlem  44269  sge0val  44329  fge0iccico  44333  gsumge0cl  44334  sge0sn  44342  sge0tsms  44343  sge0cl  44344  sge0f1o  44345  sge0ge0  44347  sge0repnf  44349  sge0fsum  44350  sge0pr  44357  sge0prle  44364  sge0split  44372  sge0p1  44377  sge0iunmptlemre  44378  sge0rpcpnf  44384  sge0rernmpt  44385  sge0isum  44390  sge0ad2en  44394  sge0xaddlem1  44396  sge0xaddlem2  44397  sge0uzfsumgt  44407  sge0seq  44409  sge0reuz  44410  voliunsge0lem  44435  meage0  44438  meassre  44440  meaiuninclem  44443  omessre  44473  omeiunltfirp  44482  carageniuncllem2  44485  carageniuncl  44486  omege0  44496  hoiprodcl  44510  hoicvrrex  44519  ovnpnfelsup  44522  ovnlerp  44525  ovnf  44526  ovn0lem  44528  ovnsubaddlem1  44533  hoiprodcl3  44543  hoidmvcl  44545  sge0hsphoire  44552  hoidmv1lelem1  44554  hoidmv1lelem2  44555  hoidmv1lelem3  44556  hoidmv1le  44557  hoidmvlelem1  44558  hoidmvlelem4  44561  hoidmvlelem5  44562  ovnhoilem1  44564  volicorege0  44600  ovolval5lem1  44615  pimgtpnf2f  44668  pimiooltgt  44673  smfliminflem  44793  rrxsphere  46552  itscnhlinecirc02p  46589
  Copyright terms: Public domain W3C validator