Theorem rexrd 10680

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 10525  ℝ^*cxr 10663

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-xr 10668

This theorem is referenced by:  xnn0xr  11960  rpxr  12386  rpxrd  12420  max0sub  12577  qextltlem  12583  xralrple  12586  xnegcl  12594  xaddf  12605  xnn0lem1lt  12625  xnn0lenn0nn0  12626  xmulf  12653  xadddi  12676  xrub  12693  supxrre  12708  infxrre  12717  ixxub  12747  ixxlb  12748  ioo0  12751  ico0  12772  ioc0  12773  iooshf  12804  icoshftf1o  12852  supicc  12879  supiccub  12880  supicclub  12881  xnn0xrge0  12884  ssfzunsn  12948  addmodid  13282  hashnnn0genn0  13699  hashunsnggt  13751  elicc4abs  14671  caucvgrlem  15021  fprodge1  15341  pcxcl  16187  pcdvdsb  16195  pcaddlem  16214  ramcl2lem  16335  ramlb  16345  0ram  16346  setsstruct  16515  prdsxmetlem  22975  xblss2ps  23008  xblss2  23009  blss2ps  23010  blss2  23011  blhalf  23012  metustto  23160  metustexhalf  23163  nmoi  23334  nmoix  23335  nmoi2  23336  nmoleub  23337  qdensere  23375  cnblcld  23380  ioo2blex  23399  tgioo  23401  blcvx  23403  zcld  23418  recld2  23419  iccntr  23426  icccmplem1  23427  reconnlem1  23431  reconnlem2  23432  opnreen  23436  metnrmlem3  23466  icoopnst  23544  iocopnst  23545  cnheibor  23560  lebnumii  23571  nmoleub2lem  23719  lmnn  23867  iscau3  23882  minveclem4  24036  ivthlem1  24055  ivthlem2  24056  ivthlem3  24057  ivth2  24059  ivthle  24060  ivthle2  24061  ivthicc  24062  evthicc  24063  cniccbdd  24065  ovolgelb  24084  ovollb2lem  24092  ovolunlem1  24101  ovoliunlem1  24106  ovoliunlem2  24107  ovoliun  24109  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem4  24124  ovolicc2lem5  24125  ovolicc2  24126  ovolicc  24127  nulmbl2  24140  voliunlem2  24155  ioombl1lem4  24165  ioorcl2  24176  uniioombllem1  24185  uniioombllem2a  24186  uniioombllem3  24189  dyaddisjlem  24199  dyadmaxlem  24201  opnmbllem  24205  volivth  24211  vitalilem4  24215  mbfmulc2lem  24251  mbfmax  24253  mbfposr  24256  ismbf3d  24258  mbfaddlem  24264  mbflimsup  24270  mbfi1fseqlem4  24322  itg2lcl  24331  xrge0f  24335  itg2itg1  24340  itg2const2  24345  itg2seq  24346  itg2uba  24347  itg2lea  24348  itg2mulclem  24350  itg2mulc  24351  itg2splitlem  24352  itg2split  24353  itg2monolem2  24355  itg2monolem3  24356  itg2mono  24357  itg2gt0  24364  itg2cnlem1  24365  itg2cnlem2  24366  itg2cn  24367  iblss  24408  itgle  24413  itgeqa  24417  itgioo  24419  ibladdlem  24423  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgsplit  24439  itgspliticc  24440  itgsplitioo  24441  bddmulibl  24442  bddiblnc  24445  ditgcl  24461  ditgswap  24462  ditgsplitlem  24463  dvferm1lem  24587  dvferm2lem  24589  dvferm  24591  rollelem  24592  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  dvlip2  24598  c1liplem1  24599  c1lip1  24600  dveq0  24603  dvgt0lem1  24605  dvivthlem1  24611  dvivth  24613  lhop1lem  24616  lhop1  24617  lhop2  24618  lhop  24619  dvcnvrelem1  24620  dvcnvre  24622  dvcvx  24623  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumlem4  24632  dvfsumrlimge0  24633  dvfsumrlim2  24635  ftc1lem1  24638  ftc1lem2  24639  ftc1a  24640  ftc1lem4  24642  ftc2  24647  ftc2ditglem  24648  itgparts  24650  itgsubstlem  24651  itgsubst  24652  itgpowd  24653  degltlem1  24673  deg1ge  24699  coe1mul3  24700  deg1sublt  24711  deg1mul2  24715  deg1tmle  24718  deg1tm  24719  plypf1  24809  taylfvallem1  24952  tayl0  24957  pserulm  25017  psercnlem1  25020  pserdvlem1  25022  pserdvlem2  25023  abelthlem3  25028  abelth  25036  efcvx  25044  logno1  25227  logtayl  25251  xrlimcnp  25554  logfacbnd3  25807  log2sumbnd  26128  pntpbnd2  26171  pntibndlem3  26176  ttgcontlem1  26679  nmooge0  28550  nmoub3i  28556  isblo3i  28584  ubthlem1  28653  minvecolem4  28663  nmopge0  29694  nmfnge0  29710  nmophmi  29814  branmfn  29888  xaddeq0  30503  xlt2addrd  30508  xmulcand  30623  xreceu  30624  xdivrec  30629  fsumrp0cl  30729  xrge0slmod  30968  cnre2csqlem  31263  tpr2rico  31265  xrge0iifcnv  31286  xrge0iifhom  31290  lmxrge0  31305  esumfsup  31439  esumpcvgval  31447  esumcvg  31455  dya2iocress  31642  dya2iocbrsiga  31643  dya2icobrsiga  31644  dya2icoseg  31645  dya2iocucvr  31652  sxbrsigalem2  31654  omssubaddlem  31667  omssubadd  31668  orvcgteel  31835  dstrvprob  31839  orvclteel  31840  sgnmul  31910  sgnsub  31912  sgnmulsgn  31917  sgnmulsgp  31918  signstcl  31945  signstf  31946  signstf0  31948  signstfvn  31949  signsvtn0  31950  signsvfn  31962  signsvfpn  31965  signsvfnn  31966  ftc2re  31979  cvmliftlem6  32650  cvmliftlem7  32651  cvmliftlem8  32652  cvmliftlem9  32653  cvmliftlem10  32654  cvmliftlem13  32656  ivthALT  33796  iooelexlt  34779  relowlssretop  34780  relowlpssretop  34781  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem30  35087  poimir  35090  heicant  35092  opnmbllem0  35093  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2addnclem  35108  itg2addnclem2  35109  itg2gt0cn  35112  ibladdnclem  35113  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  ftc1cnnclem  35128  ftc1anclem1  35130  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  ftc2nc  35139  areacirclem1  35145  areacirclem5  35149  areacirc  35150  isbnd3  35222  blbnd  35225  prdsbnd  35231  prdsbnd2  35233  cntotbnd  35234  idomrootle  40139  idomodle  40140  imo72b2  40878  cvgdvgrat  41017  radcnvrat  41018  rfcnpre3  41662  rfcnpre4  41663  nnxrd  41671  absfico  41847  lefldiveq  41924  lttri5d  41931  supxrgere  41965  supxrgelem  41969  supxrge  41970  xralrple2  41986  infxr  41999  infleinflem1  42002  infleinflem2  42003  xralrple4  42005  xralrple3  42006  xrralrecnnle  42017  xrralrecnnge  42026  supxrunb3  42036  unb2ltle  42052  zxrd  42092  gtnelioc  42128  ltnelicc  42134  iooabslt  42136  gtnelicc  42137  eliooshift  42143  iocopn  42157  eliccelioc  42158  iooshift  42159  icoopn  42162  ge0lere  42169  iooiinicc  42179  sqrlearg  42190  iooiinioc  42193  uzinico  42197  preimaiocmnf  42198  uzubioo  42204  fsumge0cl  42215  limciccioolb  42263  lptioo1  42274  limcicciooub  42279  ltmod  42280  lptre2pt  42282  limsupre  42283  limcresiooub  42284  limcresioolb  42285  limcleqr  42286  limsupresico  42342  limsuppnfdlem  42343  limsupub  42346  limsupequzlem  42364  limsupre2lem  42366  limsupre3lem  42374  limsupvaluz2  42380  supcnvlimsup  42382  liminfresico  42413  limsup10exlem  42414  liminflelimsuplem  42417  limsupgtlem  42419  liminfval4  42431  liminfvaluz2  42437  limsupvaluz4  42442  liminflimsupclim  42449  xlimxrre  42473  xlimmnfvlem1  42474  xlimmnfv  42476  xlimpnfvlem1  42478  xlimpnfv  42480  sinaover2ne0  42510  ioccncflimc  42527  icccncfext  42529  icocncflimc  42531  cncfiooicclem1  42535  cncfiooicc  42536  cncfiooiccre  42537  cncfioobdlem  42538  dvbdfbdioolem1  42570  dvbdfbdioolem2  42571  dvbdfbdioo  42572  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc1  42575  ioodvbdlimc2lem  42576  ioodvbdlimc2  42577  ditgeqiooicc  42602  iblsplit  42608  itgcoscmulx  42611  ibliooicc  42613  iblspltprt  42615  itgsincmulx  42616  itgsubsticc  42618  itgioocnicc  42619  iblcncfioo  42620  itgspltprt  42621  itgiccshift  42622  volioore  42632  voliooico  42634  voliooicof  42638  voliccico  42641  stoweidlem34  42676  stoweidlem52  42694  stirlinglem5  42720  dirkercncflem1  42745  dirkercncflem4  42748  fourierdlem4  42753  fourierdlem10  42759  fourierdlem19  42768  fourierdlem20  42769  fourierdlem24  42773  fourierdlem25  42774  fourierdlem26  42775  fourierdlem27  42776  fourierdlem28  42777  fourierdlem31  42780  fourierdlem32  42781  fourierdlem33  42782  fourierdlem35  42784  fourierdlem37  42786  fourierdlem40  42789  fourierdlem41  42790  fourierdlem43  42792  fourierdlem44  42793  fourierdlem46  42794  fourierdlem47  42795  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem52  42800  fourierdlem54  42802  fourierdlem57  42805  fourierdlem59  42807  fourierdlem60  42808  fourierdlem61  42809  fourierdlem62  42810  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem68  42816  fourierdlem69  42817  fourierdlem70  42818  fourierdlem72  42820  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem84  42832  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem92  42840  fourierdlem93  42841  fourierdlem94  42842  fourierdlem97  42845  fourierdlem100  42848  fourierdlem101  42849  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem107  42855  fourierdlem109  42857  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fourierdlem114  42862  sqwvfoura  42870  fouriersw  42873  etransclem23  42899  etransclem46  42922  qndenserrnbllem  42936  rrxsnicc  42942  ioorrnopnlem  42946  ioorrnopnxrlem  42948  salgencntex  42983  sge0cl  43020  sge0fsum  43026  sge0iunmptlemre  43054  sge0isum  43066  sge0ad2en  43070  sge0xaddlem1  43072  sge0xaddlem2  43073  sge0reuz  43086  voliunsge0lem  43111  meassre  43116  omessre  43149  omeiunltfirp  43158  hoissre  43183  hoiprodcl  43186  ovnsubaddlem1  43209  hoiprodcl3  43219  hoidmvcl  43221  hsphoidmvle2  43224  hsphoidmvle  43225  sge0hsphoire  43228  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  ovnhoilem1  43240  ovnhoilem2  43241  ovnhoi  43242  ovnlecvr2  43249  hspdifhsp  43255  hoidifhspdmvle  43259  hoiqssbllem1  43261  hoiqssbllem2  43262  hoiqssbllem3  43263  hspmbllem1  43265  hspmbllem2  43266  volicorege0  43276  ovolval5lem1  43291  ovolval5lem2  43292  iinhoiicclem  43312  iinhoiicc  43313  iunhoiioolem  43314  iunhoiioo  43315  vonioolem2  43320  vonicclem2  43323  vonsn  43330  pimltmnf2  43336  pimconstlt0  43339  pimgtpnf2  43342  salpreimagelt  43343  salpreimalegt  43345  preimageiingt  43355  preimaleiinlt  43356  pimrecltneg  43358  issmflem  43361  issmflelem  43378  issmfgtlem  43389  issmfgt  43390  smfaddlem1  43396  issmfgelem  43402  issmfge  43403  smfpimioompt  43418  smfresal  43420  smfrec  43421  smfmullem1  43423  smfmullem2  43424  smfmullem3  43425  smfmullem4  43426  smfpimbor1lem1  43430  smfsuplem1  43442  smflimsuplem4  43454  smfliminflem  43461  bgoldbtbnd  44327  eenglngeehlnmlem2  45152