Theorem rexrd 10691

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  ℝ^*cxr 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679

This theorem is referenced by:  xnn0xr  11973  rpxr  12399  rpxrd  12433  max0sub  12590  qextltlem  12596  xralrple  12599  xnegcl  12607  xaddf  12618  xnn0lem1lt  12638  xnn0lenn0nn0  12639  xmulf  12666  xadddi  12689  xrub  12706  supxrre  12721  infxrre  12730  ixxub  12760  ixxlb  12761  ioo0  12764  ico0  12785  ioc0  12786  iooshf  12816  icoshftf1o  12861  supicc  12887  supiccub  12888  supicclub  12889  xnn0xrge0  12892  ssfzunsn  12954  addmodid  13288  hashnnn0genn0  13704  hashunsnggt  13756  elicc4abs  14679  caucvgrlem  15029  fprodge1  15349  pcxcl  16197  pcdvdsb  16205  pcaddlem  16224  ramcl2lem  16345  ramlb  16355  0ram  16356  setsstruct  16523  prdsxmetlem  22978  xblss2ps  23011  xblss2  23012  blss2ps  23013  blss2  23014  blhalf  23015  metustto  23163  metustexhalf  23166  nmoi  23337  nmoix  23338  nmoi2  23339  nmoleub  23340  qdensere  23378  cnblcld  23383  ioo2blex  23402  tgioo  23404  blcvx  23406  zcld  23421  recld2  23422  iccntr  23429  icccmplem1  23430  reconnlem1  23434  reconnlem2  23435  opnreen  23439  metnrmlem3  23469  icoopnst  23543  iocopnst  23544  cnheibor  23559  lebnumii  23570  nmoleub2lem  23718  lmnn  23866  iscau3  23881  minveclem4  24035  ivthlem1  24052  ivthlem2  24053  ivthlem3  24054  ivth2  24056  ivthle  24057  ivthle2  24058  ivthicc  24059  evthicc  24060  cniccbdd  24062  ovolgelb  24081  ovollb2lem  24089  ovolunlem1  24098  ovoliunlem1  24103  ovoliunlem2  24104  ovoliun  24106  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem4  24121  ovolicc2lem5  24122  ovolicc2  24123  ovolicc  24124  nulmbl2  24137  voliunlem2  24152  ioombl1lem4  24162  ioorcl2  24173  uniioombllem1  24182  uniioombllem2a  24183  uniioombllem3  24186  dyaddisjlem  24196  dyadmaxlem  24198  opnmbllem  24202  volivth  24208  vitalilem4  24212  mbfmulc2lem  24248  mbfmax  24250  mbfposr  24253  ismbf3d  24255  mbfaddlem  24261  mbflimsup  24267  mbfi1fseqlem4  24319  itg2lcl  24328  xrge0f  24332  itg2itg1  24337  itg2const2  24342  itg2seq  24343  itg2uba  24344  itg2lea  24345  itg2mulclem  24347  itg2mulc  24348  itg2splitlem  24349  itg2split  24350  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  itg2cn  24364  iblss  24405  itgle  24410  itgeqa  24414  itgioo  24416  ibladdlem  24420  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgsplit  24436  itgspliticc  24437  itgsplitioo  24438  bddmulibl  24439  ditgcl  24456  ditgswap  24457  ditgsplitlem  24458  dvferm1lem  24581  dvferm2lem  24583  dvferm  24585  rollelem  24586  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlip2  24592  c1liplem1  24593  c1lip1  24594  dveq0  24597  dvgt0lem1  24599  dvivthlem1  24605  dvivth  24607  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  dvcnvrelem1  24614  dvcnvre  24616  dvcvx  24617  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlimge0  24627  dvfsumrlim2  24629  ftc1lem1  24632  ftc1lem2  24633  ftc1a  24634  ftc1lem4  24636  ftc2  24641  ftc2ditglem  24642  itgparts  24644  itgsubstlem  24645  itgsubst  24646  degltlem1  24666  deg1ge  24692  coe1mul3  24693  deg1sublt  24704  deg1mul2  24708  deg1tmle  24711  deg1tm  24712  plypf1  24802  taylfvallem1  24945  tayl0  24950  pserulm  25010  psercnlem1  25013  pserdvlem1  25015  pserdvlem2  25016  abelthlem3  25021  abelth  25029  efcvx  25037  logno1  25219  logtayl  25243  xrlimcnp  25546  logfacbnd3  25799  log2sumbnd  26120  pntpbnd2  26163  pntibndlem3  26168  ttgcontlem1  26671  nmooge0  28544  nmoub3i  28550  isblo3i  28578  ubthlem1  28647  minvecolem4  28657  nmopge0  29688  nmfnge0  29704  nmophmi  29808  branmfn  29882  xaddeq0  30477  xlt2addrd  30482  xmulcand  30597  xreceu  30598  xdivrec  30603  fsumrp0cl  30682  xrge0slmod  30917  cnre2csqlem  31153  tpr2rico  31155  xrge0iifcnv  31176  xrge0iifhom  31180  lmxrge0  31195  esumfsup  31329  esumpcvgval  31337  esumcvg  31345  dya2iocress  31532  dya2iocbrsiga  31533  dya2icobrsiga  31534  dya2icoseg  31535  dya2iocucvr  31542  sxbrsigalem2  31544  omssubaddlem  31557  omssubadd  31558  orvcgteel  31725  dstrvprob  31729  orvclteel  31730  sgnmul  31800  sgnsub  31802  sgnmulsgn  31807  sgnmulsgp  31808  signstcl  31835  signstf  31836  signstf0  31838  signstfvn  31839  signsvtn0  31840  signsvfn  31852  signsvfpn  31855  signsvfnn  31856  ftc2re  31869  cvmliftlem6  32537  cvmliftlem7  32538  cvmliftlem8  32539  cvmliftlem9  32540  cvmliftlem10  32541  cvmliftlem13  32543  ivthALT  33683  iooelexlt  34646  relowlssretop  34647  relowlpssretop  34648  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem30  34937  poimir  34940  heicant  34942  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem  34958  itg2addnclem2  34959  itg2gt0cn  34962  ibladdnclem  34963  iblabsnclem  34970  iblabsnc  34971  iblmulc2nc  34972  bddiblnc  34977  ftc1cnnclem  34980  ftc1anclem1  34982  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  areacirclem1  34997  areacirclem5  35001  areacirc  35002  isbnd3  35077  blbnd  35080  prdsbnd  35086  prdsbnd2  35088  cntotbnd  35089  idomrootle  39844  idomodle  39845  itgpowd  39870  imo72b2  40574  cvgdvgrat  40694  radcnvrat  40695  rfcnpre3  41339  rfcnpre4  41340  nnxrd  41348  absfico  41530  lefldiveq  41608  lttri5d  41615  supxrgere  41650  supxrgelem  41654  supxrge  41655  xralrple2  41671  infxr  41684  infleinflem1  41687  infleinflem2  41688  xralrple4  41690  xralrple3  41691  xrralrecnnle  41702  xrralrecnnge  41711  supxrunb3  41721  unb2ltle  41738  zxrd  41778  gtnelioc  41814  ltnelicc  41821  iooabslt  41823  gtnelicc  41824  eliooshift  41831  iocopn  41845  eliccelioc  41846  iooshift  41847  icoopn  41850  ge0lere  41857  iooiinicc  41867  sqrlearg  41878  iooiinioc  41881  uzinico  41885  preimaiocmnf  41886  uzubioo  41892  fsumge0cl  41903  limciccioolb  41951  lptioo1  41962  limcicciooub  41967  ltmod  41968  lptre2pt  41970  limsupre  41971  limcresiooub  41972  limcresioolb  41973  limcleqr  41974  limsupresico  42030  limsuppnfdlem  42031  limsupub  42034  limsupequzlem  42052  limsupre2lem  42054  limsupre3lem  42062  limsupvaluz2  42068  supcnvlimsup  42070  liminfresico  42101  limsup10exlem  42102  liminflelimsuplem  42105  limsupgtlem  42107  liminfval4  42119  liminfvaluz2  42125  limsupvaluz4  42130  liminflimsupclim  42137  xlimxrre  42161  xlimmnfvlem1  42162  xlimmnfv  42164  xlimpnfvlem1  42166  xlimpnfv  42168  sinaover2ne0  42198  ioccncflimc  42217  icccncfext  42219  icocncflimc  42221  cncfiooicclem1  42225  cncfiooicc  42226  cncfiooiccre  42227  cncfioobdlem  42228  dvbdfbdioolem1  42262  dvbdfbdioolem2  42263  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc1  42267  ioodvbdlimc2lem  42268  ioodvbdlimc2  42269  ditgeqiooicc  42294  iblsplit  42300  itgcoscmulx  42303  ibliooicc  42305  iblspltprt  42307  itgsincmulx  42308  itgsubsticc  42310  itgioocnicc  42311  iblcncfioo  42312  itgspltprt  42313  itgiccshift  42314  volioore  42324  voliooico  42326  voliooicof  42330  voliccico  42333  stoweidlem34  42368  stoweidlem52  42386  stirlinglem5  42412  dirkercncflem1  42437  dirkercncflem4  42440  fourierdlem4  42445  fourierdlem10  42451  fourierdlem19  42460  fourierdlem20  42461  fourierdlem24  42465  fourierdlem25  42466  fourierdlem26  42467  fourierdlem27  42468  fourierdlem28  42469  fourierdlem31  42472  fourierdlem32  42473  fourierdlem33  42474  fourierdlem35  42476  fourierdlem37  42478  fourierdlem40  42481  fourierdlem41  42482  fourierdlem43  42484  fourierdlem44  42485  fourierdlem46  42486  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem52  42492  fourierdlem54  42494  fourierdlem57  42497  fourierdlem59  42499  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem68  42508  fourierdlem69  42509  fourierdlem70  42510  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem84  42524  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem92  42532  fourierdlem93  42533  fourierdlem94  42534  fourierdlem97  42537  fourierdlem100  42540  fourierdlem101  42541  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem109  42549  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fourierdlem114  42554  sqwvfoura  42562  fouriersw  42565  etransclem23  42591  etransclem46  42614  qndenserrnbllem  42628  rrxsnicc  42634  ioorrnopnlem  42638  ioorrnopnxrlem  42640  salgencntex  42675  sge0cl  42712  sge0fsum  42718  sge0iunmptlemre  42746  sge0isum  42758  sge0ad2en  42762  sge0xaddlem1  42764  sge0xaddlem2  42765  sge0reuz  42778  voliunsge0lem  42803  meassre  42808  omessre  42841  omeiunltfirp  42850  hoissre  42875  hoiprodcl  42878  ovnsubaddlem1  42901  hoiprodcl3  42911  hoidmvcl  42913  hsphoidmvle2  42916  hsphoidmvle  42917  sge0hsphoire  42920  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  ovnhoilem1  42932  ovnhoilem2  42933  ovnhoi  42934  ovnlecvr2  42941  hspdifhsp  42947  hoidifhspdmvle  42951  hoiqssbllem1  42953  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem1  42957  hspmbllem2  42958  volicorege0  42968  ovolval5lem1  42983  ovolval5lem2  42984  iinhoiicclem  43004  iinhoiicc  43005  iunhoiioolem  43006  iunhoiioo  43007  vonioolem2  43012  vonicclem2  43015  vonsn  43022  pimltmnf2  43028  pimconstlt0  43031  pimgtpnf2  43034  salpreimagelt  43035  salpreimalegt  43037  preimageiingt  43047  preimaleiinlt  43048  pimrecltneg  43050  issmflem  43053  issmflelem  43070  issmfgtlem  43081  issmfgt  43082  smfaddlem1  43088  issmfgelem  43094  issmfge  43095  smfpimioompt  43110  smfresal  43112  smfrec  43113  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  smfmullem4  43118  smfpimbor1lem1  43122  smfsuplem1  43134  smflimsuplem4  43146  smfliminflem  43153  bgoldbtbnd  44023  eenglngeehlnmlem2  44774