Theorem rexrd 10956

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-xr 10944

This theorem is referenced by:  xnn0xr  12240  rpxr  12668  rpxrd  12702  max0sub  12859  qextltlem  12865  xralrple  12868  xnegcl  12876  xaddf  12887  xnn0lem1lt  12907  xnn0lenn0nn0  12908  xmulf  12935  xadddi  12958  xrub  12975  supxrre  12990  infxrre  12999  ixxub  13029  ixxlb  13030  ioo0  13033  ico0  13054  ioc0  13055  iooshf  13087  icoshftf1o  13135  supicc  13162  supiccub  13163  supicclub  13164  xnn0xrge0  13167  ssfzunsn  13231  addmodid  13567  hashnnn0genn0  13985  hashunsnggt  14037  elicc4abs  14959  caucvgrlem  15312  fprodge1  15633  pcxcl  16490  pcdvdsb  16498  pcaddlem  16517  ramcl2lem  16638  ramlb  16648  0ram  16649  setsstruct  16805  prdsxmetlem  23429  xblss2ps  23462  xblss2  23463  blss2ps  23464  blss2  23465  blhalf  23466  metustto  23615  metustexhalf  23618  nmoi  23798  nmoix  23799  nmoi2  23800  nmoleub  23801  qdensere  23839  cnblcld  23844  ioo2blex  23863  tgioo  23865  blcvx  23867  zcld  23882  recld2  23883  iccntr  23890  icccmplem1  23891  reconnlem1  23895  reconnlem2  23896  opnreen  23900  metnrmlem3  23930  icoopnst  24008  iocopnst  24009  cnheibor  24024  lebnumii  24035  nmoleub2lem  24183  lmnn  24332  iscau3  24347  minveclem4  24501  ivthlem1  24520  ivthlem2  24521  ivthlem3  24522  ivth2  24524  ivthle  24525  ivthle2  24526  ivthicc  24527  evthicc  24528  cniccbdd  24530  ovolgelb  24549  ovollb2lem  24557  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun  24574  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem4  24589  ovolicc2lem5  24590  ovolicc2  24591  ovolicc  24592  nulmbl2  24605  voliunlem2  24620  ioombl1lem4  24630  ioorcl2  24641  uniioombllem1  24650  uniioombllem2a  24651  uniioombllem3  24654  dyaddisjlem  24664  dyadmaxlem  24666  opnmbllem  24670  volivth  24676  vitalilem4  24680  mbfmulc2lem  24716  mbfmax  24718  mbfposr  24721  ismbf3d  24723  mbfaddlem  24729  mbflimsup  24735  mbfi1fseqlem4  24788  itg2lcl  24797  xrge0f  24801  itg2itg1  24806  itg2const2  24811  itg2seq  24812  itg2uba  24813  itg2lea  24814  itg2mulclem  24816  itg2mulc  24817  itg2splitlem  24818  itg2split  24819  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  itg2cn  24833  iblss  24874  itgle  24879  itgeqa  24883  itgioo  24885  ibladdlem  24889  iblabs  24898  iblabsr  24899  iblmulc2  24900  itgsplit  24905  itgspliticc  24906  itgsplitioo  24907  bddmulibl  24908  bddiblnc  24911  ditgcl  24927  ditgswap  24928  ditgsplitlem  24929  dvferm1lem  25053  dvferm2lem  25055  dvferm  25057  rollelem  25058  rolle  25059  cmvth  25060  mvth  25061  dvlip  25062  dvlip2  25064  c1liplem1  25065  c1lip1  25066  dveq0  25069  dvgt0lem1  25071  dvivthlem1  25077  dvivth  25079  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  dvcnvrelem1  25086  dvcnvre  25088  dvcvx  25089  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsumrlimge0  25099  dvfsumrlim2  25101  ftc1lem1  25104  ftc1lem2  25105  ftc1a  25106  ftc1lem4  25108  ftc2  25113  ftc2ditglem  25114  itgparts  25116  itgsubstlem  25117  itgsubst  25118  itgpowd  25119  degltlem1  25142  deg1ge  25168  coe1mul3  25169  deg1sublt  25180  deg1mul2  25184  deg1tmle  25187  deg1tm  25188  plypf1  25278  taylfvallem1  25421  tayl0  25426  pserulm  25486  psercnlem1  25489  pserdvlem1  25491  pserdvlem2  25492  abelthlem3  25497  abelth  25505  efcvx  25513  logno1  25696  logtayl  25720  xrlimcnp  26023  logfacbnd3  26276  log2sumbnd  26597  pntpbnd2  26640  pntibndlem3  26645  ttgcontlem1  27155  nmooge0  29030  nmoub3i  29036  isblo3i  29064  ubthlem1  29133  minvecolem4  29143  nmopge0  30174  nmfnge0  30190  nmophmi  30294  branmfn  30368  xaddeq0  30978  xlt2addrd  30983  xmulcand  31097  xreceu  31098  xdivrec  31103  fsumrp0cl  31206  xrge0slmod  31450  cnre2csqlem  31762  tpr2rico  31764  xrge0iifcnv  31785  xrge0iifhom  31789  lmxrge0  31804  esumfsup  31938  esumpcvgval  31946  esumcvg  31954  dya2iocress  32141  dya2iocbrsiga  32142  dya2icobrsiga  32143  dya2icoseg  32144  dya2iocucvr  32151  sxbrsigalem2  32153  omssubaddlem  32166  omssubadd  32167  orvcgteel  32334  dstrvprob  32338  orvclteel  32339  sgnmul  32409  sgnsub  32411  sgnmulsgn  32416  sgnmulsgp  32417  signstcl  32444  signstf  32445  signstf0  32447  signstfvn  32448  signsvtn0  32449  signsvfn  32461  signsvfpn  32464  signsvfnn  32465  ftc2re  32478  cvmliftlem6  33152  cvmliftlem7  33153  cvmliftlem8  33154  cvmliftlem9  33155  cvmliftlem10  33156  cvmliftlem13  33158  ivthALT  34451  iooelexlt  35460  relowlssretop  35461  relowlpssretop  35462  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem30  35734  poimir  35737  heicant  35739  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnclem  35755  itg2addnclem2  35756  itg2gt0cn  35759  ibladdnclem  35760  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  ftc1cnnclem  35775  ftc1anclem1  35777  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  ftc2nc  35786  areacirclem1  35792  areacirclem5  35796  areacirc  35797  isbnd3  35869  blbnd  35872  prdsbnd  35878  prdsbnd2  35880  cntotbnd  35881  dvrelog3  40001  0nonelalab  40003  dvrelogpow2b  40004  dvle2  40008  aks4d1p1p6  40009  aks4d1p1p5  40011  idomrootle  40936  idomodle  40937  imo72b2  41672  cvgdvgrat  41820  radcnvrat  41821  rfcnpre3  42465  rfcnpre4  42466  nnxrd  42474  absfico  42647  lefldiveq  42721  lttri5d  42728  supxrgere  42762  supxrgelem  42766  supxrge  42767  xralrple2  42783  infxr  42796  infleinflem1  42799  infleinflem2  42800  xralrple4  42802  xralrple3  42803  xrralrecnnle  42812  xrralrecnnge  42820  supxrunb3  42829  unb2ltle  42845  zxrd  42883  gtnelioc  42919  ltnelicc  42925  iooabslt  42927  gtnelicc  42928  eliooshift  42934  iocopn  42948  eliccelioc  42949  iooshift  42950  icoopn  42953  ge0lere  42960  iooiinicc  42970  sqrlearg  42981  iooiinioc  42984  uzinico  42988  preimaiocmnf  42989  uzubioo  42995  fsumge0cl  43004  limciccioolb  43052  lptioo1  43063  limcicciooub  43068  ltmod  43069  lptre2pt  43071  limsupre  43072  limcresiooub  43073  limcresioolb  43074  limcleqr  43075  limsupresico  43131  limsuppnfdlem  43132  limsupub  43135  limsupequzlem  43153  limsupre2lem  43155  limsupre3lem  43163  limsupvaluz2  43169  supcnvlimsup  43171  liminfresico  43202  limsup10exlem  43203  liminflelimsuplem  43206  limsupgtlem  43208  liminfval4  43220  liminfvaluz2  43226  limsupvaluz4  43231  liminflimsupclim  43238  xlimxrre  43262  xlimmnfvlem1  43263  xlimmnfv  43265  xlimpnfvlem1  43267  xlimpnfv  43269  sinaover2ne0  43299  ioccncflimc  43316  icccncfext  43318  icocncflimc  43320  cncfiooicclem1  43324  cncfiooicc  43325  cncfiooiccre  43326  cncfioobdlem  43327  dvbdfbdioolem1  43359  dvbdfbdioolem2  43360  dvbdfbdioo  43361  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc1  43364  ioodvbdlimc2lem  43365  ioodvbdlimc2  43366  ditgeqiooicc  43391  iblsplit  43397  itgcoscmulx  43400  ibliooicc  43402  iblspltprt  43404  itgsincmulx  43405  itgsubsticc  43407  itgioocnicc  43408  iblcncfioo  43409  itgspltprt  43410  itgiccshift  43411  volioore  43421  voliooico  43423  voliooicof  43427  voliccico  43430  stoweidlem34  43465  stoweidlem52  43483  stirlinglem5  43509  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem4  43542  fourierdlem10  43548  fourierdlem19  43557  fourierdlem20  43558  fourierdlem24  43562  fourierdlem25  43563  fourierdlem26  43564  fourierdlem27  43565  fourierdlem28  43566  fourierdlem31  43569  fourierdlem32  43570  fourierdlem33  43571  fourierdlem35  43573  fourierdlem37  43575  fourierdlem40  43578  fourierdlem41  43579  fourierdlem43  43581  fourierdlem44  43582  fourierdlem46  43583  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem52  43589  fourierdlem54  43591  fourierdlem57  43594  fourierdlem59  43596  fourierdlem60  43597  fourierdlem61  43598  fourierdlem62  43599  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem68  43605  fourierdlem69  43606  fourierdlem70  43607  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem84  43621  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem93  43630  fourierdlem94  43631  fourierdlem97  43634  fourierdlem100  43637  fourierdlem101  43638  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem109  43646  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fourierdlem114  43651  sqwvfoura  43659  fouriersw  43662  etransclem23  43688  etransclem46  43711  qndenserrnbllem  43725  rrxsnicc  43731  ioorrnopnlem  43735  ioorrnopnxrlem  43737  salgencntex  43772  sge0cl  43809  sge0fsum  43815  sge0iunmptlemre  43843  sge0isum  43855  sge0ad2en  43859  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0reuz  43875  voliunsge0lem  43900  meassre  43905  omessre  43938  omeiunltfirp  43947  hoissre  43972  hoiprodcl  43975  ovnsubaddlem1  43998  hoiprodcl3  44008  hoidmvcl  44010  hsphoidmvle2  44013  hsphoidmvle  44014  sge0hsphoire  44017  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  ovnhoilem1  44029  ovnhoilem2  44030  ovnhoi  44031  ovnlecvr2  44038  hspdifhsp  44044  hoidifhspdmvle  44048  hoiqssbllem1  44050  hoiqssbllem2  44051  hoiqssbllem3  44052  hspmbllem1  44054  hspmbllem2  44055  volicorege0  44065  ovolval5lem1  44080  ovolval5lem2  44081  iinhoiicclem  44101  iinhoiicc  44102  iunhoiioolem  44103  iunhoiioo  44104  vonioolem2  44109  vonicclem2  44112  vonsn  44119  pimltmnf2  44125  pimconstlt0  44128  pimgtpnf2  44131  salpreimagelt  44132  salpreimalegt  44134  preimageiingt  44144  preimaleiinlt  44145  pimrecltneg  44147  issmflem  44150  issmflelem  44167  issmfgtlem  44178  issmfgt  44179  smfaddlem1  44185  issmfgelem  44191  issmfge  44192  smfpimioompt  44207  smfresal  44209  smfrec  44210  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  smfmullem4  44215  smfpimbor1lem1  44219  smfsuplem1  44231  smflimsuplem4  44243  smfliminflem  44250  bgoldbtbnd  45149  eenglngeehlnmlem2  45972