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

Theorem pnfxr 11778
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 3735 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 df-pnf 9929 . . . . 5 +∞ = 𝒫
3 cnex 9870 . . . . . . 7 ℂ ∈ V
43uniex 6825 . . . . . 6 ℂ ∈ V
54pwex 4766 . . . . 5 𝒫 ℂ ∈ V
62, 5eqeltri 2680 . . . 4 +∞ ∈ V
76prid1 4237 . . 3 +∞ ∈ {+∞, -∞}
81, 7sselii 3561 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
9 df-xr 9931 . 2 * = (ℝ ∪ {+∞, -∞})
108, 9eleqtrri 2683 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3169  cun 3534  𝒫 cpw 4104  {cpr 4123   cuni 4363  cc 9787  cr 9788  +∞cpnf 9924  -∞cmnf 9925  *cxr 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-pow 4761  ax-un 6821  ax-cnex 9845
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-v 3171  df-un 3541  df-in 3543  df-ss 3550  df-pw 4106  df-sn 4122  df-pr 4124  df-uni 4364  df-pnf 9929  df-xr 9931
This theorem is referenced by:  pnfex  11779  pnfnemnf  11783  xrltnr  11787  ltpnf  11788  mnfltpnf  11794  pnfnlt  11796  pnfge  11798  nltpnft  11827  xrre  11830  xrre2  11831  xnegcl  11874  xaddf  11885  xaddpnf1  11887  xaddpnf2  11888  pnfaddmnf  11891  mnfaddpnf  11892  xaddass2  11906  xlt2add  11916  xsubge0  11917  xmulneg1  11925  xmulf  11928  xmulpnf1  11930  xmulpnf2  11931  xmulmnf1  11932  xmulpnf1n  11934  xlemul1a  11944  xadddilem  11950  xadddi2  11953  xrsupsslem  11962  xrinfmsslem  11963  supxrpnf  11973  supxrunb1  11974  supxrunb2  11975  supxrbnd  11983  xrinf0  11992  elicore  12050  elioc2  12060  elico2  12061  elicc2  12062  ioomax  12072  iccmax  12073  ioopos  12074  elioopnf  12091  elicopnf  12093  unirnioo  12097  xrge0neqmnf  12100  elxrge0  12105  difreicc  12128  ioopnfsup  12477  icopnfsup  12478  xrsup  12481  hashbnd  12937  hashnnn0genn0  12942  hashxrcl  12959  hashdomi  12979  sgnpnf  13624  rexico  13884  limsupgre  14003  rlim3  14020  fprodge0  14506  fprodge1  14508  pcxcl  15346  pc2dvds  15364  pcadd  15374  ramxrcl  15502  ramubcl  15503  xrsnsgrp  19544  xrsdsreclblem  19554  rge0srg  19579  leordtvallem1  20763  leordtval2  20765  lecldbas  20772  pnfnei  20773  mnfnei  20774  xblpnfps  21948  xblpnf  21949  xblss2ps  21954  blssec  21988  blpnfctr  21989  nmoix  22272  icopnfcld  22310  iocmnfcld  22311  xrtgioo  22346  reconnlem1  22366  xrge0tsms  22374  metdstri  22390  iccpnfcnv  22479  ovolf  22971  ovolicopnf  23013  ovolre  23014  volsup  23045  ioombl1lem4  23050  icombl1  23052  icombl  23053  ioombl  23054  uniioombllem1  23069  mbfdm  23115  ismbfd  23127  mbfmax  23136  ismbf3d  23141  itg2ge0  23222  lhop2  23496  dvfsumlem2  23508  dvfsumrlim  23512  dvfsumrlim2  23513  taylfvallem1  23829  taylfval  23831  tayl0  23834  radcnvcl  23889  radcnvle  23892  psercnlem1  23897  logccv  24123  rlimcnp  24406  rlimcnp2  24407  xrlimcnp  24409  logfacbnd3  24662  chebbnd1  24875  chebbnd2  24880  dchrisumlem3  24894  log2sumbnd  24947  pntpbnd1  24989  pntibndlem2  24994  pntlemb  25000  pntleme  25011  pnt  25017  umgrafi  25614  sizeusglecusg  25777  topnfbey  26480  isblo3i  26843  xgepnf  28707  xrge0infss  28718  dfrp2  28725  xrdifh  28735  elxrge02  28774  xdivpnfrp  28775  xrge0addass  28824  xrge0addgt0  28825  xrge0adddir  28826  xrge0npcan  28828  fsumrp0cl  28829  pnfinf  28871  xrnarchi  28872  xrge0tsmsd  28919  xrge0slmod  28978  unitssxrge0  29077  tpr2rico  29089  xrge0iifcnv  29110  xrge0iifiso  29112  xrge0iifhom  29114  xrge0mulc1cn  29118  pnfneige0  29128  lmxrge0  29129  esumle  29250  esumlef  29254  esumcst  29255  esumpr2  29259  esumpinfval  29265  esumpinfsum  29269  esumpcvgval  29270  hashf2  29276  esumcvg  29278  esumcvgsum  29280  voliune  29422  volfiniune  29423  ddemeas  29429  sxbrsigalem0  29463  sxbrsigalem2  29478  oms0  29489  sibfinima  29531  sitmcl  29543  probmeasb  29622  orvcgteel  29659  dstfrvclim1  29669  signsply0  29757  iooelexlt  32186  mbfposadd  32427  itg2addnclem2  32432  ftc1anclem5  32459  asindmre  32465  dvasin  32466  dvacos  32467  dvconstbi  37355  rfcnpre3  38015  absfico  38205  xadd0ge  38278  xrgepnfd  38289  xrge0nemnfd  38290  supxrgere  38291  supxrgelem  38295  supxrge  38296  xralrple2  38312  infxr  38325  infleinflem2  38329  xrralrecnnge  38355  iocopn  38394  pnfel0pnf  38402  ge0nemnf2  38403  ge0xrre  38406  ge0lere  38407  ressiooinf  38432  fsumge0cl  38441  limcicciooub  38505  limsupre  38509  limcresiooub  38510  limcleqr  38512  icccncfext  38574  iblsplit  38659  itgsubsticclem  38668  fourierdlem31  38832  fourierdlem33  38834  fourierdlem46  38846  fourierdlem47  38847  fourierdlem48  38848  fourierdlem49  38849  fourierdlem65  38865  fourierdlem73  38873  fourierdlem75  38875  fourierdlem85  38885  fourierdlem88  38888  fourierdlem95  38895  fourierdlem97  38897  fourierdlem103  38903  fourierdlem104  38904  fourierdlem107  38907  fourierdlem109  38909  fourierdlem111  38911  fourierdlem112  38912  fourierdlem113  38913  fouriersw  38925  ioorrnopnxrlem  39003  sge0val  39060  fge0iccico  39064  gsumge0cl  39065  sge0sn  39073  sge0tsms  39074  sge0cl  39075  sge0f1o  39076  sge0ge0  39078  sge0repnf  39080  sge0fsum  39081  sge0pr  39088  sge0prle  39095  sge0split  39103  sge0p1  39108  sge0iunmptlemre  39109  sge0rpcpnf  39115  sge0rernmpt  39116  sge0isum  39121  sge0ad2en  39125  sge0xaddlem1  39127  sge0xaddlem2  39128  sge0uzfsumgt  39138  sge0seq  39140  sge0reuz  39141  voliunsge0lem  39166  meage0  39169  meassre  39171  meaiuninclem  39174  omessre  39201  omeiunltfirp  39210  carageniuncllem2  39213  carageniuncl  39214  omege0  39224  hoiprodcl  39238  hoicvrrex  39247  ovnpnfelsup  39250  ovnlerp  39253  ovnf  39254  ovn0lem  39256  ovnsubaddlem1  39261  hoiprodcl3  39271  hoidmvcl  39273  sge0hsphoire  39280  hoidmv1lelem1  39282  hoidmv1lelem2  39283  hoidmv1lelem3  39284  hoidmv1le  39285  hoidmvlelem1  39286  hoidmvlelem4  39289  hoidmvlelem5  39290  ovnhoilem1  39292  volicorege0  39328  ovolval5lem1  39343  pimgtpnf2  39395  pimiooltgt  39399  xnn0xr  40201  xnn0xrge0  40202  upgrfi  40316
  Copyright terms: Public domain W3C validator