Theorem rexrd 11363

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
rexrd	⊢ (𝜑 → 𝐴 ∈ ℝ*)

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 11357	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3906	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11203  ℝ^*cxr 11346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-xr 11351

This theorem is used by:  xnn0xr  12688  rpxr  13134  rpxrd  13169  max0sub  13330  qextltlem  13336  xralrple  13339  xnegcl  13347  xaddf  13358  xnn0lem1lt  13378  xnn0lenn0nn0  13379  xmulf  13406  xadddi  13429  xrub  13446  supxrre  13461  infxrre  13471  ixxub  13501  ixxlb  13502  ioo0  13505  ico0  13526  ioc0  13527  iooshf  13561  icoshftf1o  13609  supicc  13636  supiccub  13637  supicclub  13638  xnn0xrge0  13641  ssfzunsn  13708  addmodid  14066  hashnnn0genn0  14491  hashunsnggt  14542  sgnsub  15265  sgnmul  15266  sgnmulsgn  15268  elicc4abs  15493  caucvgrlem  15846  fprodge1  16168  pcxcl  17045  pcdvdsb  17053  pcaddlem  17072  ramcl2lem  17193  ramlb  17203  0ram  17204  setsstruct  17360  prdsxmetlem  24693  xblss2ps  24726  xblss2  24727  blss2ps  24728  blss2  24729  blhalf  24730  metustto  24878  metustexhalf  24881  nmoi  25053  nmoix  25054  nmoi2  25055  nmoleub  25056  qdensere  25094  cnblcld  25099  ioo2blex  25119  tgioo  25121  blcvx  25123  zcld  25139  recld2  25140  iccntr  25147  icccmplem1  25148  reconnlem1  25152  reconnlem2  25153  opnreen  25157  metnrmlem3  25187  icoopnst  25266  iocopnst  25267  cnheibor  25282  lebnumii  25293  nmoleub2lem  25441  lmnn  25590  iscau3  25605  minveclem4  25759  ivthlem1  25778  ivthlem2  25779  ivthlem3  25780  ivth2  25782  ivthle  25783  ivthle2  25784  ivthicc  25785  evthicc  25786  cniccbdd  25788  ovolgelb  25807  ovollb2lem  25815  ovolunlem1  25824  ovoliunlem1  25829  ovoliunlem2  25830  ovoliun  25832  ovolscalem1  25840  ovolicc1  25843  ovolicc2lem4  25847  ovolicc2lem5  25848  ovolicc2  25849  ovolicc  25850  nulmbl2  25863  voliunlem2  25878  ioombl1lem4  25888  ioorcl2  25899  uniioombllem1  25908  uniioombllem2a  25909  uniioombllem3  25912  dyaddisjlem  25922  dyadmaxlem  25924  opnmbllem  25928  volivth  25934  vitalilem4  25938  mbfmulc2lem  25974  mbfmax  25976  mbfposr  25979  ismbf3d  25981  mbfaddlem  25987  mbflimsup  25993  mbfi1fseqlem4  26045  itg2lcl  26054  xrge0f  26058  itg2itg1  26063  itg2const2  26068  itg2seq  26069  itg2uba  26070  itg2lea  26071  itg2mulclem  26073  itg2mulc  26074  itg2splitlem  26075  itg2split  26076  itg2monolem2  26078  itg2monolem3  26079  itg2mono  26080  itg2gt0  26087  itg2cnlem1  26088  itg2cnlem2  26089  itg2cn  26090  iblss  26131  itgle  26136  itgeqa  26140  itgioo  26142  ibladdlem  26146  iblabs  26155  iblabsr  26156  iblmulc2  26157  itgsplit  26162  itgspliticc  26163  itgsplitioo  26164  bddmulibl  26165  bddiblnc  26168  ditgcl  26184  ditgswap  26185  ditgsplitlem  26186  dvferm1lem  26310  dvferm2lem  26312  dvferm  26314  rollelem  26315  rolle  26316  cmvth  26317  mvth  26318  dvlip  26319  dvlip2  26321  c1liplem1  26322  c1lip1  26323  dveq0  26326  dvgt0lem1  26328  dvivthlem1  26334  dvivth  26336  lhop1lem  26339  lhop1  26340  lhop2  26341  lhop  26342  dvcnvrelem1  26343  dvcnvre  26345  dvcvx  26346  dvfsumle  26347  dvfsumge  26348  dvfsumabs  26349  dvfsumlem2  26353  dvfsumlem3  26354  dvfsumlem4  26355  dvfsumrlimge0  26356  dvfsumrlim2  26358  ftc1lem1  26361  ftc1lem2  26362  ftc1a  26363  ftc1lem4  26365  ftc2  26370  ftc2ditglem  26371  itgparts  26373  itgsubstlem  26374  itgsubst  26375  itgpowd  26376  degltlem1  26396  deg1ge  26422  coe1mul3  26423  deg1sublt  26434  deg1mul2  26438  deg1tmle  26442  deg1tm  26443  idomrootle  26497  plypf1  26537  taylfvallem1  26690  tayl0  26695  pserulm  26755  psercnlem1  26758  pserdvlem1  26760  pserdvlem2  26761  abelthlem3  26766  abelth  26774  efcvx  26782  logno1  26970  logtayl  26994  xrlimcnp  27302  logfacbnd3  27556  log2sumbnd  27877  pntpbnd2  27920  pntibndlem3  27925  ttgcontlem1  29468  nmooge0  31375  nmoub3i  31381  isblo3i  31409  ubthlem1  31478  minvecolem4  31488  nmopge0  32519  nmfnge0  32535  nmophmi  32639  branmfn  32713  sgnval2  33374  nn0mnfxrd  33390  xaddeq0  33392  xlt2addrd  33398  sgnmulsgp  33470  xmulcand  33534  xreceu  33535  xdivrec  33540  fsumrp0cl  33629  xrge0slmod  33956  ply1degltel  34173  ply1degleel  34174  ply1degltlss  34175  ply1degltdimlem  34301  ply1degltdim  34302  fldextrspundgdvdslem  34359  extdgfialglem1  34371  cos9thpiminplylem2  34462  cnre2csqlem  34589  tpr2rico  34591  xrge0iifcnv  34612  xrge0iifhom  34616  lmxrge0  34631  esumfsup  34749  esumpcvgval  34757  esumcvg  34765  dya2iocress  34953  dya2iocbrsiga  34954  dya2icobrsiga  34955  dya2icoseg  34956  dya2iocucvr  34963  sxbrsigalem2  34965  omssubaddlem  34978  omssubadd  34979  orvcgteel  35147  dstrvprob  35151  orvclteel  35152  signstcl  35241  signstf  35242  signstf0  35244  signstfvn  35245  signsvtn0  35246  signsvfn  35258  signsvfpn  35261  signsvfnn  35262  ftc2re  35274  cvmliftlem6  36142  cvmliftlem7  36143  cvmliftlem8  36144  cvmliftlem9  36145  cvmliftlem10  36146  cvmliftlem13  36148  ivthALT  37216  iooelexlt  38379  relowlssretop  38380  relowlpssretop  38381  sin2h  38627  cos2h  38628  tan2h  38629  poimirlem30  38662  poimir  38665  heicant  38667  opnmbllem0  38668  mblfinlem1  38669  mblfinlem2  38670  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  itg2addnclem  38683  itg2addnclem2  38684  itg2gt0cn  38687  ibladdnclem  38688  iblabsnclem  38695  iblabsnc  38696  iblmulc2nc  38697  ftc1cnnclem  38703  ftc1anclem1  38705  ftc1anclem4  38708  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  ftc2nc  38714  areacirclem1  38720  areacirclem5  38724  areacirc  38725  isbnd3  38812  blbnd  38815  prdsbnd  38821  prdsbnd2  38823  cntotbnd  38824  dvrelog3  43209  0nonelalab  43211  dvrelogpow2b  43212  dvle2  43216  aks4d1p1p6  43217  aks4d1p1p5  43219  aks6d1c6lem3  43316  aks6d1c7lem2  43325  unitscyglem5  43343  idomodle  44287  imo72b2  45266  cvgdvgrat  45391  radcnvrat  45392  rfcnpre3  46144  rfcnpre4  46145  absfico  46325  nnxrd  46384  lefldiveq  46402  lttri5d  46409  supxrgere  46439  supxrgelem  46443  supxrge  46444  xralrple2  46460  infxr  46472  infleinflem1  46475  infleinflem2  46476  xralrple4  46478  xralrple3  46479  xrralrecnnle  46488  xrralrecnnge  46495  supxrunb3  46504  unb2ltle  46519  zxrd  46557  gtnelioc  46597  ltnelicc  46603  iooabslt  46605  gtnelicc  46606  eliooshift  46612  iocopn  46626  eliccelioc  46627  iooshift  46628  icoopn  46631  ge0lere  46638  iooiinicc  46648  sqrlearg  46659  iooiinioc  46662  uzinico  46665  preimaiocmnf  46666  uzubioo  46671  fsumge0cl  46679  limciccioolb  46727  lptioo1  46738  limcicciooub  46741  ltmod  46742  lptre2pt  46744  limsupre  46745  limcresiooub  46746  limcresioolb  46747  limcleqr  46748  limsupresico  46804  limsuppnfdlem  46805  limsupub  46808  limsupequzlem  46826  limsupre2lem  46828  limsupre3lem  46836  limsupvaluz2  46842  supcnvlimsup  46844  liminfresico  46875  limsup10exlem  46876  liminflelimsuplem  46879  limsupgtlem  46881  liminfval4  46893  liminfvaluz2  46899  limsupvaluz4  46904  liminflimsupclim  46911  xlimxrre  46935  xlimmnfvlem1  46936  xlimmnfv  46938  xlimpnfvlem1  46940  xlimpnfv  46942  sinaover2ne0  46972  ioccncflimc  46989  icccncfext  46991  icocncflimc  46993  cncfiooicclem1  46997  cncfiooicc  46998  cncfiooiccre  46999  cncfioobdlem  47000  dvbdfbdioolem1  47032  dvbdfbdioolem2  47033  dvbdfbdioo  47034  ioodvbdlimc1lem1  47035  ioodvbdlimc1lem2  47036  ioodvbdlimc1  47037  ioodvbdlimc2lem  47038  ioodvbdlimc2  47039  ditgeqiooicc  47064  iblsplit  47070  itgcoscmulx  47073  ibliooicc  47075  iblspltprt  47077  itgsincmulx  47078  itgsubsticc  47080  itgioocnicc  47081  iblcncfioo  47082  itgspltprt  47083  itgiccshift  47084  volioore  47094  voliooico  47096  voliooicof  47100  voliccico  47103  stoweidlem34  47138  stoweidlem52  47156  stirlinglem5  47182  dirkercncflem1  47207  dirkercncflem4  47210  fourierdlem4  47215  fourierdlem10  47221  fourierdlem19  47230  fourierdlem20  47231  fourierdlem24  47235  fourierdlem25  47236  fourierdlem26  47237  fourierdlem27  47238  fourierdlem28  47239  fourierdlem31  47242  fourierdlem32  47243  fourierdlem33  47244  fourierdlem35  47246  fourierdlem37  47248  fourierdlem40  47251  fourierdlem41  47252  fourierdlem43  47254  fourierdlem44  47255  fourierdlem46  47256  fourierdlem47  47257  fourierdlem48  47258  fourierdlem49  47259  fourierdlem50  47260  fourierdlem51  47261  fourierdlem52  47262  fourierdlem54  47264  fourierdlem57  47267  fourierdlem59  47269  fourierdlem60  47270  fourierdlem61  47271  fourierdlem62  47272  fourierdlem63  47273  fourierdlem64  47274  fourierdlem65  47275  fourierdlem68  47278  fourierdlem69  47279  fourierdlem70  47280  fourierdlem72  47282  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem78  47288  fourierdlem79  47289  fourierdlem81  47291  fourierdlem82  47292  fourierdlem84  47294  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem92  47302  fourierdlem93  47303  fourierdlem94  47304  fourierdlem97  47307  fourierdlem100  47310  fourierdlem101  47311  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem107  47317  fourierdlem109  47319  fourierdlem111  47321  fourierdlem112  47322  fourierdlem113  47323  fourierdlem114  47324  sqwvfoura  47332  fouriersw  47335  etransclem23  47361  etransclem46  47384  qndenserrnbllem  47398  rrxsnicc  47404  ioorrnopnlem  47408  ioorrnopnxrlem  47410  salgencntex  47447  sge0cl  47485  sge0fsum  47491  sge0iunmptlemre  47519  sge0isum  47531  sge0ad2en  47535  sge0xaddlem1  47537  sge0xaddlem2  47538  sge0reuz  47551  voliunsge0lem  47576  meassre  47581  omessre  47614  omeiunltfirp  47623  hoissre  47648  hoiprodcl  47651  ovnsubaddlem1  47674  hoiprodcl3  47684  hoidmvcl  47686  hsphoidmvle2  47689  hsphoidmvle  47690  sge0hsphoire  47693  hoidmv1lelem1  47695  hoidmv1lelem2  47696  hoidmv1lelem3  47697  hoidmv1le  47698  hoidmvlelem1  47699  hoidmvlelem2  47700  hoidmvlelem3  47701  hoidmvlelem4  47702  ovnhoilem1  47705  ovnhoilem2  47706  ovnhoi  47707  ovnlecvr2  47714  hspdifhsp  47720  hoidifhspdmvle  47724  hoiqssbllem1  47726  hoiqssbllem2  47727  hoiqssbllem3  47728  hspmbllem1  47730  hspmbllem2  47731  volicorege0  47741  ovolval5lem1  47756  ovolval5lem2  47757  iinhoiicclem  47777  iinhoiicc  47778  iunhoiioolem  47779  iunhoiioo  47780  vonioolem2  47785  vonicclem2  47788  vonsn  47795  pimltmnf2f  47801  pimconstlt0  47805  pimgtpnf2f  47809  salpreimagelt  47811  salpreimalegt  47813  preimageiingt  47824  preimaleiinlt  47825  pimrecltneg  47828  issmflem  47831  issmflelem  47848  issmfgtlem  47859  issmfgt  47860  smfaddlem1  47867  issmfgelem  47873  issmfge  47874  smfpimioompt  47890  smfresal  47892  smfrec  47893  smfmullem1  47895  smfmullem2  47896  smfmullem3  47897  smfmullem4  47898  smfpimbor1lem1  47902  smfsuplem1  47915  smflimsuplem4  47927  smfliminflem  47934  smfdmmblpimne  47941  smfpimne  47943  smfpimne2  47944  fsupdm  47946  finfdm  47950  smfinfdmmbllem  47952  bgoldbtbnd  49001  eenglngeehlnmlem2  49945