Theorem rexrd 11261

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11106  ℝ^*cxr 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-in 3955  df-ss 3965  df-xr 11249

This theorem is referenced by:  xnn0xr  12546  rpxr  12980  rpxrd  13014  max0sub  13172  qextltlem  13178  xralrple  13181  xnegcl  13189  xaddf  13200  xnn0lem1lt  13220  xnn0lenn0nn0  13221  xmulf  13248  xadddi  13271  xrub  13288  supxrre  13303  infxrre  13312  ixxub  13342  ixxlb  13343  ioo0  13346  ico0  13367  ioc0  13368  iooshf  13400  icoshftf1o  13448  supicc  13475  supiccub  13476  supicclub  13477  xnn0xrge0  13480  ssfzunsn  13544  addmodid  13881  hashnnn0genn0  14300  hashunsnggt  14351  elicc4abs  15263  caucvgrlem  15616  fprodge1  15936  pcxcl  16791  pcdvdsb  16799  pcaddlem  16818  ramcl2lem  16939  ramlb  16949  0ram  16950  setsstruct  17106  prdsxmetlem  23866  xblss2ps  23899  xblss2  23900  blss2ps  23901  blss2  23902  blhalf  23903  metustto  24054  metustexhalf  24057  nmoi  24237  nmoix  24238  nmoi2  24239  nmoleub  24240  qdensere  24278  cnblcld  24283  ioo2blex  24302  tgioo  24304  blcvx  24306  zcld  24321  recld2  24322  iccntr  24329  icccmplem1  24330  reconnlem1  24334  reconnlem2  24335  opnreen  24339  metnrmlem3  24369  icoopnst  24447  iocopnst  24448  cnheibor  24463  lebnumii  24474  nmoleub2lem  24622  lmnn  24772  iscau3  24787  minveclem4  24941  ivthlem1  24960  ivthlem2  24961  ivthlem3  24962  ivth2  24964  ivthle  24965  ivthle2  24966  ivthicc  24967  evthicc  24968  cniccbdd  24970  ovolgelb  24989  ovollb2lem  24997  ovolunlem1  25006  ovoliunlem1  25011  ovoliunlem2  25012  ovoliun  25014  ovolscalem1  25022  ovolicc1  25025  ovolicc2lem4  25029  ovolicc2lem5  25030  ovolicc2  25031  ovolicc  25032  nulmbl2  25045  voliunlem2  25060  ioombl1lem4  25070  ioorcl2  25081  uniioombllem1  25090  uniioombllem2a  25091  uniioombllem3  25094  dyaddisjlem  25104  dyadmaxlem  25106  opnmbllem  25110  volivth  25116  vitalilem4  25120  mbfmulc2lem  25156  mbfmax  25158  mbfposr  25161  ismbf3d  25163  mbfaddlem  25169  mbflimsup  25175  mbfi1fseqlem4  25228  itg2lcl  25237  xrge0f  25241  itg2itg1  25246  itg2const2  25251  itg2seq  25252  itg2uba  25253  itg2lea  25254  itg2mulclem  25256  itg2mulc  25257  itg2splitlem  25258  itg2split  25259  itg2monolem2  25261  itg2monolem3  25262  itg2mono  25263  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  itg2cn  25273  iblss  25314  itgle  25319  itgeqa  25323  itgioo  25325  ibladdlem  25329  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgsplit  25345  itgspliticc  25346  itgsplitioo  25347  bddmulibl  25348  bddiblnc  25351  ditgcl  25367  ditgswap  25368  ditgsplitlem  25369  dvferm1lem  25493  dvferm2lem  25495  dvferm  25497  rollelem  25498  rolle  25499  cmvth  25500  mvth  25501  dvlip  25502  dvlip2  25504  c1liplem1  25505  c1lip1  25506  dveq0  25509  dvgt0lem1  25511  dvivthlem1  25517  dvivth  25519  lhop1lem  25522  lhop1  25523  lhop2  25524  lhop  25525  dvcnvrelem1  25526  dvcnvre  25528  dvcvx  25529  dvfsumle  25530  dvfsumge  25531  dvfsumabs  25532  dvfsumlem2  25536  dvfsumlem3  25537  dvfsumlem4  25538  dvfsumrlimge0  25539  dvfsumrlim2  25541  ftc1lem1  25544  ftc1lem2  25545  ftc1a  25546  ftc1lem4  25548  ftc2  25553  ftc2ditglem  25554  itgparts  25556  itgsubstlem  25557  itgsubst  25558  itgpowd  25559  degltlem1  25582  deg1ge  25608  coe1mul3  25609  deg1sublt  25620  deg1mul2  25624  deg1tmle  25627  deg1tm  25628  plypf1  25718  taylfvallem1  25861  tayl0  25866  pserulm  25926  psercnlem1  25929  pserdvlem1  25931  pserdvlem2  25932  abelthlem3  25937  abelth  25945  efcvx  25953  logno1  26136  logtayl  26160  xrlimcnp  26463  logfacbnd3  26716  log2sumbnd  27037  pntpbnd2  27080  pntibndlem3  27085  ttgcontlem1  28132  nmooge0  30008  nmoub3i  30014  isblo3i  30042  ubthlem1  30111  minvecolem4  30121  nmopge0  31152  nmfnge0  31168  nmophmi  31272  branmfn  31346  xaddeq0  31954  xlt2addrd  31959  xmulcand  32075  xreceu  32076  xdivrec  32081  fsumrp0cl  32184  xrge0slmod  32452  ply1degltel  32655  ply1degltlss  32656  ply1degltdimlem  32696  ply1degltdim  32697  cnre2csqlem  32879  tpr2rico  32881  xrge0iifcnv  32902  xrge0iifhom  32906  lmxrge0  32921  esumfsup  33057  esumpcvgval  33065  esumcvg  33073  dya2iocress  33262  dya2iocbrsiga  33263  dya2icobrsiga  33264  dya2icoseg  33265  dya2iocucvr  33272  sxbrsigalem2  33274  omssubaddlem  33287  omssubadd  33288  orvcgteel  33455  dstrvprob  33459  orvclteel  33460  sgnmul  33530  sgnsub  33532  sgnmulsgn  33537  sgnmulsgp  33538  signstcl  33565  signstf  33566  signstf0  33568  signstfvn  33569  signsvtn0  33570  signsvfn  33582  signsvfpn  33585  signsvfnn  33586  ftc2re  33599  cvmliftlem6  34270  cvmliftlem7  34271  cvmliftlem8  34272  cvmliftlem9  34273  cvmliftlem10  34274  cvmliftlem13  34276  gg-cmvth  35170  gg-dvfsumle  35171  gg-dvfsumlem2  35172  ivthALT  35209  iooelexlt  36232  relowlssretop  36233  relowlpssretop  36234  sin2h  36467  cos2h  36468  tan2h  36469  poimirlem30  36507  poimir  36510  heicant  36512  opnmbllem0  36513  mblfinlem1  36514  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem  36528  itg2addnclem2  36529  itg2gt0cn  36532  ibladdnclem  36533  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  ftc1cnnclem  36548  ftc1anclem1  36550  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  ftc2nc  36559  areacirclem1  36565  areacirclem5  36569  areacirc  36570  isbnd3  36641  blbnd  36644  prdsbnd  36650  prdsbnd2  36652  cntotbnd  36653  dvrelog3  40919  0nonelalab  40921  dvrelogpow2b  40922  dvle2  40926  aks4d1p1p6  40927  aks4d1p1p5  40929  idomrootle  41923  idomodle  41924  imo72b2  42910  cvgdvgrat  43058  radcnvrat  43059  rfcnpre3  43703  rfcnpre4  43704  absfico  43903  nnxrd  43970  lefldiveq  43989  lttri5d  43996  supxrgere  44030  supxrgelem  44034  supxrge  44035  xralrple2  44051  infxr  44064  infleinflem1  44067  infleinflem2  44068  xralrple4  44070  xralrple3  44071  xrralrecnnle  44080  xrralrecnnge  44087  supxrunb3  44096  unb2ltle  44112  zxrd  44150  gtnelioc  44191  ltnelicc  44197  iooabslt  44199  gtnelicc  44200  eliooshift  44206  iocopn  44220  eliccelioc  44221  iooshift  44222  icoopn  44225  ge0lere  44232  iooiinicc  44242  sqrlearg  44253  iooiinioc  44256  uzinico  44260  preimaiocmnf  44261  uzubioo  44267  fsumge0cl  44276  limciccioolb  44324  lptioo1  44335  limcicciooub  44340  ltmod  44341  lptre2pt  44343  limsupre  44344  limcresiooub  44345  limcresioolb  44346  limcleqr  44347  limsupresico  44403  limsuppnfdlem  44404  limsupub  44407  limsupequzlem  44425  limsupre2lem  44427  limsupre3lem  44435  limsupvaluz2  44441  supcnvlimsup  44443  liminfresico  44474  limsup10exlem  44475  liminflelimsuplem  44478  limsupgtlem  44480  liminfval4  44492  liminfvaluz2  44498  limsupvaluz4  44503  liminflimsupclim  44510  xlimxrre  44534  xlimmnfvlem1  44535  xlimmnfv  44537  xlimpnfvlem1  44539  xlimpnfv  44541  sinaover2ne0  44571  ioccncflimc  44588  icccncfext  44590  icocncflimc  44592  cncfiooicclem1  44596  cncfiooicc  44597  cncfiooiccre  44598  cncfioobdlem  44599  dvbdfbdioolem1  44631  dvbdfbdioolem2  44632  dvbdfbdioo  44633  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc1  44636  ioodvbdlimc2lem  44637  ioodvbdlimc2  44638  ditgeqiooicc  44663  iblsplit  44669  itgcoscmulx  44672  ibliooicc  44674  iblspltprt  44676  itgsincmulx  44677  itgsubsticc  44679  itgioocnicc  44680  iblcncfioo  44681  itgspltprt  44682  itgiccshift  44683  volioore  44693  voliooico  44695  voliooicof  44699  voliccico  44702  stoweidlem34  44737  stoweidlem52  44755  stirlinglem5  44781  dirkercncflem1  44806  dirkercncflem4  44809  fourierdlem4  44814  fourierdlem10  44820  fourierdlem19  44829  fourierdlem20  44830  fourierdlem24  44834  fourierdlem25  44835  fourierdlem26  44836  fourierdlem27  44837  fourierdlem28  44838  fourierdlem31  44841  fourierdlem32  44842  fourierdlem33  44843  fourierdlem35  44845  fourierdlem37  44847  fourierdlem40  44850  fourierdlem41  44851  fourierdlem43  44853  fourierdlem44  44854  fourierdlem46  44855  fourierdlem47  44856  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem51  44860  fourierdlem52  44861  fourierdlem54  44863  fourierdlem57  44866  fourierdlem59  44868  fourierdlem60  44869  fourierdlem61  44870  fourierdlem62  44871  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem68  44877  fourierdlem69  44878  fourierdlem70  44879  fourierdlem72  44881  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem78  44887  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem84  44893  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem92  44901  fourierdlem93  44902  fourierdlem94  44903  fourierdlem97  44906  fourierdlem100  44909  fourierdlem101  44910  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem107  44916  fourierdlem109  44918  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  fourierdlem114  44923  sqwvfoura  44931  fouriersw  44934  etransclem23  44960  etransclem46  44983  qndenserrnbllem  44997  rrxsnicc  45003  ioorrnopnlem  45007  ioorrnopnxrlem  45009  salgencntex  45046  sge0cl  45084  sge0fsum  45090  sge0iunmptlemre  45118  sge0isum  45130  sge0ad2en  45134  sge0xaddlem1  45136  sge0xaddlem2  45137  sge0reuz  45150  voliunsge0lem  45175  meassre  45180  omessre  45213  omeiunltfirp  45222  hoissre  45247  hoiprodcl  45250  ovnsubaddlem1  45273  hoiprodcl3  45283  hoidmvcl  45285  hsphoidmvle2  45288  hsphoidmvle  45289  sge0hsphoire  45292  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1lelem3  45296  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  ovnhoilem1  45304  ovnhoilem2  45305  ovnhoi  45306  ovnlecvr2  45313  hspdifhsp  45319  hoidifhspdmvle  45323  hoiqssbllem1  45325  hoiqssbllem2  45326  hoiqssbllem3  45327  hspmbllem1  45329  hspmbllem2  45330  volicorege0  45340  ovolval5lem1  45355  ovolval5lem2  45356  iinhoiicclem  45376  iinhoiicc  45377  iunhoiioolem  45378  iunhoiioo  45379  vonioolem2  45384  vonicclem2  45387  vonsn  45394  pimltmnf2f  45400  pimconstlt0  45404  pimgtpnf2f  45408  salpreimagelt  45410  salpreimalegt  45412  preimageiingt  45423  preimaleiinlt  45424  pimrecltneg  45427  issmflem  45430  issmflelem  45447  issmfgtlem  45458  issmfgt  45459  smfaddlem1  45466  issmfgelem  45472  issmfge  45473  smfpimioompt  45489  smfresal  45491  smfrec  45492  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  smfmullem4  45497  smfpimbor1lem1  45501  smfsuplem1  45514  smflimsuplem4  45526  smfliminflem  45533  smfdmmblpimne  45540  smfpimne  45542  smfpimne2  45543  fsupdm  45545  finfdm  45549  smfinfdmmbllem  45551  bgoldbtbnd  46464  eenglngeehlnmlem2  47378