Theorem rexrd 11389

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11229  ℝ^*cxr 11372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-xr 11377

This theorem is used by:  xnn0xr  12714  rpxr  13160  rpxrd  13195  max0sub  13356  qextltlem  13362  xralrple  13365  xnegcl  13373  xaddf  13384  xnn0lem1lt  13404  xnn0lenn0nn0  13405  xmulf  13432  xadddi  13455  xrub  13472  supxrre  13487  infxrre  13497  ixxub  13527  ixxlb  13528  ioo0  13531  ico0  13552  ioc0  13553  iooshf  13587  icoshftf1o  13635  supicc  13662  supiccub  13663  supicclub  13664  xnn0xrge0  13667  ssfzunsn  13734  addmodid  14092  hashnnn0genn0  14517  hashunsnggt  14568  sgnsub  15291  sgnmul  15292  sgnmulsgn  15294  elicc4abs  15519  caucvgrlem  15872  fprodge1  16194  pcxcl  17071  pcdvdsb  17079  pcaddlem  17098  ramcl2lem  17219  ramlb  17229  0ram  17230  setsstruct  17386  prdsxmetlem  24720  xblss2ps  24753  xblss2  24754  blss2ps  24755  blss2  24756  blhalf  24757  metustto  24905  metustexhalf  24908  nmoi  25080  nmoix  25081  nmoi2  25082  nmoleub  25083  qdensere  25121  cnblcld  25126  ioo2blex  25146  tgioo  25148  blcvx  25150  zcld  25166  recld2  25167  iccntr  25174  icccmplem1  25175  reconnlem1  25179  reconnlem2  25180  opnreen  25184  metnrmlem3  25214  icoopnst  25293  iocopnst  25294  cnheibor  25309  lebnumii  25320  nmoleub2lem  25468  lmnn  25617  iscau3  25632  minveclem4  25786  ivthlem1  25805  ivthlem2  25806  ivthlem3  25807  ivth2  25809  ivthle  25810  ivthle2  25811  ivthicc  25812  evthicc  25813  cniccbdd  25815  ovolgelb  25834  ovollb2lem  25842  ovolunlem1  25851  ovoliunlem1  25856  ovoliunlem2  25857  ovoliun  25859  ovolscalem1  25867  ovolicc1  25870  ovolicc2lem4  25874  ovolicc2lem5  25875  ovolicc2  25876  ovolicc  25877  nulmbl2  25890  voliunlem2  25905  ioombl1lem4  25915  ioorcl2  25926  uniioombllem1  25935  uniioombllem2a  25936  uniioombllem3  25939  dyaddisjlem  25949  dyadmaxlem  25951  opnmbllem  25955  volivth  25961  vitalilem4  25965  mbfmulc2lem  26001  mbfmax  26003  mbfposr  26006  ismbf3d  26008  mbfaddlem  26014  mbflimsup  26020  mbfi1fseqlem4  26072  itg2lcl  26081  xrge0f  26085  itg2itg1  26090  itg2const2  26095  itg2seq  26096  itg2uba  26097  itg2lea  26098  itg2mulclem  26100  itg2mulc  26101  itg2splitlem  26102  itg2split  26103  itg2monolem2  26105  itg2monolem3  26106  itg2mono  26107  itg2gt0  26114  itg2cnlem1  26115  itg2cnlem2  26116  itg2cn  26117  iblss  26158  itgle  26163  itgeqa  26167  itgioo  26169  ibladdlem  26173  iblabs  26182  iblabsr  26183  iblmulc2  26184  itgsplit  26189  itgspliticc  26190  itgsplitioo  26191  bddmulibl  26192  bddiblnc  26195  ditgcl  26211  ditgswap  26212  ditgsplitlem  26213  dvferm1lem  26337  dvferm2lem  26339  dvferm  26341  rollelem  26342  rolle  26343  cmvth  26344  mvth  26345  dvlip  26346  dvlip2  26348  c1liplem1  26349  c1lip1  26350  dveq0  26353  dvgt0lem1  26355  dvivthlem1  26361  dvivth  26363  lhop1lem  26366  lhop1  26367  lhop2  26368  lhop  26369  dvcnvrelem1  26370  dvcnvre  26372  dvcvx  26373  dvfsumle  26374  dvfsumge  26375  dvfsumabs  26376  dvfsumlem2  26380  dvfsumlem3  26381  dvfsumlem4  26382  dvfsumrlimge0  26383  dvfsumrlim2  26385  ftc1lem1  26388  ftc1lem2  26389  ftc1a  26390  ftc1lem4  26392  ftc2  26397  ftc2ditglem  26398  itgparts  26400  itgsubstlem  26401  itgsubst  26402  itgpowd  26403  degltlem1  26423  deg1ge  26449  coe1mul3  26450  deg1sublt  26461  deg1mul2  26465  deg1tmle  26469  deg1tm  26470  idomrootle  26524  plypf1  26564  taylfvallem1  26717  tayl0  26722  pserulm  26782  psercnlem1  26785  pserdvlem1  26787  pserdvlem2  26788  abelthlem3  26793  abelth  26801  efcvx  26809  logno1  26997  logtayl  27021  xrlimcnp  27329  logfacbnd3  27583  log2sumbnd  27904  pntpbnd2  27947  pntibndlem3  27952  ttgcontlem1  29495  nmooge0  31402  nmoub3i  31408  isblo3i  31436  ubthlem1  31505  minvecolem4  31515  nmopge0  32546  nmfnge0  32562  nmophmi  32666  branmfn  32740  sgnval2  33400  nn0mnfxrd  33416  xaddeq0  33418  xlt2addrd  33424  sgnmulsgp  33496  xmulcand  33560  xreceu  33561  xdivrec  33566  fsumrp0cl  33658  xrge0slmod  33993  ply1degltel  34209  ply1degleel  34210  ply1degltlss  34211  ply1degltdimlem  34337  ply1degltdim  34338  fldextrspundgdvdslem  34395  extdgfialglem1  34407  cos9thpiminplylem2  34498  cnre2csqlem  34625  tpr2rico  34627  xrge0iifcnv  34648  xrge0iifhom  34652  lmxrge0  34667  esumfsup  34785  esumpcvgval  34793  esumcvg  34801  dya2iocress  34989  dya2iocbrsiga  34990  dya2icobrsiga  34991  dya2icoseg  34992  dya2iocucvr  34999  sxbrsigalem2  35001  omssubaddlem  35014  omssubadd  35015  orvcgteel  35183  dstrvprob  35187  orvclteel  35188  signstcl  35277  signstf  35278  signstf0  35280  signstfvn  35281  signsvtn0  35282  signsvfn  35294  signsvfpn  35297  signsvfnn  35298  ftc2re  35310  cvmliftlem6  36235  cvmliftlem7  36236  cvmliftlem8  36237  cvmliftlem9  36238  cvmliftlem10  36239  cvmliftlem13  36241  ivthALT  37314  iooelexlt  38490  relowlssretop  38491  relowlpssretop  38492  sin2h  38738  cos2h  38739  tan2h  38740  poimirlem30  38773  poimir  38776  heicant  38778  opnmbllem0  38779  mblfinlem1  38780  mblfinlem2  38781  mblfinlem3  38782  mblfinlem4  38783  ismblfin  38784  itg2addnclem  38794  itg2addnclem2  38795  itg2gt0cn  38798  ibladdnclem  38799  iblabsnclem  38806  iblabsnc  38807  iblmulc2nc  38808  ftc1cnnclem  38814  ftc1anclem1  38816  ftc1anclem4  38819  ftc1anclem5  38820  ftc1anclem6  38821  ftc1anclem7  38822  ftc1anclem8  38823  ftc1anc  38824  ftc2nc  38825  areacirclem1  38831  areacirclem5  38835  areacirc  38836  isbnd3  38921  blbnd  38924  prdsbnd  38930  prdsbnd2  38932  cntotbnd  38933  dvrelog3  43318  0nonelalab  43320  dvrelogpow2b  43321  dvle2  43325  aks4d1p1p6  43326  aks4d1p1p5  43328  aks6d1c6lem3  43425  aks6d1c7lem2  43434  unitscyglem5  43452  idomodle  44396  imo72b2  45375  cvgdvgrat  45500  radcnvrat  45501  rfcnpre3  46266  rfcnpre4  46267  absfico  46446  nnxrd  46505  lefldiveq  46523  lttri5d  46530  supxrgere  46560  supxrgelem  46564  supxrge  46565  xralrple2  46581  infxr  46593  infleinflem1  46596  infleinflem2  46597  xralrple4  46599  xralrple3  46600  xrralrecnnle  46609  xrralrecnnge  46616  supxrunb3  46625  unb2ltle  46640  zxrd  46678  gtnelioc  46718  ltnelicc  46724  iooabslt  46726  gtnelicc  46727  eliooshift  46733  iocopn  46747  eliccelioc  46748  iooshift  46749  icoopn  46752  ge0lere  46759  iooiinicc  46769  sqrlearg  46780  iooiinioc  46783  uzinico  46786  preimaiocmnf  46787  uzubioo  46792  fsumge0cl  46800  limciccioolb  46848  lptioo1  46859  limcicciooub  46862  ltmod  46863  lptre2pt  46865  limsupre  46866  limcresiooub  46867  limcresioolb  46868  limcleqr  46869  limsupresico  46925  limsuppnfdlem  46926  limsupub  46929  limsupequzlem  46947  limsupre2lem  46949  limsupre3lem  46957  limsupvaluz2  46963  supcnvlimsup  46965  liminfresico  46996  limsup10exlem  46997  liminflelimsuplem  47000  limsupgtlem  47002  liminfval4  47014  liminfvaluz2  47020  limsupvaluz4  47025  liminflimsupclim  47032  xlimxrre  47056  xlimmnfvlem1  47057  xlimmnfv  47059  xlimpnfvlem1  47061  xlimpnfv  47063  sinaover2ne0  47093  ioccncflimc  47110  icccncfext  47112  icocncflimc  47114  cncfiooicclem1  47118  cncfiooicc  47119  cncfiooiccre  47120  cncfioobdlem  47121  dvbdfbdioolem1  47153  dvbdfbdioolem2  47154  dvbdfbdioo  47155  ioodvbdlimc1lem1  47156  ioodvbdlimc1lem2  47157  ioodvbdlimc1  47158  ioodvbdlimc2lem  47159  ioodvbdlimc2  47160  ditgeqiooicc  47185  iblsplit  47191  itgcoscmulx  47194  ibliooicc  47196  iblspltprt  47198  itgsincmulx  47199  itgsubsticc  47201  itgioocnicc  47202  iblcncfioo  47203  itgspltprt  47204  itgiccshift  47205  volioore  47215  voliooico  47217  voliooicof  47221  voliccico  47224  stoweidlem34  47259  stoweidlem52  47277  stirlinglem5  47303  dirkercncflem1  47328  dirkercncflem4  47331  fourierdlem4  47336  fourierdlem10  47342  fourierdlem19  47351  fourierdlem20  47352  fourierdlem24  47356  fourierdlem25  47357  fourierdlem26  47358  fourierdlem27  47359  fourierdlem28  47360  fourierdlem31  47363  fourierdlem32  47364  fourierdlem33  47365  fourierdlem35  47367  fourierdlem37  47369  fourierdlem40  47372  fourierdlem41  47373  fourierdlem43  47375  fourierdlem44  47376  fourierdlem46  47377  fourierdlem47  47378  fourierdlem48  47379  fourierdlem49  47380  fourierdlem50  47381  fourierdlem51  47382  fourierdlem52  47383  fourierdlem54  47385  fourierdlem57  47388  fourierdlem59  47390  fourierdlem60  47391  fourierdlem61  47392  fourierdlem62  47393  fourierdlem63  47394  fourierdlem64  47395  fourierdlem65  47396  fourierdlem68  47399  fourierdlem69  47400  fourierdlem70  47401  fourierdlem72  47403  fourierdlem73  47404  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem78  47409  fourierdlem79  47410  fourierdlem81  47412  fourierdlem82  47413  fourierdlem84  47415  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem92  47423  fourierdlem93  47424  fourierdlem94  47425  fourierdlem97  47428  fourierdlem100  47431  fourierdlem101  47432  fourierdlem102  47433  fourierdlem103  47434  fourierdlem104  47435  fourierdlem107  47438  fourierdlem109  47440  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  fourierdlem114  47445  sqwvfoura  47453  fouriersw  47456  etransclem23  47482  etransclem46  47505  qndenserrnbllem  47519  rrxsnicc  47525  ioorrnopnlem  47529  ioorrnopnxrlem  47531  salgencntex  47568  sge0cl  47606  sge0fsum  47612  sge0iunmptlemre  47640  sge0isum  47652  sge0ad2en  47656  sge0xaddlem1  47658  sge0xaddlem2  47659  sge0reuz  47672  voliunsge0lem  47697  meassre  47702  omessre  47735  omeiunltfirp  47744  hoissre  47769  hoiprodcl  47772  ovnsubaddlem1  47795  hoiprodcl3  47805  hoidmvcl  47807  hsphoidmvle2  47810  hsphoidmvle  47811  sge0hsphoire  47814  hoidmv1lelem1  47816  hoidmv1lelem2  47817  hoidmv1lelem3  47818  hoidmv1le  47819  hoidmvlelem1  47820  hoidmvlelem2  47821  hoidmvlelem3  47822  hoidmvlelem4  47823  ovnhoilem1  47826  ovnhoilem2  47827  ovnhoi  47828  ovnlecvr2  47835  hspdifhsp  47841  hoidifhspdmvle  47845  hoiqssbllem1  47847  hoiqssbllem2  47848  hoiqssbllem3  47849  hspmbllem1  47851  hspmbllem2  47852  volicorege0  47862  ovolval5lem1  47877  ovolval5lem2  47878  iinhoiicclem  47898  iinhoiicc  47899  iunhoiioolem  47900  iunhoiioo  47901  vonioolem2  47906  vonicclem2  47909  vonsn  47916  pimltmnf2f  47922  pimconstlt0  47926  pimgtpnf2f  47930  salpreimagelt  47932  salpreimalegt  47934  preimageiingt  47945  preimaleiinlt  47946  pimrecltneg  47949  issmflem  47952  issmflelem  47969  issmfgtlem  47980  issmfgt  47981  smfaddlem1  47988  issmfgelem  47994  issmfge  47995  smfpimioompt  48011  smfresal  48013  smfrec  48014  smfmullem1  48016  smfmullem2  48017  smfmullem3  48018  smfmullem4  48019  smfpimbor1lem1  48023  smfsuplem1  48036  smflimsuplem4  48048  smfliminflem  48055  smfdmmblpimne  48062  smfpimne  48064  smfpimne2  48065  fsupdm  48067  finfdm  48071  smfinfdmmbllem  48073  bgoldbtbnd  49122  eenglngeehlnmlem2  50066