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

Theorem pnfxr 10387
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 3987 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 df-pnf 10371 . . . . 5 +∞ = 𝒫
3 cnex 10312 . . . . . . 7 ℂ ∈ V
43uniex 7193 . . . . . 6 ℂ ∈ V
54pwex 5063 . . . . 5 𝒫 ℂ ∈ V
62, 5eqeltri 2892 . . . 4 +∞ ∈ V
76prid1 4499 . . 3 +∞ ∈ {+∞, -∞}
81, 7sselii 3806 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
9 df-xr 10373 . 2 * = (ℝ ∪ {+∞, -∞})
108, 9eleqtrri 2895 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  Vcvv 3402  cun 3778  𝒫 cpw 4362  {cpr 4383   cuni 4641  cc 10229  cr 10230  +∞cpnf 10366  -∞cmnf 10367  *cxr 10368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-pow 5048  ax-un 7189  ax-cnex 10287
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-v 3404  df-un 3785  df-in 3787  df-ss 3794  df-pw 4364  df-sn 4382  df-pr 4384  df-uni 4642  df-pnf 10371  df-xr 10373
This theorem is referenced by:  pnfex  10388  pnfnemnf  10389  xnn0xr  11654  xrltnr  12189  ltpnf  12190  mnfltpnf  12196  pnfnlt  12198  pnfge  12200  nltpnft  12233  xgepnf  12234  xrre  12238  xrre2  12239  xnegcl  12282  xaddf  12293  xaddpnf1  12295  xaddpnf2  12296  pnfaddmnf  12299  mnfaddpnf  12300  xaddass2  12318  xlt2add  12328  xsubge0  12329  xmulneg1  12337  xmulf  12340  xmulpnf1  12342  xmulpnf2  12343  xmulmnf1  12344  xmulpnf1n  12346  xlemul1a  12356  xadddilem  12362  xadddi2  12365  xrsupsslem  12375  xrinfmsslem  12376  supxrpnf  12386  supxrunb1  12387  supxrunb2  12388  supxrbnd  12396  xrinf0  12406  elicore  12464  elioc2  12474  elico2  12475  elicc2  12476  ioomax  12486  iccmax  12487  ioopos  12488  elioopnf  12506  elicopnf  12508  unirnioo  12512  xrge0neqmnf  12515  xrge0neqmnfOLD  12516  elxrge0  12521  difreicc  12547  xnn0xrge0  12568  ioopnfsup  12907  icopnfsup  12908  xrsup  12911  hashbnd  13363  hashnnn0genn0  13371  hashxrcl  13386  hashdomi  13407  sgnpnf  14076  rexico  14336  limsupgre  14455  rlim3  14472  fprodge0  14964  fprodge1  14966  pcxcl  15802  pc2dvds  15820  pcadd  15830  ramxrcl  15958  ramubcl  15959  xrsnsgrp  20010  xrsdsreclblem  20020  rge0srg  20045  leordtvallem1  21249  leordtval2  21251  lecldbas  21258  pnfnei  21259  mnfnei  21260  xblpnfps  22434  xblpnf  22435  xblss2ps  22440  blssec  22474  blpnfctr  22475  nmoix  22767  icopnfcld  22805  iocmnfcld  22806  xrtgioo  22843  reconnlem1  22863  xrge0tsms  22871  metdstri  22888  iccpnfcnv  22977  ovolf  23486  ovolicopnf  23528  ovolre  23529  volsup  23560  ioombl1lem4  23565  icombl1  23567  icombl  23568  ioombl  23569  uniioombllem1  23585  mbfdm  23630  ismbfd  23643  mbfmax  23653  ismbf3d  23658  itg2ge0  23739  lhop2  24015  dvfsumlem2  24027  dvfsumrlim  24031  dvfsumrlim2  24032  taylfvallem1  24348  taylfval  24350  tayl0  24353  radcnvcl  24408  radcnvle  24411  psercnlem1  24416  logccv  24646  rlimcnp  24929  rlimcnp2  24930  xrlimcnp  24932  logfacbnd3  25185  chebbnd1  25398  chebbnd2  25403  dchrisumlem3  25417  log2sumbnd  25470  pntpbnd1  25512  pntibndlem2  25517  pntlemb  25523  pntleme  25534  pnt  25540  upgrfi  26223  topnfbey  27679  isblo3i  28007  xrge0infss  29875  dfrp2  29882  xrdifh  29892  elxrge02  29988  xdivpnfrp  29989  xrge0addass  30038  xrge0addgt0  30039  xrge0adddir  30040  xrge0npcan  30042  fsumrp0cl  30043  pnfinf  30085  xrnarchi  30086  xrge0tsmsd  30133  xrge0slmod  30192  unitssxrge0  30294  tpr2rico  30306  xrge0iifcnv  30327  xrge0iifiso  30329  xrge0iifhom  30331  xrge0mulc1cn  30335  pnfneige0  30345  lmxrge0  30346  esumle  30468  esumlef  30472  esumcst  30473  esumpr2  30477  esumpinfval  30483  esumpinfsum  30487  esumpcvgval  30488  hashf2  30494  esumcvg  30496  esumcvgsum  30498  voliune  30640  volfiniune  30641  ddemeas  30647  sxbrsigalem0  30681  sxbrsigalem2  30696  oms0  30707  sibfinima  30749  sitmcl  30761  probmeasb  30840  orvcgteel  30877  dstfrvclim1  30887  signsply0  30976  chtvalz  31055  hgt750lemf  31079  iooelexlt  33545  mbfposadd  33788  itg2addnclem2  33793  ftc1anclem5  33820  asindmre  33826  dvasin  33827  dvacos  33828  dvconstbi  39051  rfcnpre3  39704  absfico  39915  xadd0ge  40034  xrgepnfd  40045  xrge0nemnfd  40046  supxrgere  40047  supxrgelem  40051  supxrge  40052  xralrple2  40068  infxr  40081  infleinflem2  40085  xrralrecnnge  40110  infxrpnf  40171  xrpnf  40213  iocopn  40245  pnfel0pnf  40253  ge0xrre  40256  ge0lere  40257  ressiooinf  40282  uzinico  40285  uzubioo  40292  fsumge0cl  40303  limcicciooub  40367  limsupre  40371  limcresiooub  40372  limcleqr  40374  limsupresre  40426  limsupresico  40430  limsuppnfdlem  40431  limsuppnflem  40440  limsupmnflem  40450  liminfresico  40501  limsup10exlem  40502  liminflelimsuplem  40505  liminflelimsupuz  40515  xlimpnfvlem2  40561  icccncfext  40598  iblsplit  40679  itgsubsticclem  40688  fourierdlem31  40852  fourierdlem33  40854  fourierdlem46  40866  fourierdlem47  40867  fourierdlem48  40868  fourierdlem49  40869  fourierdlem65  40885  fourierdlem73  40893  fourierdlem75  40895  fourierdlem85  40905  fourierdlem88  40908  fourierdlem95  40915  fourierdlem97  40917  fourierdlem103  40923  fourierdlem104  40924  fourierdlem107  40927  fourierdlem109  40929  fourierdlem111  40931  fourierdlem112  40932  fourierdlem113  40933  fouriersw  40945  ioorrnopnxrlem  41023  sge0val  41080  fge0iccico  41084  gsumge0cl  41085  sge0sn  41093  sge0tsms  41094  sge0cl  41095  sge0f1o  41096  sge0ge0  41098  sge0repnf  41100  sge0fsum  41101  sge0pr  41108  sge0prle  41115  sge0split  41123  sge0p1  41128  sge0iunmptlemre  41129  sge0rpcpnf  41135  sge0rernmpt  41136  sge0isum  41141  sge0ad2en  41145  sge0xaddlem1  41147  sge0xaddlem2  41148  sge0uzfsumgt  41158  sge0seq  41160  sge0reuz  41161  voliunsge0lem  41186  meage0  41189  meassre  41191  meaiuninclem  41194  omessre  41224  omeiunltfirp  41233  carageniuncllem2  41236  carageniuncl  41237  omege0  41247  hoiprodcl  41261  hoicvrrex  41270  ovnpnfelsup  41273  ovnlerp  41276  ovnf  41277  ovn0lem  41279  ovnsubaddlem1  41284  hoiprodcl3  41294  hoidmvcl  41296  sge0hsphoire  41303  hoidmv1lelem1  41305  hoidmv1lelem2  41306  hoidmv1lelem3  41307  hoidmv1le  41308  hoidmvlelem1  41309  hoidmvlelem4  41312  hoidmvlelem5  41313  ovnhoilem1  41315  volicorege0  41351  ovolval5lem1  41366  pimgtpnf2  41417  pimiooltgt  41421  smfliminflem  41536
  Copyright terms: Public domain W3C validator