Theorem rexrd 11311

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 11305	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3981	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℝ^*cxr 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-xr 11299

This theorem is referenced by:  xnn0xr  12604  rpxr  13044  rpxrd  13078  max0sub  13238  qextltlem  13244  xralrple  13247  xnegcl  13255  xaddf  13266  xnn0lem1lt  13286  xnn0lenn0nn0  13287  xmulf  13314  xadddi  13337  xrub  13354  supxrre  13369  infxrre  13378  ixxub  13408  ixxlb  13409  ioo0  13412  ico0  13433  ioc0  13434  iooshf  13466  icoshftf1o  13514  supicc  13541  supiccub  13542  supicclub  13543  xnn0xrge0  13546  ssfzunsn  13610  addmodid  13960  hashnnn0genn0  14382  hashunsnggt  14433  elicc4abs  15358  caucvgrlem  15709  fprodge1  16031  pcxcl  16899  pcdvdsb  16907  pcaddlem  16926  ramcl2lem  17047  ramlb  17057  0ram  17058  setsstruct  17213  prdsxmetlem  24378  xblss2ps  24411  xblss2  24412  blss2ps  24413  blss2  24414  blhalf  24415  metustto  24566  metustexhalf  24569  nmoi  24749  nmoix  24750  nmoi2  24751  nmoleub  24752  qdensere  24790  cnblcld  24795  ioo2blex  24815  tgioo  24817  blcvx  24819  zcld  24835  recld2  24836  iccntr  24843  icccmplem1  24844  reconnlem1  24848  reconnlem2  24849  opnreen  24853  metnrmlem3  24883  icoopnst  24969  iocopnst  24970  cnheibor  24987  lebnumii  24998  nmoleub2lem  25147  lmnn  25297  iscau3  25312  minveclem4  25466  ivthlem1  25486  ivthlem2  25487  ivthlem3  25488  ivth2  25490  ivthle  25491  ivthle2  25492  ivthicc  25493  evthicc  25494  cniccbdd  25496  ovolgelb  25515  ovollb2lem  25523  ovolunlem1  25532  ovoliunlem1  25537  ovoliunlem2  25538  ovoliun  25540  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem4  25555  ovolicc2lem5  25556  ovolicc2  25557  ovolicc  25558  nulmbl2  25571  voliunlem2  25586  ioombl1lem4  25596  ioorcl2  25607  uniioombllem1  25616  uniioombllem2a  25617  uniioombllem3  25620  dyaddisjlem  25630  dyadmaxlem  25632  opnmbllem  25636  volivth  25642  vitalilem4  25646  mbfmulc2lem  25682  mbfmax  25684  mbfposr  25687  ismbf3d  25689  mbfaddlem  25695  mbflimsup  25701  mbfi1fseqlem4  25753  itg2lcl  25762  xrge0f  25766  itg2itg1  25771  itg2const2  25776  itg2seq  25777  itg2uba  25778  itg2lea  25779  itg2mulclem  25781  itg2mulc  25782  itg2splitlem  25783  itg2split  25784  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  iblss  25840  itgle  25845  itgeqa  25849  itgioo  25851  ibladdlem  25855  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgsplit  25871  itgspliticc  25872  itgsplitioo  25873  bddmulibl  25874  bddiblnc  25877  ditgcl  25893  ditgswap  25894  ditgsplitlem  25895  dvferm1lem  26022  dvferm2lem  26024  dvferm  26026  rollelem  26027  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlip2  26034  c1liplem1  26035  c1lip1  26036  dveq0  26039  dvgt0lem1  26041  dvivthlem1  26047  dvivth  26049  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcnvre  26058  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlimge0  26071  dvfsumrlim2  26073  ftc1lem1  26076  ftc1lem2  26077  ftc1a  26078  ftc1lem4  26080  ftc2  26085  ftc2ditglem  26086  itgparts  26088  itgsubstlem  26089  itgsubst  26090  itgpowd  26091  degltlem1  26111  deg1ge  26137  coe1mul3  26138  deg1sublt  26149  deg1mul2  26153  deg1tmle  26157  deg1tm  26158  idomrootle  26212  plypf1  26251  taylfvallem1  26398  tayl0  26403  pserulm  26465  psercnlem1  26469  pserdvlem1  26471  pserdvlem2  26472  abelthlem3  26477  abelth  26485  efcvx  26493  logno1  26678  logtayl  26702  xrlimcnp  27011  logfacbnd3  27267  log2sumbnd  27588  pntpbnd2  27631  pntibndlem3  27636  ttgcontlem1  28899  nmooge0  30786  nmoub3i  30792  isblo3i  30820  ubthlem1  30889  minvecolem4  30899  nmopge0  31930  nmfnge0  31946  nmophmi  32050  branmfn  32124  xaddeq0  32757  xlt2addrd  32762  xmulcand  32903  xreceu  32904  xdivrec  32909  fsumrp0cl  33026  xrge0slmod  33376  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  ply1degltdimlem  33673  ply1degltdim  33674  fldextrspundgdvdslem  33730  cnre2csqlem  33909  tpr2rico  33911  xrge0iifcnv  33932  xrge0iifhom  33936  lmxrge0  33951  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  dya2iocress  34276  dya2iocbrsiga  34277  dya2icobrsiga  34278  dya2icoseg  34279  dya2iocucvr  34286  sxbrsigalem2  34288  omssubaddlem  34301  omssubadd  34302  orvcgteel  34470  dstrvprob  34474  orvclteel  34475  sgnmul  34545  sgnsub  34547  sgnmulsgn  34552  sgnmulsgp  34553  signstcl  34580  signstf  34581  signstf0  34583  signstfvn  34584  signsvtn0  34585  signsvfn  34597  signsvfpn  34600  signsvfnn  34601  ftc2re  34613  cvmliftlem6  35295  cvmliftlem7  35296  cvmliftlem8  35297  cvmliftlem9  35298  cvmliftlem10  35299  cvmliftlem13  35301  ivthALT  36336  iooelexlt  37363  relowlssretop  37364  relowlpssretop  37365  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem30  37657  poimir  37660  heicant  37662  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnclem2  37679  itg2gt0cn  37682  ibladdnclem  37683  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  ftc1cnnclem  37698  ftc1anclem1  37700  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  areacirclem1  37715  areacirclem5  37719  areacirc  37720  isbnd3  37791  blbnd  37794  prdsbnd  37800  prdsbnd2  37802  cntotbnd  37803  dvrelog3  42066  0nonelalab  42068  dvrelogpow2b  42069  dvle2  42073  aks4d1p1p6  42074  aks4d1p1p5  42076  aks6d1c6lem3  42173  aks6d1c7lem2  42182  unitscyglem5  42200  idomodle  43203  imo72b2  44185  cvgdvgrat  44332  radcnvrat  44333  rfcnpre3  45038  rfcnpre4  45039  absfico  45223  nnxrd  45285  lefldiveq  45304  lttri5d  45311  supxrgere  45344  supxrgelem  45348  supxrge  45349  xralrple2  45365  infxr  45378  infleinflem1  45381  infleinflem2  45382  xralrple4  45384  xralrple3  45385  xrralrecnnle  45394  xrralrecnnge  45401  supxrunb3  45410  unb2ltle  45426  zxrd  45464  gtnelioc  45504  ltnelicc  45510  iooabslt  45512  gtnelicc  45513  eliooshift  45519  iocopn  45533  eliccelioc  45534  iooshift  45535  icoopn  45538  ge0lere  45545  iooiinicc  45555  sqrlearg  45566  iooiinioc  45569  uzinico  45573  preimaiocmnf  45574  uzubioo  45580  fsumge0cl  45588  limciccioolb  45636  lptioo1  45647  limcicciooub  45652  ltmod  45653  lptre2pt  45655  limsupre  45656  limcresiooub  45657  limcresioolb  45658  limcleqr  45659  limsupresico  45715  limsuppnfdlem  45716  limsupub  45719  limsupequzlem  45737  limsupre2lem  45739  limsupre3lem  45747  limsupvaluz2  45753  supcnvlimsup  45755  liminfresico  45786  limsup10exlem  45787  liminflelimsuplem  45790  limsupgtlem  45792  liminfval4  45804  liminfvaluz2  45810  limsupvaluz4  45815  liminflimsupclim  45822  xlimxrre  45846  xlimmnfvlem1  45847  xlimmnfv  45849  xlimpnfvlem1  45851  xlimpnfv  45853  sinaover2ne0  45883  ioccncflimc  45900  icccncfext  45902  icocncflimc  45904  cncfiooicclem1  45908  cncfiooicc  45909  cncfiooiccre  45910  cncfioobdlem  45911  dvbdfbdioolem1  45943  dvbdfbdioolem2  45944  dvbdfbdioo  45945  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc1  45948  ioodvbdlimc2lem  45949  ioodvbdlimc2  45950  ditgeqiooicc  45975  iblsplit  45981  itgcoscmulx  45984  ibliooicc  45986  iblspltprt  45988  itgsincmulx  45989  itgsubsticc  45991  itgioocnicc  45992  iblcncfioo  45993  itgspltprt  45994  itgiccshift  45995  volioore  46005  voliooico  46007  voliooicof  46011  voliccico  46014  stoweidlem34  46049  stoweidlem52  46067  stirlinglem5  46093  dirkercncflem1  46118  dirkercncflem4  46121  fourierdlem4  46126  fourierdlem10  46132  fourierdlem19  46141  fourierdlem20  46142  fourierdlem24  46146  fourierdlem25  46147  fourierdlem26  46148  fourierdlem27  46149  fourierdlem28  46150  fourierdlem31  46153  fourierdlem32  46154  fourierdlem33  46155  fourierdlem35  46157  fourierdlem37  46159  fourierdlem40  46162  fourierdlem41  46163  fourierdlem43  46165  fourierdlem44  46166  fourierdlem46  46167  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem54  46175  fourierdlem57  46178  fourierdlem59  46180  fourierdlem60  46181  fourierdlem61  46182  fourierdlem62  46183  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem68  46189  fourierdlem69  46190  fourierdlem70  46191  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem84  46205  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem94  46215  fourierdlem97  46218  fourierdlem100  46221  fourierdlem101  46222  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem109  46230  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fourierdlem114  46235  sqwvfoura  46243  fouriersw  46246  etransclem23  46272  etransclem46  46295  qndenserrnbllem  46309  rrxsnicc  46315  ioorrnopnlem  46319  ioorrnopnxrlem  46321  salgencntex  46358  sge0cl  46396  sge0fsum  46402  sge0iunmptlemre  46430  sge0isum  46442  sge0ad2en  46446  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0reuz  46462  voliunsge0lem  46487  meassre  46492  omessre  46525  omeiunltfirp  46534  hoissre  46559  hoiprodcl  46562  ovnsubaddlem1  46585  hoiprodcl3  46595  hoidmvcl  46597  hsphoidmvle2  46600  hsphoidmvle  46601  sge0hsphoire  46604  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  ovnhoilem1  46616  ovnhoilem2  46617  ovnhoi  46618  ovnlecvr2  46625  hspdifhsp  46631  hoidifhspdmvle  46635  hoiqssbllem1  46637  hoiqssbllem2  46638  hoiqssbllem3  46639  hspmbllem1  46641  hspmbllem2  46642  volicorege0  46652  ovolval5lem1  46667  ovolval5lem2  46668  iinhoiicclem  46688  iinhoiicc  46689  iunhoiioolem  46690  iunhoiioo  46691  vonioolem2  46696  vonicclem2  46699  vonsn  46706  pimltmnf2f  46712  pimconstlt0  46716  pimgtpnf2f  46720  salpreimagelt  46722  salpreimalegt  46724  preimageiingt  46735  preimaleiinlt  46736  pimrecltneg  46739  issmflem  46742  issmflelem  46759  issmfgtlem  46770  issmfgt  46771  smfaddlem1  46778  issmfgelem  46784  issmfge  46785  smfpimioompt  46801  smfresal  46803  smfrec  46804  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  smfmullem4  46809  smfpimbor1lem1  46813  smfsuplem1  46826  smflimsuplem4  46838  smfliminflem  46845  smfdmmblpimne  46852  smfpimne  46854  smfpimne2  46855  fsupdm  46857  finfdm  46861  smfinfdmmbllem  46863  bgoldbtbnd  47796  eenglngeehlnmlem2  48659