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

Theorem rexrd 8881
Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rexrd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
rexrd  |-  ( ph  ->  A  e.  RR* )

Proof of Theorem rexrd
StepHypRef Expression
1 ressxr 8876 . 2  |-  RR  C_  RR*
2 rexrd.1 . 2  |-  ( ph  ->  A  e.  RR )
31, 2sseldi 3178 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   RRcr 8736   RR*cxr 8866
This theorem is referenced by:  rpxr  10361  rpxrd  10391  max0sub  10523  qextltlem  10529  xralrple  10532  xnegcl  10540  xaddf  10551  xmulf  10592  xadddi  10615  supxrre  10646  infmxrre  10654  ixxub  10677  ixxlb  10678  ioo0  10681  ico0  10702  ioc0  10703  iooshf  10728  icoshftf1o  10759  elicc4abs  11803  caucvgrlem  12145  pcxcl  12913  pcdvdsb  12921  pcaddlem  12936  ramcl2lem  13056  ramlb  13066  0ram  13067  prdsxmetlem  17932  xblss2  17958  blss2  17959  blhalf  17960  nmoi  18237  nmoix  18238  nmoi2  18239  nmoleub  18240  qdensere  18279  cnblcld  18284  ioo2blex  18300  tgioo  18302  blcvx  18304  zcld  18319  recld2  18320  iccntr  18326  icccmplem1  18327  reconnlem1  18331  reconnlem2  18332  opnreen  18336  metnrmlem3  18365  cnheibor  18453  lebnumii  18464  nmoleub2lem  18595  lmnn  18689  iscau3  18704  minveclem4  18796  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ivthle  18816  ivthle2  18817  ivthicc  18818  evthicc  18819  cniccbdd  18821  ovolgelb  18839  ovollb2lem  18847  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun  18864  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  ovolicc  18882  nulmbl2  18894  voliunlem2  18908  ioombl1lem4  18918  ioorcl2  18927  uniioombllem1  18936  uniioombllem2a  18937  uniioombllem3  18940  dyaddisjlem  18950  dyadmaxlem  18952  opnmbllem  18956  volivth  18962  vitalilem4  18966  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  ismbf3d  19009  mbfaddlem  19015  mbflimsup  19021  mbfi1fseqlem4  19073  itg2lcl  19082  xrge0f  19086  itg2itg1  19091  itg2const2  19096  itg2seq  19097  itg2uba  19098  itg2lea  19099  itg2mulclem  19101  itg2mulc  19102  itg2splitlem  19103  itg2split  19104  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  iblss  19159  itgle  19164  itgeqa  19168  itgioo  19170  ibladdlem  19174  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgsplit  19190  itgspliticc  19191  itgsplitioo  19192  bddmulibl  19193  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  dvferm1lem  19331  dvferm2lem  19333  dvferm  19335  rollelem  19336  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlip2  19342  c1liplem1  19343  c1lip1  19344  dveq0  19347  dvgt0lem1  19349  dvivthlem1  19355  dvivth  19357  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvre  19366  dvcvx  19367  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlimge0  19377  dvfsumrlim2  19379  ftc1lem1  19382  ftc1lem2  19383  ftc1a  19384  ftc1lem4  19386  ftc2  19391  ftc2ditglem  19392  itgparts  19394  itgsubstlem  19395  itgsubst  19396  degltlem1  19458  deg1ge  19484  coe1mul3  19485  deg1sublt  19496  deg1mul2  19500  deg1tmle  19503  deg1tm  19504  plypf1  19594  taylfvallem1  19736  tayl0  19741  pserulm  19798  psercnlem1  19801  pserdvlem1  19803  pserdvlem2  19804  abelthlem3  19809  abelth  19817  efcvx  19825  logno1  19983  logtayl  20007  xrlimcnp  20263  logfacbnd3  20462  log2sumbnd  20693  pntpbnd2  20736  pntibndlem3  20741  nvlmle  21265  nmooge0  21345  nmoub3i  21351  isblo3i  21379  ubthlem1  21449  minvecolem4  21459  nmopge0  22491  nmfnge0  22507  nmophmi  22611  branmfn  22685  xmulcand  23104  xreceu  23105  xdivrec  23110  xlt2addrd  23253  cnre2csqlem  23294  cnre2csqima  23295  tpr2rico  23296  xaddeq0  23304  xrge0iifhom  23319  fsumrp0cl  23334  lmxrge0  23375  esumpcvgval  23446  esumcvg  23454  dya2iocress  23577  dya2iocbrsiga  23578  dya2iocseg  23579  orvcgteel  23668  orvclteel  23673  cvmliftlem6  23821  cvmliftlem7  23822  cvmliftlem8  23823  cvmliftlem9  23824  cvmliftlem10  23825  cvmliftlem13  23827  areacirclem2  24925  areacirclem3  24926  areacirclem6  24930  areacirc  24931  truni1  25505  truni3  25507  cbci  25508  iintlem1  25610  icccon3  25701  ivthALT  26258  isbnd3  26508  blbnd  26511  prdsbnd  26517  prdsbnd2  26519  cntotbnd  26520  idomrootle  27511  idomodle  27512  stirlinglem5  27827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-xr 8871
  Copyright terms: Public domain W3C validator