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

Theorem rexrd 9139
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 9134 . 2  |-  RR  C_  RR*
2 rexrd.1 . 2  |-  ( ph  ->  A  e.  RR )
31, 2sseldi 3348 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RRcr 8994   RR*cxr 9124
This theorem is referenced by:  rpxr  10624  rpxrd  10654  max0sub  10787  qextltlem  10793  xralrple  10796  xnegcl  10804  xaddf  10815  xmulf  10856  xadddi  10879  supxrre  10911  infmxrre  10919  ixxub  10942  ixxlb  10943  ioo0  10946  ico0  10967  ioc0  10968  iooshf  10994  icoshftf1o  11025  hashnnn0genn0  11632  elicc4abs  12128  caucvgrlem  12471  pcxcl  13239  pcdvdsb  13247  pcaddlem  13262  ramcl2lem  13382  ramlb  13392  0ram  13393  prdsxmetlem  18403  xblss2ps  18436  xblss2  18437  blss2ps  18438  blss2  18439  blhalf  18440  metusttoOLD  18592  metustto  18593  metustexhalfOLD  18598  metustexhalf  18599  nmoi  18767  nmoix  18768  nmoi2  18769  nmoleub  18770  qdensere  18809  cnblcld  18814  ioo2blex  18830  tgioo  18832  blcvx  18834  zcld  18849  recld2  18850  iccntr  18857  icccmplem1  18858  reconnlem1  18862  reconnlem2  18863  opnreen  18867  metnrmlem3  18896  cnheibor  18985  lebnumii  18996  nmoleub2lem  19127  lmnn  19221  iscau3  19236  minveclem4  19338  ivthlem1  19353  ivthlem2  19354  ivthlem3  19355  ivth2  19357  ivthle  19358  ivthle2  19359  ivthicc  19360  evthicc  19361  cniccbdd  19363  ovolgelb  19381  ovollb2lem  19389  ovolunlem1  19398  ovoliunlem1  19403  ovoliunlem2  19404  ovoliun  19406  ovolscalem1  19414  ovolicc1  19417  ovolicc2lem4  19421  ovolicc2lem5  19422  ovolicc2  19423  ovolicc  19424  nulmbl2  19436  voliunlem2  19450  ioombl1lem4  19460  ioorcl2  19469  uniioombllem1  19478  uniioombllem2a  19479  uniioombllem3  19482  dyaddisjlem  19492  dyadmaxlem  19494  opnmbllem  19498  volivth  19504  vitalilem4  19508  mbfmulc2lem  19542  mbfmax  19544  mbfposr  19547  ismbf3d  19549  mbfaddlem  19555  mbflimsup  19561  mbfi1fseqlem4  19613  itg2lcl  19622  xrge0f  19626  itg2itg1  19631  itg2const2  19636  itg2seq  19637  itg2uba  19638  itg2lea  19639  itg2mulclem  19641  itg2mulc  19642  itg2splitlem  19643  itg2split  19644  itg2monolem2  19646  itg2monolem3  19647  itg2mono  19648  itg2gt0  19655  itg2cnlem1  19656  itg2cnlem2  19657  itg2cn  19658  iblss  19699  itgle  19704  itgeqa  19708  itgioo  19710  ibladdlem  19714  iblabs  19723  iblabsr  19724  iblmulc2  19725  itgsplit  19730  itgspliticc  19731  itgsplitioo  19732  bddmulibl  19733  ditgcl  19750  ditgswap  19751  ditgsplitlem  19752  dvferm1lem  19873  dvferm2lem  19875  dvferm  19877  rollelem  19878  rolle  19879  cmvth  19880  mvth  19881  dvlip  19882  dvlip2  19884  c1liplem1  19885  c1lip1  19886  dveq0  19889  dvgt0lem1  19891  dvivthlem1  19897  dvivth  19899  lhop1lem  19902  lhop1  19903  lhop2  19904  lhop  19905  dvcnvrelem1  19906  dvcnvre  19908  dvcvx  19909  dvfsumle  19910  dvfsumge  19911  dvfsumabs  19912  dvfsumlem2  19916  dvfsumlem3  19917  dvfsumlem4  19918  dvfsumrlimge0  19919  dvfsumrlim2  19921  ftc1lem1  19924  ftc1lem2  19925  ftc1a  19926  ftc1lem4  19928  ftc2  19933  ftc2ditglem  19934  itgparts  19936  itgsubstlem  19937  itgsubst  19938  degltlem1  20000  deg1ge  20026  coe1mul3  20027  deg1sublt  20038  deg1mul2  20042  deg1tmle  20045  deg1tm  20046  plypf1  20136  taylfvallem1  20278  tayl0  20283  pserulm  20343  psercnlem1  20346  pserdvlem1  20348  pserdvlem2  20349  abelthlem3  20354  abelth  20362  efcvx  20370  logno1  20532  logtayl  20556  xrlimcnp  20812  logfacbnd3  21012  log2sumbnd  21243  pntpbnd2  21286  pntibndlem3  21291  nvlmle  22193  nmooge0  22273  nmoub3i  22279  isblo3i  22307  ubthlem1  22377  minvecolem4  22387  nmopge0  23419  nmfnge0  23435  nmophmi  23539  branmfn  23613  xaddeq0  24124  xlt2addrd  24129  xmulcand  24172  xreceu  24173  xdivrec  24178  fsumrp0cl  24222  cnre2csqlem  24313  tpr2rico  24315  xrge0iifcnv  24324  xrge0iifhom  24328  lmxrge0  24342  esumfsup  24465  esumpcvgval  24473  esumcvg  24481  dya2iocress  24629  dya2iocbrsiga  24630  dya2icobrsiga  24631  dya2icoseg  24632  dya2iocucvr  24639  sxbrsigalem2  24641  orvcgteel  24730  dstrvprob  24734  orvclteel  24735  cvmliftlem6  24982  cvmliftlem7  24983  cvmliftlem8  24984  cvmliftlem9  24985  cvmliftlem10  24986  cvmliftlem13  24988  sin2h  26250  cos2h  26251  tan2h  26252  heicant  26253  opnmbllem0  26254  mblfinlem1  26255  mblfinlem2  26256  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  dvtanlem  26268  itg2addnclem  26270  itg2addnclem2  26271  itg2gt0cn  26274  ibladdnclem  26275  iblabsnclem  26282  iblabsnc  26283  iblmulc2nc  26284  bddiblnc  26289  ftc1cnnclem  26292  ftc1anclem1  26294  ftc1anclem4  26297  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  ftc2nc  26303  areacirclem1  26306  areacirclem5  26310  areacirc  26311  ivthALT  26352  isbnd3  26507  blbnd  26510  prdsbnd  26516  prdsbnd2  26518  cntotbnd  26519  idomrootle  27502  idomodle  27503  rfcnpre3  27694  rfcnpre4  27695  stoweidlem34  27773  stoweidlem52  27791  stirlinglem5  27817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-in 3329  df-ss 3336  df-xr 9129
  Copyright terms: Public domain W3C validator