Theorem rexrd 11194

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ^*cxr 11177

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 3444  df-un 3908  df-ss 3920  df-xr 11182

This theorem is referenced by:  xnn0xr  12491  rpxr  12927  rpxrd  12962  max0sub  13123  qextltlem  13129  xralrple  13132  xnegcl  13140  xaddf  13151  xnn0lem1lt  13171  xnn0lenn0nn0  13172  xmulf  13199  xadddi  13222  xrub  13239  supxrre  13254  infxrre  13264  ixxub  13294  ixxlb  13295  ioo0  13298  ico0  13319  ioc0  13320  iooshf  13354  icoshftf1o  13402  supicc  13429  supiccub  13430  supicclub  13431  xnn0xrge0  13434  ssfzunsn  13498  addmodid  13854  hashnnn0genn0  14278  hashunsnggt  14329  elicc4abs  15255  caucvgrlem  15608  fprodge1  15930  pcxcl  16801  pcdvdsb  16809  pcaddlem  16828  ramcl2lem  16949  ramlb  16959  0ram  16960  setsstruct  17115  prdsxmetlem  24324  xblss2ps  24357  xblss2  24358  blss2ps  24359  blss2  24360  blhalf  24361  metustto  24509  metustexhalf  24512  nmoi  24684  nmoix  24685  nmoi2  24686  nmoleub  24687  qdensere  24725  cnblcld  24730  ioo2blex  24750  tgioo  24752  blcvx  24754  zcld  24770  recld2  24771  iccntr  24778  icccmplem1  24779  reconnlem1  24783  reconnlem2  24784  opnreen  24788  metnrmlem3  24818  icoopnst  24904  iocopnst  24905  cnheibor  24922  lebnumii  24933  nmoleub2lem  25082  lmnn  25231  iscau3  25246  minveclem4  25400  ivthlem1  25420  ivthlem2  25421  ivthlem3  25422  ivth2  25424  ivthle  25425  ivthle2  25426  ivthicc  25427  evthicc  25428  cniccbdd  25430  ovolgelb  25449  ovollb2lem  25457  ovolunlem1  25466  ovoliunlem1  25471  ovoliunlem2  25472  ovoliun  25474  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem4  25489  ovolicc2lem5  25490  ovolicc2  25491  ovolicc  25492  nulmbl2  25505  voliunlem2  25520  ioombl1lem4  25530  ioorcl2  25541  uniioombllem1  25550  uniioombllem2a  25551  uniioombllem3  25554  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  volivth  25576  vitalilem4  25580  mbfmulc2lem  25616  mbfmax  25618  mbfposr  25621  ismbf3d  25623  mbfaddlem  25629  mbflimsup  25635  mbfi1fseqlem4  25687  itg2lcl  25696  xrge0f  25700  itg2itg1  25705  itg2const2  25710  itg2seq  25711  itg2uba  25712  itg2lea  25713  itg2mulclem  25715  itg2mulc  25716  itg2splitlem  25717  itg2split  25718  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  itg2cn  25732  iblss  25774  itgle  25779  itgeqa  25783  itgioo  25785  ibladdlem  25789  iblabs  25798  iblabsr  25799  iblmulc2  25800  itgsplit  25805  itgspliticc  25806  itgsplitioo  25807  bddmulibl  25808  bddiblnc  25811  ditgcl  25827  ditgswap  25828  ditgsplitlem  25829  dvferm1lem  25956  dvferm2lem  25958  dvferm  25960  rollelem  25961  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlip2  25968  c1liplem1  25969  c1lip1  25970  dveq0  25973  dvgt0lem1  25975  dvivthlem1  25981  dvivth  25983  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  dvcnvrelem1  25990  dvcnvre  25992  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlimge0  26005  dvfsumrlim2  26007  ftc1lem1  26010  ftc1lem2  26011  ftc1a  26012  ftc1lem4  26014  ftc2  26019  ftc2ditglem  26020  itgparts  26022  itgsubstlem  26023  itgsubst  26024  itgpowd  26025  degltlem1  26045  deg1ge  26071  coe1mul3  26072  deg1sublt  26083  deg1mul2  26087  deg1tmle  26091  deg1tm  26092  idomrootle  26146  plypf1  26185  taylfvallem1  26332  tayl0  26337  pserulm  26399  psercnlem1  26403  pserdvlem1  26405  pserdvlem2  26406  abelthlem3  26411  abelth  26419  efcvx  26427  logno1  26613  logtayl  26637  xrlimcnp  26946  logfacbnd3  27202  log2sumbnd  27523  pntpbnd2  27566  pntibndlem3  27571  ttgcontlem1  28969  nmooge0  30854  nmoub3i  30860  isblo3i  30888  ubthlem1  30957  minvecolem4  30967  nmopge0  31998  nmfnge0  32014  nmophmi  32118  branmfn  32192  sgnval2  32824  nn0mnfxrd  32841  xaddeq0  32843  xlt2addrd  32849  sgnmul  32926  sgnsub  32928  sgnmulsgn  32933  sgnmulsgp  32934  xmulcand  33012  xreceu  33013  xdivrec  33018  fsumrp0cl  33113  xrge0slmod  33440  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  ply1degltdimlem  33799  ply1degltdim  33800  fldextrspundgdvdslem  33857  extdgfialglem1  33869  cos9thpiminplylem2  33960  cnre2csqlem  34087  tpr2rico  34089  xrge0iifcnv  34110  xrge0iifhom  34114  lmxrge0  34129  esumfsup  34247  esumpcvgval  34255  esumcvg  34263  dya2iocress  34451  dya2iocbrsiga  34452  dya2icobrsiga  34453  dya2icoseg  34454  dya2iocucvr  34461  sxbrsigalem2  34463  omssubaddlem  34476  omssubadd  34477  orvcgteel  34645  dstrvprob  34649  orvclteel  34650  signstcl  34742  signstf  34743  signstf0  34745  signstfvn  34746  signsvtn0  34747  signsvfn  34759  signsvfpn  34762  signsvfnn  34763  ftc2re  34775  cvmliftlem6  35503  cvmliftlem7  35504  cvmliftlem8  35505  cvmliftlem9  35506  cvmliftlem10  35507  cvmliftlem13  35509  ivthALT  36548  iooelexlt  37614  relowlssretop  37615  relowlpssretop  37616  sin2h  37858  cos2h  37859  tan2h  37860  poimirlem30  37898  poimir  37901  heicant  37903  opnmbllem0  37904  mblfinlem1  37905  mblfinlem2  37906  mblfinlem3  37907  mblfinlem4  37908  ismblfin  37909  itg2addnclem  37919  itg2addnclem2  37920  itg2gt0cn  37923  ibladdnclem  37924  iblabsnclem  37931  iblabsnc  37932  iblmulc2nc  37933  ftc1cnnclem  37939  ftc1anclem1  37941  ftc1anclem4  37944  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  ftc2nc  37950  areacirclem1  37956  areacirclem5  37960  areacirc  37961  isbnd3  38032  blbnd  38035  prdsbnd  38041  prdsbnd2  38043  cntotbnd  38044  dvrelog3  42432  0nonelalab  42434  dvrelogpow2b  42435  dvle2  42439  aks4d1p1p6  42440  aks4d1p1p5  42442  aks6d1c6lem3  42539  aks6d1c7lem2  42548  unitscyglem5  42566  idomodle  43545  imo72b2  44525  cvgdvgrat  44666  radcnvrat  44667  rfcnpre3  45390  rfcnpre4  45391  absfico  45573  nnxrd  45633  lefldiveq  45651  lttri5d  45658  supxrgere  45689  supxrgelem  45693  supxrge  45694  xralrple2  45710  infxr  45722  infleinflem1  45725  infleinflem2  45726  xralrple4  45728  xralrple3  45729  xrralrecnnle  45738  xrralrecnnge  45745  supxrunb3  45754  unb2ltle  45770  zxrd  45808  gtnelioc  45848  ltnelicc  45854  iooabslt  45856  gtnelicc  45857  eliooshift  45863  iocopn  45877  eliccelioc  45878  iooshift  45879  icoopn  45882  ge0lere  45889  iooiinicc  45899  sqrlearg  45910  iooiinioc  45913  uzinico  45916  preimaiocmnf  45917  uzubioo  45922  fsumge0cl  45930  limciccioolb  45978  lptioo1  45989  limcicciooub  45992  ltmod  45993  lptre2pt  45995  limsupre  45996  limcresiooub  45997  limcresioolb  45998  limcleqr  45999  limsupresico  46055  limsuppnfdlem  46056  limsupub  46059  limsupequzlem  46077  limsupre2lem  46079  limsupre3lem  46087  limsupvaluz2  46093  supcnvlimsup  46095  liminfresico  46126  limsup10exlem  46127  liminflelimsuplem  46130  limsupgtlem  46132  liminfval4  46144  liminfvaluz2  46150  limsupvaluz4  46155  liminflimsupclim  46162  xlimxrre  46186  xlimmnfvlem1  46187  xlimmnfv  46189  xlimpnfvlem1  46191  xlimpnfv  46193  sinaover2ne0  46223  ioccncflimc  46240  icccncfext  46242  icocncflimc  46244  cncfiooicclem1  46248  cncfiooicc  46249  cncfiooiccre  46250  cncfioobdlem  46251  dvbdfbdioolem1  46283  dvbdfbdioolem2  46284  dvbdfbdioo  46285  ioodvbdlimc1lem1  46286  ioodvbdlimc1lem2  46287  ioodvbdlimc1  46288  ioodvbdlimc2lem  46289  ioodvbdlimc2  46290  ditgeqiooicc  46315  iblsplit  46321  itgcoscmulx  46324  ibliooicc  46326  iblspltprt  46328  itgsincmulx  46329  itgsubsticc  46331  itgioocnicc  46332  iblcncfioo  46333  itgspltprt  46334  itgiccshift  46335  volioore  46345  voliooico  46347  voliooicof  46351  voliccico  46354  stoweidlem34  46389  stoweidlem52  46407  stirlinglem5  46433  dirkercncflem1  46458  dirkercncflem4  46461  fourierdlem4  46466  fourierdlem10  46472  fourierdlem19  46481  fourierdlem20  46482  fourierdlem24  46486  fourierdlem25  46487  fourierdlem26  46488  fourierdlem27  46489  fourierdlem28  46490  fourierdlem31  46493  fourierdlem32  46494  fourierdlem33  46495  fourierdlem35  46497  fourierdlem37  46499  fourierdlem40  46502  fourierdlem41  46503  fourierdlem43  46505  fourierdlem44  46506  fourierdlem46  46507  fourierdlem47  46508  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem51  46512  fourierdlem52  46513  fourierdlem54  46515  fourierdlem57  46518  fourierdlem59  46520  fourierdlem60  46521  fourierdlem61  46522  fourierdlem62  46523  fourierdlem63  46524  fourierdlem64  46525  fourierdlem65  46526  fourierdlem68  46529  fourierdlem69  46530  fourierdlem70  46531  fourierdlem72  46533  fourierdlem73  46534  fourierdlem74  46535  fourierdlem75  46536  fourierdlem76  46537  fourierdlem78  46539  fourierdlem79  46540  fourierdlem81  46542  fourierdlem82  46543  fourierdlem84  46545  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem92  46553  fourierdlem93  46554  fourierdlem94  46555  fourierdlem97  46558  fourierdlem100  46561  fourierdlem101  46562  fourierdlem102  46563  fourierdlem103  46564  fourierdlem104  46565  fourierdlem107  46568  fourierdlem109  46570  fourierdlem111  46572  fourierdlem112  46573  fourierdlem113  46574  fourierdlem114  46575  sqwvfoura  46583  fouriersw  46586  etransclem23  46612  etransclem46  46635  qndenserrnbllem  46649  rrxsnicc  46655  ioorrnopnlem  46659  ioorrnopnxrlem  46661  salgencntex  46698  sge0cl  46736  sge0fsum  46742  sge0iunmptlemre  46770  sge0isum  46782  sge0ad2en  46786  sge0xaddlem1  46788  sge0xaddlem2  46789  sge0reuz  46802  voliunsge0lem  46827  meassre  46832  omessre  46865  omeiunltfirp  46874  hoissre  46899  hoiprodcl  46902  ovnsubaddlem1  46925  hoiprodcl3  46935  hoidmvcl  46937  hsphoidmvle2  46940  hsphoidmvle  46941  sge0hsphoire  46944  hoidmv1lelem1  46946  hoidmv1lelem2  46947  hoidmv1lelem3  46948  hoidmv1le  46949  hoidmvlelem1  46950  hoidmvlelem2  46951  hoidmvlelem3  46952  hoidmvlelem4  46953  ovnhoilem1  46956  ovnhoilem2  46957  ovnhoi  46958  ovnlecvr2  46965  hspdifhsp  46971  hoidifhspdmvle  46975  hoiqssbllem1  46977  hoiqssbllem2  46978  hoiqssbllem3  46979  hspmbllem1  46981  hspmbllem2  46982  volicorege0  46992  ovolval5lem1  47007  ovolval5lem2  47008  iinhoiicclem  47028  iinhoiicc  47029  iunhoiioolem  47030  iunhoiioo  47031  vonioolem2  47036  vonicclem2  47039  vonsn  47046  pimltmnf2f  47052  pimconstlt0  47056  pimgtpnf2f  47060  salpreimagelt  47062  salpreimalegt  47064  preimageiingt  47075  preimaleiinlt  47076  pimrecltneg  47079  issmflem  47082  issmflelem  47099  issmfgtlem  47110  issmfgt  47111  smfaddlem1  47118  issmfgelem  47124  issmfge  47125  smfpimioompt  47141  smfresal  47143  smfrec  47144  smfmullem1  47146  smfmullem2  47147  smfmullem3  47148  smfmullem4  47149  smfpimbor1lem1  47153  smfsuplem1  47166  smflimsuplem4  47178  smfliminflem  47185  smfdmmblpimne  47192  smfpimne  47194  smfpimne2  47195  fsupdm  47197  finfdm  47201  smfinfdmmbllem  47203  bgoldbtbnd  48166  eenglngeehlnmlem2  49095