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

Theorem pnfxr 11412
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  |- +oo  e.  RR*

Proof of Theorem pnfxr
StepHypRef Expression
1 ssun2 3636 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9676 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9619 . . . . . . 7  |-  CC  e.  _V
43uniex 6601 . . . . . 6  |-  U. CC  e.  _V
54pwex 4608 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2513 . . . 4  |- +oo  e.  _V
76prid1 4111 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3467 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9678 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2516 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1870   _Vcvv 3087    u. cun 3440   ~Pcpw 3985   {cpr 4004   U.cuni 4222   CCcc 9536   RRcr 9537   +oocpnf 9671   -oocmnf 9672   RR*cxr 9673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-pow 4603  ax-un 6597  ax-cnex 9594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-v 3089  df-un 3447  df-in 3449  df-ss 3456  df-pw 3987  df-sn 4003  df-pr 4005  df-uni 4223  df-pnf 9676  df-xr 9678
This theorem is referenced by:  pnfex  11413  pnfnemnf  11417  xrltnr  11421  ltpnf  11422  mnfltpnf  11428  pnfnlt  11430  pnfge  11432  nltpnft  11461  xrre  11464  xrre2  11465  xnegcl  11506  xaddf  11517  xaddpnf1  11519  xaddpnf2  11520  pnfaddmnf  11523  mnfaddpnf  11524  xaddass2  11536  xlt2add  11546  xsubge0  11547  xmulneg1  11555  xmulf  11558  xmulpnf1  11560  xmulpnf2  11561  xmulmnf1  11562  xmulpnf1n  11564  xlemul1a  11574  xadddilem  11580  xadddi2  11583  xrsupsslem  11592  xrinfmsslem  11593  supxrpnf  11604  supxrunb1  11605  supxrunb2  11606  supxrbnd  11614  xrinf0  11623  xrinfm0OLD  11627  elicore  11687  elioc2  11697  elico2  11698  elicc2  11699  ioomax  11709  iccmax  11710  ioopos  11711  elioopnf  11728  elicopnf  11730  unirnioo  11734  elxrge0  11739  difreicc  11762  ioopnfsup  12088  icopnfsup  12089  xrsup  12092  hashbnd  12518  hashnnn0genn0  12523  hashxrcl  12536  hashdomi  12556  sgnpnf  13135  rexico  13395  limsupgre  13520  limsupgreOLD  13521  rlim3  13540  fprodge0  14025  fprodge1  14027  pcxcl  14773  pc2dvds  14791  pcadd  14797  ramxrcl  14938  ramubcl  14939  xrsnsgrp  18939  xrsdsreclblem  18949  rge0srg  18972  leordtvallem1  20157  leordtval2  20159  lecldbas  20166  pnfnei  20167  mnfnei  20168  xblpnfps  21341  xblpnf  21342  xblss2ps  21347  blssec  21381  blpnfctr  21382  nmoix  21661  icopnfcld  21699  iocmnfcld  21700  xrtgioo  21735  reconnlem1  21755  xrge0tsms  21763  metdstri  21779  iccpnfcnv  21868  ovolf  22313  ovolicopnf  22355  ovolre  22356  volsup  22386  ioombl1lem4  22391  icombl1  22393  icombl  22394  ioombl  22395  uniioombllem1  22415  mbfdm  22461  ismbfd  22473  mbfmax  22482  ismbf3d  22487  itg2ge0  22570  lhop2  22844  dvfsumlem2  22856  dvfsumrlim  22860  dvfsumrlim2  22861  taylfvallem1  23177  taylfval  23179  tayl0  23182  radcnvcl  23237  radcnvle  23240  psercnlem1  23245  logccv  23473  rlimcnp  23756  rlimcnp2  23757  xrlimcnp  23759  logfacbnd3  24014  chebbnd1  24173  chebbnd2  24178  dchrisumlem3  24192  log2sumbnd  24245  pntpbnd1  24287  pntibndlem2  24292  pntlemb  24298  pntleme  24309  pnt  24315  umgrafi  24895  sizeusglecusg  25059  topnfbey  25751  isblo3i  26287  xgepnf  28170  xrge0infss  28181  dfrp2  28188  xrdifh  28198  elxrge02  28239  xdivpnfrp  28240  xrge0addass  28289  xrge0neqmnf  28290  xrge0addgt0  28292  xrge0adddir  28293  xrge0npcan  28295  fsumrp0cl  28296  pnfinf  28338  xrnarchi  28339  xrge0tsmsd  28387  xrge0slmod  28446  unitssxrge0  28545  tpr2rico  28557  xrge0iifcnv  28578  xrge0iifiso  28580  xrge0iifhom  28582  xrge0mulc1cn  28586  pnfneige0  28596  lmxrge0  28597  esumle  28718  esumlef  28722  esumcst  28723  esumpr2  28727  esumpinfval  28733  esumpinfsum  28737  esumpcvgval  28738  hashf2  28744  esumcvg  28746  esumcvgsum  28748  voliune  28891  volfiniune  28892  ddemeas  28898  sxbrsigalem0  28932  sxbrsigalem2  28947  oms0  28958  sibfinima  29000  probmeasb  29089  orvcgteel  29126  dstfrvclim1  29136  signsply0  29228  iooelexlt  31499  mbfposadd  31692  itg2addnclem2  31698  ftc1anclem5  31725  asindmre  31731  dvasin  31732  dvacos  31733  dvconstbi  36320  rfcnpre3  36994  xadd0ge  37151  xrgepnfd  37163  xrge0nemnfd  37164  supxrgere  37165  supxrgelem  37169  supxrge  37170  iocopn  37206  pnfel0pnf  37214  ge0nemnf2  37215  ge0xrre  37218  fsumge0cl  37227  limcicciooub  37289  limsupre  37293  limsupreOLD  37294  limcresiooub  37295  limcleqr  37297  icccncfext  37337  iblsplit  37412  itgsubsticclem  37421  fourierdlem31  37569  fourierdlem33  37571  fourierdlem46  37584  fourierdlem47  37585  fourierdlem48  37586  fourierdlem49  37587  fourierdlem65  37603  fourierdlem73  37611  fourierdlem75  37613  fourierdlem85  37623  fourierdlem88  37626  fourierdlem95  37633  fourierdlem97  37635  fourierdlem103  37641  fourierdlem104  37642  fourierdlem107  37645  fourierdlem109  37647  fourierdlem111  37649  fourierdlem112  37650  fourierdlem113  37651  fouriersw  37663  sge0val  37742  fge0iccico  37746  gsumge0cl  37747  sge0sn  37755  sge0tsms  37756  sge0cl  37757  sge0f1o  37758  sge0ge0  37760  sge0repnf  37762  sge0fsum  37763  sge0pr  37770  sge0prle  37777  sge0split  37785  sge0p1  37790  sge0iunmptlemre  37791  omessre  37840  omeiunltfirp  37849  carageniuncllem2  37852  carageniuncl  37853
  Copyright terms: Public domain W3C validator