Theorem rexrd 11186

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  ℝ^*cxr 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-xr 11174

This theorem is referenced by:  xnn0xr  12506  rpxr  12943  rpxrd  12978  max0sub  13139  qextltlem  13145  xralrple  13148  xnegcl  13156  xaddf  13167  xnn0lem1lt  13187  xnn0lenn0nn0  13188  xmulf  13215  xadddi  13238  xrub  13255  supxrre  13270  infxrre  13280  ixxub  13310  ixxlb  13311  ioo0  13314  ico0  13335  ioc0  13336  iooshf  13370  icoshftf1o  13418  supicc  13445  supiccub  13446  supicclub  13447  xnn0xrge0  13450  ssfzunsn  13515  addmodid  13872  hashnnn0genn0  14296  hashunsnggt  14347  elicc4abs  15273  caucvgrlem  15626  fprodge1  15951  pcxcl  16823  pcdvdsb  16831  pcaddlem  16850  ramcl2lem  16971  ramlb  16981  0ram  16982  setsstruct  17137  prdsxmetlem  24343  xblss2ps  24376  xblss2  24377  blss2ps  24378  blss2  24379  blhalf  24380  metustto  24528  metustexhalf  24531  nmoi  24703  nmoix  24704  nmoi2  24705  nmoleub  24706  qdensere  24744  cnblcld  24749  ioo2blex  24769  tgioo  24771  blcvx  24773  zcld  24789  recld2  24790  iccntr  24797  icccmplem1  24798  reconnlem1  24802  reconnlem2  24803  opnreen  24807  metnrmlem3  24837  icoopnst  24916  iocopnst  24917  cnheibor  24932  lebnumii  24943  nmoleub2lem  25091  lmnn  25240  iscau3  25255  minveclem4  25409  ivthlem1  25428  ivthlem2  25429  ivthlem3  25430  ivth2  25432  ivthle  25433  ivthle2  25434  ivthicc  25435  evthicc  25436  cniccbdd  25438  ovolgelb  25457  ovollb2lem  25465  ovolunlem1  25474  ovoliunlem1  25479  ovoliunlem2  25480  ovoliun  25482  ovolscalem1  25490  ovolicc1  25493  ovolicc2lem4  25497  ovolicc2lem5  25498  ovolicc2  25499  ovolicc  25500  nulmbl2  25513  voliunlem2  25528  ioombl1lem4  25538  ioorcl2  25549  uniioombllem1  25558  uniioombllem2a  25559  uniioombllem3  25562  dyaddisjlem  25572  dyadmaxlem  25574  opnmbllem  25578  volivth  25584  vitalilem4  25588  mbfmulc2lem  25624  mbfmax  25626  mbfposr  25629  ismbf3d  25631  mbfaddlem  25637  mbflimsup  25643  mbfi1fseqlem4  25695  itg2lcl  25704  xrge0f  25708  itg2itg1  25713  itg2const2  25718  itg2seq  25719  itg2uba  25720  itg2lea  25721  itg2mulclem  25723  itg2mulc  25724  itg2splitlem  25725  itg2split  25726  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  itg2cn  25740  iblss  25782  itgle  25787  itgeqa  25791  itgioo  25793  ibladdlem  25797  iblabs  25806  iblabsr  25807  iblmulc2  25808  itgsplit  25813  itgspliticc  25814  itgsplitioo  25815  bddmulibl  25816  bddiblnc  25819  ditgcl  25835  ditgswap  25836  ditgsplitlem  25837  dvferm1lem  25961  dvferm2lem  25963  dvferm  25965  rollelem  25966  rolle  25967  cmvth  25968  mvth  25969  dvlip  25970  dvlip2  25972  c1liplem1  25973  c1lip1  25974  dveq0  25977  dvgt0lem1  25979  dvivthlem1  25985  dvivth  25987  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  dvcnvrelem1  25994  dvcnvre  25996  dvcvx  25997  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  dvfsumlem2  26004  dvfsumlem3  26005  dvfsumlem4  26006  dvfsumrlimge0  26007  dvfsumrlim2  26009  ftc1lem1  26012  ftc1lem2  26013  ftc1a  26014  ftc1lem4  26016  ftc2  26021  ftc2ditglem  26022  itgparts  26024  itgsubstlem  26025  itgsubst  26026  itgpowd  26027  degltlem1  26047  deg1ge  26073  coe1mul3  26074  deg1sublt  26085  deg1mul2  26089  deg1tmle  26093  deg1tm  26094  idomrootle  26148  plypf1  26187  taylfvallem1  26333  tayl0  26338  pserulm  26400  psercnlem1  26403  pserdvlem1  26405  pserdvlem2  26406  abelthlem3  26411  abelth  26419  efcvx  26427  logno1  26613  logtayl  26637  xrlimcnp  26945  logfacbnd3  27200  log2sumbnd  27521  pntpbnd2  27564  pntibndlem3  27569  ttgcontlem1  28967  nmooge0  30853  nmoub3i  30859  isblo3i  30887  ubthlem1  30956  minvecolem4  30966  nmopge0  31997  nmfnge0  32013  nmophmi  32117  branmfn  32191  sgnval2  32823  nn0mnfxrd  32839  xaddeq0  32841  xlt2addrd  32847  sgnmul  32923  sgnsub  32925  sgnmulsgn  32930  sgnmulsgp  32931  xmulcand  32995  xreceu  32996  xdivrec  33001  fsumrp0cl  33096  xrge0slmod  33423  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  ply1degltdimlem  33782  ply1degltdim  33783  fldextrspundgdvdslem  33840  extdgfialglem1  33852  cos9thpiminplylem2  33943  cnre2csqlem  34070  tpr2rico  34072  xrge0iifcnv  34093  xrge0iifhom  34097  lmxrge0  34112  esumfsup  34230  esumpcvgval  34238  esumcvg  34246  dya2iocress  34434  dya2iocbrsiga  34435  dya2icobrsiga  34436  dya2icoseg  34437  dya2iocucvr  34444  sxbrsigalem2  34446  omssubaddlem  34459  omssubadd  34460  orvcgteel  34628  dstrvprob  34632  orvclteel  34633  signstcl  34725  signstf  34726  signstf0  34728  signstfvn  34729  signsvtn0  34730  signsvfn  34742  signsvfpn  34745  signsvfnn  34746  ftc2re  34758  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  cvmliftlem13  35494  ivthALT  36533  iooelexlt  37692  relowlssretop  37693  relowlpssretop  37694  sin2h  37945  cos2h  37946  tan2h  37947  poimirlem30  37985  poimir  37988  heicant  37990  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  itg2addnclem  38006  itg2addnclem2  38007  itg2gt0cn  38010  ibladdnclem  38011  iblabsnclem  38018  iblabsnc  38019  iblmulc2nc  38020  ftc1cnnclem  38026  ftc1anclem1  38028  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  ftc2nc  38037  areacirclem1  38043  areacirclem5  38047  areacirc  38048  isbnd3  38119  blbnd  38122  prdsbnd  38128  prdsbnd2  38130  cntotbnd  38131  dvrelog3  42518  0nonelalab  42520  dvrelogpow2b  42521  dvle2  42525  aks4d1p1p6  42526  aks4d1p1p5  42528  aks6d1c6lem3  42625  aks6d1c7lem2  42634  unitscyglem5  42652  idomodle  43637  imo72b2  44617  cvgdvgrat  44758  radcnvrat  44759  rfcnpre3  45482  rfcnpre4  45483  absfico  45665  nnxrd  45725  lefldiveq  45743  lttri5d  45750  supxrgere  45781  supxrgelem  45785  supxrge  45786  xralrple2  45802  infxr  45814  infleinflem1  45817  infleinflem2  45818  xralrple4  45820  xralrple3  45821  xrralrecnnle  45830  xrralrecnnge  45837  supxrunb3  45846  unb2ltle  45861  zxrd  45899  gtnelioc  45939  ltnelicc  45945  iooabslt  45947  gtnelicc  45948  eliooshift  45954  iocopn  45968  eliccelioc  45969  iooshift  45970  icoopn  45973  ge0lere  45980  iooiinicc  45990  sqrlearg  46001  iooiinioc  46004  uzinico  46007  preimaiocmnf  46008  uzubioo  46013  fsumge0cl  46021  limciccioolb  46069  lptioo1  46080  limcicciooub  46083  ltmod  46084  lptre2pt  46086  limsupre  46087  limcresiooub  46088  limcresioolb  46089  limcleqr  46090  limsupresico  46146  limsuppnfdlem  46147  limsupub  46150  limsupequzlem  46168  limsupre2lem  46170  limsupre3lem  46178  limsupvaluz2  46184  supcnvlimsup  46186  liminfresico  46217  limsup10exlem  46218  liminflelimsuplem  46221  limsupgtlem  46223  liminfval4  46235  liminfvaluz2  46241  limsupvaluz4  46246  liminflimsupclim  46253  xlimxrre  46277  xlimmnfvlem1  46278  xlimmnfv  46280  xlimpnfvlem1  46282  xlimpnfv  46284  sinaover2ne0  46314  ioccncflimc  46331  icccncfext  46333  icocncflimc  46335  cncfiooicclem1  46339  cncfiooicc  46340  cncfiooiccre  46341  cncfioobdlem  46342  dvbdfbdioolem1  46374  dvbdfbdioolem2  46375  dvbdfbdioo  46376  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc1  46379  ioodvbdlimc2lem  46380  ioodvbdlimc2  46381  ditgeqiooicc  46406  iblsplit  46412  itgcoscmulx  46415  ibliooicc  46417  iblspltprt  46419  itgsincmulx  46420  itgsubsticc  46422  itgioocnicc  46423  iblcncfioo  46424  itgspltprt  46425  itgiccshift  46426  volioore  46436  voliooico  46438  voliooicof  46442  voliccico  46445  stoweidlem34  46480  stoweidlem52  46498  stirlinglem5  46524  dirkercncflem1  46549  dirkercncflem4  46552  fourierdlem4  46557  fourierdlem10  46563  fourierdlem19  46572  fourierdlem20  46573  fourierdlem24  46577  fourierdlem25  46578  fourierdlem26  46579  fourierdlem27  46580  fourierdlem28  46581  fourierdlem31  46584  fourierdlem32  46585  fourierdlem33  46586  fourierdlem35  46588  fourierdlem37  46590  fourierdlem40  46593  fourierdlem41  46594  fourierdlem43  46596  fourierdlem44  46597  fourierdlem46  46598  fourierdlem47  46599  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem52  46604  fourierdlem54  46606  fourierdlem57  46609  fourierdlem59  46611  fourierdlem60  46612  fourierdlem61  46613  fourierdlem62  46614  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem68  46620  fourierdlem69  46621  fourierdlem70  46622  fourierdlem72  46624  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem84  46636  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem93  46645  fourierdlem94  46646  fourierdlem97  46649  fourierdlem100  46652  fourierdlem101  46653  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem109  46661  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fourierdlem114  46666  sqwvfoura  46674  fouriersw  46677  etransclem23  46703  etransclem46  46726  qndenserrnbllem  46740  rrxsnicc  46746  ioorrnopnlem  46750  ioorrnopnxrlem  46752  salgencntex  46789  sge0cl  46827  sge0fsum  46833  sge0iunmptlemre  46861  sge0isum  46873  sge0ad2en  46877  sge0xaddlem1  46879  sge0xaddlem2  46880  sge0reuz  46893  voliunsge0lem  46918  meassre  46923  omessre  46956  omeiunltfirp  46965  hoissre  46990  hoiprodcl  46993  ovnsubaddlem1  47016  hoiprodcl3  47026  hoidmvcl  47028  hsphoidmvle2  47031  hsphoidmvle  47032  sge0hsphoire  47035  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  ovnhoilem1  47047  ovnhoilem2  47048  ovnhoi  47049  ovnlecvr2  47056  hspdifhsp  47062  hoidifhspdmvle  47066  hoiqssbllem1  47068  hoiqssbllem2  47069  hoiqssbllem3  47070  hspmbllem1  47072  hspmbllem2  47073  volicorege0  47083  ovolval5lem1  47098  ovolval5lem2  47099  iinhoiicclem  47119  iinhoiicc  47120  iunhoiioolem  47121  iunhoiioo  47122  vonioolem2  47127  vonicclem2  47130  vonsn  47137  pimltmnf2f  47143  pimconstlt0  47147  pimgtpnf2f  47151  salpreimagelt  47153  salpreimalegt  47155  preimageiingt  47166  preimaleiinlt  47167  pimrecltneg  47170  issmflem  47173  issmflelem  47190  issmfgtlem  47201  issmfgt  47202  smfaddlem1  47209  issmfgelem  47215  issmfge  47216  smfpimioompt  47232  smfresal  47234  smfrec  47235  smfmullem1  47237  smfmullem2  47238  smfmullem3  47239  smfmullem4  47240  smfpimbor1lem1  47244  smfsuplem1  47257  smflimsuplem4  47269  smfliminflem  47276  smfdmmblpimne  47283  smfpimne  47285  smfpimne2  47286  fsupdm  47288  finfdm  47292  smfinfdmmbllem  47294  bgoldbtbnd  48297  eenglngeehlnmlem2  49226