Theorem rexrd 9716

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
rexrd	|- ( ph -> A e. RR* )

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 9710	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sseldi 3442	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1898   RRcr 9564   RR*cxr 9700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430  df-xr 9705

This theorem is referenced by:  rpxr  11338  rpxrd  11371  max0sub  11518  qextltlem  11524  xralrple  11527  xnegcl  11535  xaddf  11546  xmulf  11587  xadddi  11610  supxrre  11642  infxrre  11651  infmxrreOLD  11655  ixxub  11685  ixxlb  11686  ixxlbOLD  11687  ioo0  11690  ico0  11711  ioc0  11712  iooshf  11742  icoshftf1o  11784  supicc  11809  supiccub  11810  supicclub  11811  addmodid  12171  hashnnn0genn0  12558  elicc4abs  13431  caucvgrlem  13785  caucvgrlemOLD  13786  fprodge1  14098  pcxcl  14859  pcdvdsb  14867  pcaddlem  14882  ramcl2lem  15011  ramcl2lemOLD  15012  ramlb  15026  0ram  15027  prdsxmetlem  21432  xblss2ps  21465  xblss2  21466  blss2ps  21467  blss2  21468  blhalf  21469  metustto  21617  metustexhalf  21620  nmoi  21782  nmoix  21783  nmoi2  21784  nmoleub  21785  nmoiOLD  21798  nmoixOLD  21799  nmoi2OLD  21800  nmoleubOLD  21801  qdensere  21839  cnblcld  21844  ioo2blex  21861  tgioo  21863  blcvx  21865  zcld  21880  recld2  21881  iccntr  21888  icccmplem1  21889  reconnlem1  21893  reconnlem2  21894  opnreen  21898  metnrmlem3  21927  metnrmlem3OLD  21942  icoopnst  22016  cnheibor  22032  lebnumii  22046  nmoleub2lem  22177  lmnn  22282  iscau3  22297  minveclem4  22423  minveclem4OLD  22435  ivthlem1  22451  ivthlem2  22452  ivthlem3  22453  ivth2  22455  ivthle  22456  ivthle2  22457  ivthicc  22458  evthicc  22459  cniccbdd  22461  ovolgelb  22482  ovollb2lem  22490  ovolunlem1  22499  ovoliunlem1  22504  ovoliunlem2  22505  ovoliun  22507  ovolscalem1  22515  ovolicc1  22518  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ovolicc2lem5  22524  ovolicc2  22525  ovolicc  22526  nulmbl2  22539  voliunlem2  22553  ioombl1lem4  22563  ioorcl2  22573  uniioombllem1  22587  uniioombllem2a  22588  uniioombllem3  22592  dyaddisjlem  22602  dyadmaxlem  22604  opnmbllem  22608  volivth  22614  vitalilem4  22618  mbfmulc2lem  22652  mbfmax  22654  mbfposr  22657  ismbf3d  22659  mbfaddlem  22665  mbflimsup  22672  mbflimsupOLD  22673  mbfi1fseqlem4  22725  itg2lcl  22734  xrge0f  22738  itg2itg1  22743  itg2const2  22748  itg2seq  22749  itg2uba  22750  itg2lea  22751  itg2mulclem  22753  itg2mulc  22754  itg2splitlem  22755  itg2split  22756  itg2monolem2  22758  itg2monolem3  22759  itg2mono  22760  itg2gt0  22767  itg2cnlem1  22768  itg2cnlem2  22769  itg2cn  22770  iblss  22811  itgle  22816  itgeqa  22820  itgioo  22822  ibladdlem  22826  iblabs  22835  iblabsr  22836  iblmulc2  22837  itgsplit  22842  itgspliticc  22843  itgsplitioo  22844  bddmulibl  22845  ditgcl  22862  ditgswap  22863  ditgsplitlem  22864  dvferm1lem  22985  dvferm2lem  22987  dvferm  22989  rollelem  22990  rolle  22991  cmvth  22992  mvth  22993  dvlip  22994  dvlip2  22996  c1liplem1  22997  c1lip1  22998  dveq0  23001  dvgt0lem1  23003  dvivthlem1  23009  dvivth  23011  lhop1lem  23014  lhop1  23015  lhop2  23016  lhop  23017  dvcnvrelem1  23018  dvcnvre  23020  dvcvx  23021  dvfsumle  23022  dvfsumge  23023  dvfsumabs  23024  dvfsumlem2  23028  dvfsumlem3  23029  dvfsumlem4  23030  dvfsumrlimge0  23031  dvfsumrlim2  23033  ftc1lem1  23036  ftc1lem2  23037  ftc1a  23038  ftc1lem4  23040  ftc2  23045  ftc2ditglem  23046  itgparts  23048  itgsubstlem  23049  itgsubst  23050  degltlem1  23070  deg1ge  23096  coe1mul3  23097  deg1sublt  23108  deg1mul2  23112  deg1tmle  23115  deg1tm  23116  plypf1  23215  taylfvallem1  23361  tayl0  23366  pserulm  23426  psercnlem1  23429  pserdvlem1  23431  pserdvlem2  23432  abelthlem3  23437  abelth  23445  efcvx  23453  logno1  23630  logtayl  23654  xrlimcnp  23943  logfacbnd3  24200  log2sumbnd  24431  pntpbnd2  24474  pntibndlem3  24479  ttgcontlem1  24964  nvlmle  26377  nmooge0  26457  nmoub3i  26463  isblo3i  26491  ubthlem1  26561  minvecolem4  26571  minvecolem4OLD  26581  nmopge0  27613  nmfnge0  27629  nmophmi  27733  branmfn  27807  xaddeq0  28379  xlt2addrd  28387  xmulcand  28439  xreceu  28440  xdivrec  28445  fsumrp0cl  28507  xrge0slmod  28656  cnre2csqlem  28765  tpr2rico  28767  xrge0iifcnv  28788  xrge0iifhom  28792  lmxrge0  28807  esumfsup  28940  esumpcvgval  28948  esumcvg  28956  dya2iocress  29145  dya2iocbrsiga  29146  dya2icobrsiga  29147  dya2icoseg  29148  dya2iocucvr  29155  sxbrsigalem2  29157  omssubaddlem  29176  omssubadd  29177  omssubaddlemOLD  29180  omssubaddOLD  29181  orvcgteel  29349  dstrvprob  29353  orvclteel  29354  sgnmul  29462  sgnsub  29464  sgnmulsgn  29469  sgnmulsgp  29470  signstcl  29503  signstf  29504  signstf0  29506  signstfvn  29507  signsvtn0  29508  signstfvneq0  29510  signsvfn  29520  signsvfpn  29523  signsvfnn  29524  cvmliftlem6  30062  cvmliftlem7  30063  cvmliftlem8  30064  cvmliftlem9  30065  cvmliftlem10  30066  cvmliftlem13  30068  ivthALT  31040  iooelexlt  31810  relowlssretop  31811  relowlpssretop  31812  sin2h  31980  cos2h  31981  tan2h  31982  poimirlem30  32015  poimir  32018  heicant  32020  opnmbllem0  32021  mblfinlem1  32022  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  dvtanlemOLD  32036  itg2addnclem  32038  itg2addnclem2  32039  itg2gt0cn  32042  ibladdnclem  32043  iblabsnclem  32050  iblabsnc  32051  iblmulc2nc  32052  bddiblnc  32057  ftc1cnnclem  32060  ftc1anclem1  32062  ftc1anclem4  32065  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  ftc2nc  32071  areacirclem1  32077  areacirclem5  32081  areacirc  32082  isbnd3  32161  blbnd  32164  prdsbnd  32170  prdsbnd2  32172  cntotbnd  32173  idomrootle  36114  idomodle  36115  itgpowd  36144  imo72b2  36663  cvgdvgrat  36706  radcnvrat  36707  rfcnpre3  37394  rfcnpre4  37395  nnxrd  37403  lefldiveq  37544  lttri5d  37555  supxrgere  37594  supxrgelem  37598  supxrge  37599  xralrple2  37615  gtnelioc  37625  ltnelicc  37632  iooabslt  37634  gtnelicc  37635  eliooshift  37642  iocopn  37659  eliccelioc  37660  iooshift  37661  icoopn  37664  ge0lere  37672  fsumge0cl  37690  limciccioolb  37739  lptioo1  37750  limcicciooub  37755  ltmod  37756  lptre2pt  37758  limsupre  37759  limsupreOLD  37760  limcresiooub  37761  limcresioolb  37762  limcleqr  37763  sinaover2ne0  37781  ioccncflimc  37801  icccncfext  37803  icocncflimc  37805  cncfiooicclem1  37809  cncfiooicc  37810  cncfiooiccre  37811  cncfioobdlem  37812  dvbdfbdioolem1  37838  dvbdfbdioolem2  37839  dvbdfbdioo  37840  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem1OLD  37843  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc1  37845  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  ioodvbdlimc2  37848  ditgeqiooicc  37875  iblsplit  37881  itgcoscmulx  37884  ibliooicc  37886  iblspltprt  37888  itgsincmulx  37889  itgsubsticc  37891  itgioocnicc  37892  iblcncfioo  37893  itgspltprt  37894  itgiccshift  37895  stoweidlem34  37933  stoweidlem52  37951  stirlinglem5  37978  dirkercncflem1  38003  dirkercncflem4  38006  fourierdlem4  38011  fourierdlem10  38017  fourierdlem19  38026  fourierdlem20  38027  fourierdlem24  38031  fourierdlem25  38032  fourierdlem26  38033  fourierdlem27  38034  fourierdlem28  38035  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem32  38040  fourierdlem33  38041  fourierdlem35  38043  fourierdlem37  38045  fourierdlem40  38048  fourierdlem41  38049  fourierdlem43  38052  fourierdlem44  38053  fourierdlem46  38054  fourierdlem47  38055  fourierdlem48  38056  fourierdlem49  38057  fourierdlem50  38058  fourierdlem51  38059  fourierdlem52  38060  fourierdlem54  38062  fourierdlem57  38065  fourierdlem59  38067  fourierdlem60  38068  fourierdlem61  38069  fourierdlem62  38070  fourierdlem63  38071  fourierdlem64  38072  fourierdlem65  38073  fourierdlem68  38076  fourierdlem69  38077  fourierdlem70  38078  fourierdlem72  38080  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem78  38086  fourierdlem79  38087  fourierdlem81  38089  fourierdlem82  38090  fourierdlem84  38092  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem92  38100  fourierdlem93  38101  fourierdlem94  38102  fourierdlem97  38105  fourierdlem100  38108  fourierdlem101  38109  fourierdlem102  38110  fourierdlem103  38111  fourierdlem104  38112  fourierdlem107  38115  fourierdlem109  38117  fourierdlem111  38119  fourierdlem112  38120  fourierdlem113  38121  fourierdlem114  38122  sqwvfoura  38130  fouriersw  38133  etransclem23  38160  etransclem46  38183  qndenserrnbllem  38201  salgencntex  38240  sge0cl  38261  sge0fsum  38267  sge0iunmptlemre  38295  sge0isum  38307  sge0ad2en  38311  sge0xaddlem1  38313  sge0xaddlem2  38314  omessre  38369  omeiunltfirp  38378  hoissre  38404  hoiprodcl  38407  ovnsubaddlem1  38430  hoiprodcl3  38440  hoidmvcl  38442  hsphoidmvle2  38445  hsphoidmvle  38446  sge0hsphoire  38449  hoidmv1lelem1  38451  hoidmv1lelem2  38452  hoidmv1lelem3  38453  hoidmv1le  38454  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvlelem4  38458  ovnhoilem1  38461  ovnhoilem2  38462  ovnhoi  38463  ovnlecvr2  38470  hspdifhsp  38476  hoidifhspdmvle  38480  hoiqssbllem1  38482  hoiqssbllem2  38483  hoiqssbllem3  38484  hspmbllem1  38486  hspmbllem2  38487  bgoldbtbnd  38942  xnn0xr  39121  xnn0xrge0  39122