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 4148 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 pnfex 10683 . . . 4 +∞ ∈ V
32prid1 4692 . . 3 +∞ ∈ {+∞, -∞}
41, 3sselii 3963 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
5 df-xr 10668 . 2 * = (ℝ ∪ {+∞, -∞})
64, 5eleqtrri 2912 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  cun 3933  {cpr 4561  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 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-pow 5258  ax-un 7450  ax-cnex 10582
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-v 3497  df-un 3940  df-in 3942  df-ss 3951  df-pw 4539  df-sn 4560  df-pr 4562  df-uni 4833  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  20511  xrsdsreclblem  20521  rge0srg  20546  leordtvallem1  21748  leordtval2  21750  lecldbas  21757  pnfnei  21758  mnfnei  21759  xblpnfps  22934  xblpnf  22935  xblss2ps  22940  blssec  22974  blpnfctr  22975  nmoix  23267  icopnfcld  23305  iocmnfcld  23306  xrtgioo  23343  reconnlem1  23363  xrge0tsms  23371  metdstri  23388  iccpnfcnv  23477  ovolf  24012  ovolicopnf  24054  ovolre  24055  volsup  24086  ioombl1lem4  24091  icombl1  24093  icombl  24094  ioombl  24095  uniioombllem1  24111  mbfdm  24156  ismbfd  24169  mbfmax  24179  ismbf3d  24184  itg2ge0  24265  lhop2  24541  dvfsumlem2  24553  dvfsumrlim  24557  dvfsumrlim2  24558  taylfvallem1  24874  taylfval  24876  tayl0  24879  radcnvcl  24934  radcnvle  24937  psercnlem1  24942  logccv  25173  rlimcnp  25471  rlimcnp2  25472  xrlimcnp  25474  logfacbnd3  25727  chebbnd1  25976  chebbnd2  25981  dchrisumlem3  25995  log2sumbnd  26048  pntpbnd1  26090  pntibndlem2  26095  pntlemb  26101  pntleme  26112  pnt  26118  upgrfi  26804  topnfbey  28176  isblo3i  28506  xrge0infss  30411  dfrp2  30418  xrdifh  30430  hashxpe  30456  elxrge02  30536  xdivpnfrp  30537  xrge0addass  30605  xrge0addgt0  30606  xrge0adddir  30607  xrge0npcan  30609  fsumrp0cl  30610  xrge0tsmsd  30620  pnfinf  30740  xrnarchi  30741  xrge0slmod  30845  unitssxrge0  31043  tpr2rico  31055  xrge0iifcnv  31076  xrge0iifiso  31078  xrge0iifhom  31080  xrge0mulc1cn  31084  pnfneige0  31094  lmxrge0  31095  esumle  31217  esumlef  31221  esumcst  31222  esumpr2  31226  esumpinfval  31232  esumpinfsum  31236  esumpcvgval  31237  hashf2  31243  esumcvg  31245  esumcvgsum  31247  voliune  31388  volfiniune  31389  ddemeas  31395  sxbrsigalem0  31429  sxbrsigalem2  31444  oms0  31455  sibfinima  31497  sitmcl  31509  probmeasb  31588  orvcgteel  31625  dstfrvclim1  31635  signsply0  31721  chtvalz  31800  hgt750lemf  31824  iooelexlt  34526  mbfposadd  34821  itg2addnclem2  34826  ftc1anclem5  34853  asindmre  34859  dvasin  34860  dvacos  34861  dvconstbi  40546  rfcnpre3  41170  absfico  41361  xadd0ge  41468  xrgepnfd  41479  xrge0nemnfd  41480  supxrgere  41481  supxrgelem  41485  supxrge  41486  xralrple2  41502  infxr  41515  infleinflem2  41519  xrralrecnnge  41542  infxrpnf  41601  xrpnf  41642  iocopn  41676  pnfel0pnf  41684  ge0xrre  41687  ge0lere  41688  ressiooinf  41713  uzinico  41716  uzubioo  41723  fsumge0cl  41734  limcicciooub  41798  limsupre  41802  limcresiooub  41803  limcleqr  41805  limsupresre  41857  limsupresico  41861  limsuppnfdlem  41862  limsuppnflem  41871  limsupmnflem  41881  liminfresico  41932  limsup10exlem  41933  liminflelimsuplem  41936  liminflelimsupuz  41946  limsupub2  41973  liminflbuz2  41976  liminflimsupxrre  41978  xlimpnfvlem2  41998  xlimliminflimsup  42023  icccncfext  42050  iblsplit  42131  itgsubsticclem  42140  fourierdlem31  42304  fourierdlem33  42306  fourierdlem46  42318  fourierdlem47  42319  fourierdlem48  42320  fourierdlem49  42321  fourierdlem65  42337  fourierdlem73  42345  fourierdlem75  42347  fourierdlem85  42357  fourierdlem88  42360  fourierdlem95  42367  fourierdlem97  42369  fourierdlem103  42375  fourierdlem104  42376  fourierdlem107  42379  fourierdlem109  42381  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fouriersw  42397  ioorrnopnxrlem  42472  sge0val  42529  fge0iccico  42533  gsumge0cl  42534  sge0sn  42542  sge0tsms  42543  sge0cl  42544  sge0f1o  42545  sge0ge0  42547  sge0repnf  42549  sge0fsum  42550  sge0pr  42557  sge0prle  42564  sge0split  42572  sge0p1  42577  sge0iunmptlemre  42578  sge0rpcpnf  42584  sge0rernmpt  42585  sge0isum  42590  sge0ad2en  42594  sge0xaddlem1  42596  sge0xaddlem2  42597  sge0uzfsumgt  42607  sge0seq  42609  sge0reuz  42610  voliunsge0lem  42635  meage0  42638  meassre  42640  meaiuninclem  42643  omessre  42673  omeiunltfirp  42682  carageniuncllem2  42685  carageniuncl  42686  omege0  42696  hoiprodcl  42710  hoicvrrex  42719  ovnpnfelsup  42722  ovnlerp  42725  ovnf  42726  ovn0lem  42728  ovnsubaddlem1  42733  hoiprodcl3  42743  hoidmvcl  42745  sge0hsphoire  42752  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1lelem3  42756  hoidmv1le  42757  hoidmvlelem1  42758  hoidmvlelem4  42761  hoidmvlelem5  42762  ovnhoilem1  42764  volicorege0  42800  ovolval5lem1  42815  pimgtpnf2  42866  pimiooltgt  42870  smfliminflem  42985  rrxsphere  44633  itscnhlinecirc02p  44670
  Copyright terms: Public domain W3C validator