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

Theorem pnfxr 10130
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 3810 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 df-pnf 10114 . . . . 5 +∞ = 𝒫
3 cnex 10055 . . . . . . 7 ℂ ∈ V
43uniex 6995 . . . . . 6 ℂ ∈ V
54pwex 4878 . . . . 5 𝒫 ℂ ∈ V
62, 5eqeltri 2726 . . . 4 +∞ ∈ V
76prid1 4329 . . 3 +∞ ∈ {+∞, -∞}
81, 7sselii 3633 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
9 df-xr 10116 . 2 * = (ℝ ∪ {+∞, -∞})
108, 9eleqtrri 2729 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cun 3605  𝒫 cpw 4191  {cpr 4212   cuni 4468  cc 9972  cr 9973  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-pow 4873  ax-un 6991  ax-cnex 10030
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-pw 4193  df-sn 4211  df-pr 4213  df-uni 4469  df-pnf 10114  df-xr 10116
This theorem is referenced by:  pnfex  10131  pnfnemnf  10132  xnn0xr  11406  xrltnr  11991  ltpnf  11992  mnfltpnf  11998  pnfnlt  12000  pnfge  12002  nltpnft  12033  xgepnf  12034  xrre  12038  xrre2  12039  xnegcl  12082  xaddf  12093  xaddpnf1  12095  xaddpnf2  12096  pnfaddmnf  12099  mnfaddpnf  12100  xaddass2  12118  xlt2add  12128  xsubge0  12129  xmulneg1  12137  xmulf  12140  xmulpnf1  12142  xmulpnf2  12143  xmulmnf1  12144  xmulpnf1n  12146  xlemul1a  12156  xadddilem  12162  xadddi2  12165  xrsupsslem  12175  xrinfmsslem  12176  supxrpnf  12186  supxrunb1  12187  supxrunb2  12188  supxrbnd  12196  xrinf0  12206  elicore  12264  elioc2  12274  elico2  12275  elicc2  12276  ioomax  12286  iccmax  12287  ioopos  12288  elioopnf  12305  elicopnf  12307  unirnioo  12311  xrge0neqmnf  12314  elxrge0  12319  difreicc  12342  xnn0xrge0  12363  ioopnfsup  12703  icopnfsup  12704  xrsup  12707  hashbnd  13163  hashnnn0genn0  13171  hashxrcl  13186  hashdomi  13207  sgnpnf  13877  rexico  14137  limsupgre  14256  rlim3  14273  fprodge0  14768  fprodge1  14770  pcxcl  15612  pc2dvds  15630  pcadd  15640  ramxrcl  15768  ramubcl  15769  xrsnsgrp  19830  xrsdsreclblem  19840  rge0srg  19865  leordtvallem1  21062  leordtval2  21064  lecldbas  21071  pnfnei  21072  mnfnei  21073  xblpnfps  22247  xblpnf  22248  xblss2ps  22253  blssec  22287  blpnfctr  22288  nmoix  22580  icopnfcld  22618  iocmnfcld  22619  xrtgioo  22656  reconnlem1  22676  xrge0tsms  22684  metdstri  22701  iccpnfcnv  22790  ovolf  23296  ovolicopnf  23338  ovolre  23339  volsup  23370  ioombl1lem4  23375  icombl1  23377  icombl  23378  ioombl  23379  uniioombllem1  23395  mbfdm  23440  ismbfd  23452  mbfmax  23461  ismbf3d  23466  itg2ge0  23547  lhop2  23823  dvfsumlem2  23835  dvfsumrlim  23839  dvfsumrlim2  23840  taylfvallem1  24156  taylfval  24158  tayl0  24161  radcnvcl  24216  radcnvle  24219  psercnlem1  24224  logccv  24454  rlimcnp  24737  rlimcnp2  24738  xrlimcnp  24740  logfacbnd3  24993  chebbnd1  25206  chebbnd2  25211  dchrisumlem3  25225  log2sumbnd  25278  pntpbnd1  25320  pntibndlem2  25325  pntlemb  25331  pntleme  25342  pnt  25348  upgrfi  26031  topnfbey  27455  isblo3i  27784  xrge0infss  29653  dfrp2  29660  xrdifh  29670  elxrge02  29768  xdivpnfrp  29769  xrge0addass  29818  xrge0addgt0  29819  xrge0adddir  29820  xrge0npcan  29822  fsumrp0cl  29823  pnfinf  29865  xrnarchi  29866  xrge0tsmsd  29913  xrge0slmod  29972  unitssxrge0  30074  tpr2rico  30086  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  xrge0mulc1cn  30115  pnfneige0  30125  lmxrge0  30126  esumle  30248  esumlef  30252  esumcst  30253  esumpr2  30257  esumpinfval  30263  esumpinfsum  30267  esumpcvgval  30268  hashf2  30274  esumcvg  30276  esumcvgsum  30278  voliune  30420  volfiniune  30421  ddemeas  30427  sxbrsigalem0  30461  sxbrsigalem2  30476  oms0  30487  sibfinima  30529  sitmcl  30541  probmeasb  30620  orvcgteel  30657  dstfrvclim1  30667  signsply0  30756  chtvalz  30835  hgt750lemf  30859  iooelexlt  33340  mbfposadd  33587  itg2addnclem2  33592  ftc1anclem5  33619  asindmre  33625  dvasin  33626  dvacos  33627  dvconstbi  38850  rfcnpre3  39506  absfico  39724  xadd0ge  39849  xrgepnfd  39860  xrge0nemnfd  39861  supxrgere  39862  supxrgelem  39866  supxrge  39867  xralrple2  39883  infxr  39896  infleinflem2  39900  xrralrecnnge  39926  infxrpnf  39987  xrpnf  40029  iocopn  40064  pnfel0pnf  40072  ge0nemnf2  40073  ge0xrre  40076  ge0lere  40077  ressiooinf  40102  uzinico  40105  uzubioo  40112  fsumge0cl  40123  limcicciooub  40187  limsupre  40191  limcresiooub  40192  limcleqr  40194  limsupresre  40246  limsupresico  40250  limsuppnfdlem  40251  limsuppnflem  40260  limsupmnflem  40270  liminfresico  40321  limsup10exlem  40322  liminflelimsuplem  40325  liminflelimsupuz  40335  xlimpnfvlem2  40381  icccncfext  40418  iblsplit  40500  itgsubsticclem  40509  fourierdlem31  40673  fourierdlem33  40675  fourierdlem46  40687  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem65  40706  fourierdlem73  40714  fourierdlem75  40716  fourierdlem85  40726  fourierdlem88  40729  fourierdlem95  40736  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem109  40750  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fouriersw  40766  ioorrnopnxrlem  40844  sge0val  40901  fge0iccico  40905  gsumge0cl  40906  sge0sn  40914  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0ge0  40919  sge0repnf  40921  sge0fsum  40922  sge0pr  40929  sge0prle  40936  sge0split  40944  sge0p1  40949  sge0iunmptlemre  40950  sge0rpcpnf  40956  sge0rernmpt  40957  sge0isum  40962  sge0ad2en  40966  sge0xaddlem1  40968  sge0xaddlem2  40969  sge0uzfsumgt  40979  sge0seq  40981  sge0reuz  40982  voliunsge0lem  41007  meage0  41010  meassre  41012  meaiuninclem  41015  omessre  41045  omeiunltfirp  41054  carageniuncllem2  41057  carageniuncl  41058  omege0  41068  hoiprodcl  41082  hoicvrrex  41091  ovnpnfelsup  41094  ovnlerp  41097  ovnf  41098  ovn0lem  41100  ovnsubaddlem1  41105  hoiprodcl3  41115  hoidmvcl  41117  sge0hsphoire  41124  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem4  41133  hoidmvlelem5  41134  ovnhoilem1  41136  volicorege0  41172  ovolval5lem1  41187  pimgtpnf2  41238  pimiooltgt  41242  smfliminflem  41357
  Copyright terms: Public domain W3C validator