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

Theorem pnfxr 11350
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 3667 . . 3
2 df-pnf 9651 . . . . 5
3 cnex 9594 . . . . . . 7
43uniex 6596 . . . . . 6
54pwex 4635 . . . . 5
62, 5eqeltri 2541 . . . 4
76prid1 4138 . . 3
81, 7sselii 3500 . 2
9 df-xr 9653 . 2
108, 9eleqtrri 2544 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  u.cun 3473  ~Pcpw 4012  {cpr 4031  U.cuni 4249   cc 9511   cr 9512   cpnf 9646   cmnf 9647   cxr 9648
This theorem is referenced by:  pnfex  11351  pnfnemnf  11355  xrltnr  11359  ltpnf  11360  mnfltpnf  11364  pnfnlt  11366  pnfge  11368  nltpnft  11396  xrre  11399  xrre2  11400  xnegcl  11441  xaddf  11452  xaddpnf1  11454  xaddpnf2  11455  pnfaddmnf  11458  mnfaddpnf  11459  xaddass2  11471  xlt2add  11481  xsubge0  11482  xmulneg1  11490  xmulf  11493  xmulpnf1  11495  xmulpnf2  11496  xmulmnf1  11497  xmulpnf1n  11499  xlemul1a  11509  xadddilem  11515  xadddi2  11518  xrsupsslem  11527  xrinfmsslem  11528  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  supxrbnd  11549  xrinfm0  11557  elioc2  11616  elico2  11617  elicc2  11618  ioomax  11628  iccmax  11629  ioopos  11630  elioopnf  11647  elicopnf  11649  unirnioo  11653  elxrge0  11658  difreicc  11681  ioopnfsup  11991  icopnfsup  11992  xrsup  11995  hashbnd  12411  hashnnn0genn0  12416  hashxrcl  12429  hashdomi  12448  sgnpnf  12926  rexico  13186  limsupgre  13304  rlim3  13321  pcxcl  14384  pc2dvds  14402  pcadd  14408  ramxrcl  14535  ramubcl  14536  xrsnsgrp  18454  xrsdsreclblem  18464  rge0srg  18487  leordtvallem1  19711  leordtval2  19713  lecldbas  19720  pnfnei  19721  mnfnei  19722  xblpnfps  20898  xblpnf  20899  xblss2ps  20904  blssec  20938  blpnfctr  20939  nmoix  21236  icopnfcld  21275  iocmnfcld  21276  xrtgioo  21311  reconnlem1  21331  xrge0tsms  21339  metdstri  21355  iccpnfcnv  21444  ovolf  21893  ovolicopnf  21935  ovolre  21936  volsup  21966  ioombl1lem4  21971  icombl1  21973  icombl  21974  ioombl  21975  uniioombllem1  21990  mbfdm  22035  ismbfd  22047  mbfmax  22056  ismbf3d  22061  itg2ge0  22142  lhop2  22416  dvfsumlem2  22428  dvfsumrlim  22432  dvfsumrlim2  22433  taylfvallem1  22752  taylfval  22754  tayl0  22757  radcnvcl  22812  radcnvle  22815  psercnlem1  22820  logccv  23044  rlimcnp  23295  rlimcnp2  23296  xrlimcnp  23298  logfacbnd3  23498  chebbnd1  23657  chebbnd2  23662  dchrisumlem3  23676  log2sumbnd  23729  pntpbnd1  23771  pntibndlem2  23776  pntlemb  23782  pntleme  23793  pnt  23799  umgrafi  24322  sizeusglecusg  24486  isblo3i  25716  xgepnf  27570  xrge0infss  27580  xrdifh  27591  elxrge02  27628  xdivpnfrp  27629  xrge0addass  27678  xrge0neqmnf  27679  xrge0addgt0  27681  xrge0adddir  27682  xrge0npcan  27684  fsumrp0cl  27685  pnfinf  27727  xrnarchi  27728  xrge0tsmsd  27775  xrge0slmod  27834  unitssxrge0  27882  tpr2rico  27894  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  xrge0mulc1cn  27923  pnfneige0  27933  lmxrge0  27934  esumle  28065  esumlef  28070  esumcst  28071  esumpr2  28074  esumpinfval  28079  esumpinfsum  28083  esumpcvgval  28084  hashf2  28090  esumcvg  28092  voliune  28201  volfiniune  28202  ddemeas  28208  sxbrsigalem0  28242  sxbrsigalem2  28257  oms0  28266  sibfinima  28281  probmeasb  28369  orvcgteel  28406  dstfrvclim1  28416  signsply0  28508  mbfposadd  30062  itg2addnclem2  30067  ftc1anclem5  30094  asindmre  30102  dvasin  30103  dvacos  30104  dvconstbi  31239  rfcnpre3  31408  elicore  31537  iocopn  31560  fprodge0  31597  fprodge1  31598  limcicciooub  31643  limsupre  31647  limcresiooub  31648  limcleqr  31650  icccncfext  31690  iblsplit  31765  itgsubsticclem  31774  fourierdlem31  31920  fourierdlem33  31922  fourierdlem46  31935  fourierdlem47  31936  fourierdlem48  31937  fourierdlem49  31938  fourierdlem65  31954  fourierdlem73  31962  fourierdlem75  31964  fourierdlem85  31974  fourierdlem88  31977  fourierdlem95  31984  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem109  31998  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fouriersw  32014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-pow 4630  ax-un 6592  ax-cnex 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-pw 4014  df-sn 4030  df-pr 4032  df-uni 4250  df-pnf 9651  df-xr 9653
  Copyright terms: Public domain W3C validator