Theorem rexrd 10089

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 10083	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sseldi 3601	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1990   RRcr 9935   RR*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-xr 10078

This theorem is referenced by:  xnn0xr  11368  rpxr  11840  rpxrd  11873  max0sub  12027  qextltlem  12033  xralrple  12036  xnegcl  12044  xaddf  12055  xnn0lenn0nn0  12075  xmulf  12102  xadddi  12125  supxrre  12157  infxrre  12166  ixxub  12196  ixxlb  12197  ioo0  12200  ico0  12221  ioc0  12222  iooshf  12252  icoshftf1o  12295  supicc  12320  supiccub  12321  supicclub  12322  xnn0xrge0  12325  ssfzunsn  12387  addmodid  12718  hashnnn0genn0  13131  elicc4abs  14059  caucvgrlem  14403  fprodge1  14726  pcxcl  15565  pcdvdsb  15573  pcaddlem  15592  ramcl2lem  15713  ramlb  15723  0ram  15724  setsstruct  15898  prdsxmetlem  22173  xblss2ps  22206  xblss2  22207  blss2ps  22208  blss2  22209  blhalf  22210  metustto  22358  metustexhalf  22361  nmoi  22532  nmoix  22533  nmoi2  22534  nmoleub  22535  qdensere  22573  cnblcld  22578  ioo2blex  22597  tgioo  22599  blcvx  22601  zcld  22616  recld2  22617  iccntr  22624  icccmplem1  22625  reconnlem1  22629  reconnlem2  22630  opnreen  22634  metnrmlem3  22664  icoopnst  22738  cnheibor  22754  lebnumii  22765  nmoleub2lem  22914  lmnn  23061  iscau3  23076  minveclem4  23203  ivthlem1  23220  ivthlem2  23221  ivthlem3  23222  ivth2  23224  ivthle  23225  ivthle2  23226  ivthicc  23227  evthicc  23228  cniccbdd  23230  ovolgelb  23248  ovollb2lem  23256  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun  23273  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicc2  23290  ovolicc  23291  nulmbl2  23304  voliunlem2  23319  ioombl1lem4  23329  ioorcl2  23340  uniioombllem1  23349  uniioombllem2a  23350  uniioombllem3  23353  dyaddisjlem  23363  dyadmaxlem  23365  opnmbllem  23369  volivth  23375  vitalilem4  23380  mbfmulc2lem  23414  mbfmax  23416  mbfposr  23419  ismbf3d  23421  mbfaddlem  23427  mbflimsup  23433  mbfi1fseqlem4  23485  itg2lcl  23494  xrge0f  23498  itg2itg1  23503  itg2const2  23508  itg2seq  23509  itg2uba  23510  itg2lea  23511  itg2mulclem  23513  itg2mulc  23514  itg2splitlem  23515  itg2split  23516  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  itg2cn  23530  iblss  23571  itgle  23576  itgeqa  23580  itgioo  23582  ibladdlem  23586  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgsplit  23602  itgspliticc  23603  itgsplitioo  23604  bddmulibl  23605  ditgcl  23622  ditgswap  23623  ditgsplitlem  23624  dvferm1lem  23747  dvferm2lem  23749  dvferm  23751  rollelem  23752  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlip2  23758  c1liplem1  23759  c1lip1  23760  dveq0  23763  dvgt0lem1  23765  dvivthlem1  23771  dvivth  23773  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvre  23782  dvcvx  23783  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlimge0  23793  dvfsumrlim2  23795  ftc1lem1  23798  ftc1lem2  23799  ftc1a  23800  ftc1lem4  23802  ftc2  23807  ftc2ditglem  23808  itgparts  23810  itgsubstlem  23811  itgsubst  23812  degltlem1  23832  deg1ge  23858  coe1mul3  23859  deg1sublt  23870  deg1mul2  23874  deg1tmle  23877  deg1tm  23878  plypf1  23968  taylfvallem1  24111  tayl0  24116  pserulm  24176  psercnlem1  24179  pserdvlem1  24181  pserdvlem2  24182  abelthlem3  24187  abelth  24195  efcvx  24203  logno1  24382  logtayl  24406  xrlimcnp  24695  logfacbnd3  24948  log2sumbnd  25233  pntpbnd2  25276  pntibndlem3  25281  ttgcontlem1  25765  nmooge0  27622  nmoub3i  27628  isblo3i  27656  ubthlem1  27726  minvecolem4  27736  nmopge0  28770  nmfnge0  28786  nmophmi  28890  branmfn  28964  xaddeq0  29518  xlt2addrd  29523  xmulcand  29629  xreceu  29630  xdivrec  29635  fsumrp0cl  29695  xrge0slmod  29844  cnre2csqlem  29956  tpr2rico  29958  xrge0iifcnv  29979  xrge0iifhom  29983  lmxrge0  29998  esumfsup  30132  esumpcvgval  30140  esumcvg  30148  dya2iocress  30336  dya2iocbrsiga  30337  dya2icobrsiga  30338  dya2icoseg  30339  dya2iocucvr  30346  sxbrsigalem2  30348  omssubaddlem  30361  omssubadd  30362  orvcgteel  30529  dstrvprob  30533  orvclteel  30534  sgnmul  30604  sgnsub  30606  sgnmulsgn  30611  sgnmulsgp  30612  signstcl  30642  signstf  30643  signstf0  30645  signstfvn  30646  signsvtn0  30647  signstfvneq0  30649  signsvfn  30659  signsvfpn  30662  signsvfnn  30663  ftc2re  30676  cvmliftlem6  31272  cvmliftlem7  31273  cvmliftlem8  31274  cvmliftlem9  31275  cvmliftlem10  31276  cvmliftlem13  31278  ivthALT  32330  iooelexlt  33210  relowlssretop  33211  relowlpssretop  33212  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem30  33439  poimir  33442  heicant  33444  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem2  33462  itg2gt0cn  33465  ibladdnclem  33466  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  ftc1cnnclem  33483  ftc1anclem1  33485  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  areacirclem1  33500  areacirclem5  33504  areacirc  33505  isbnd3  33583  blbnd  33586  prdsbnd  33592  prdsbnd2  33594  cntotbnd  33595  idomrootle  37773  idomodle  37774  itgpowd  37800  imo72b2  38475  cvgdvgrat  38512  radcnvrat  38513  rfcnpre3  39192  rfcnpre4  39193  nnxrd  39201  absfico  39410  lefldiveq  39505  lttri5d  39513  supxrgere  39549  supxrgelem  39553  supxrge  39554  xralrple2  39570  infxr  39583  infleinflem1  39586  infleinflem2  39587  xralrple4  39589  xralrple3  39590  xrralrecnnle  39602  xrralrecnnge  39613  supxrunb3  39623  unb2ltle  39642  zxrd  39682  gtnelioc  39712  ltnelicc  39719  iooabslt  39721  gtnelicc  39722  eliooshift  39729  iocopn  39746  eliccelioc  39747  iooshift  39748  icoopn  39751  ge0lere  39759  iooiinicc  39769  sqrlearg  39780  iooiinioc  39783  uzinico  39787  preimaiocmnf  39788  uzubioo  39794  fsumge0cl  39805  limciccioolb  39853  lptioo1  39864  limcicciooub  39869  ltmod  39870  lptre2pt  39872  limsupre  39873  limcresiooub  39874  limcresioolb  39875  limcleqr  39876  limsupresico  39932  limsuppnfdlem  39933  limsupub  39936  limsupequzlem  39954  limsupre2lem  39956  limsupre3lem  39964  limsupvaluz2  39970  supcnvlimsup  39972  liminfresico  40003  limsup10exlem  40004  liminflelimsuplem  40007  limsupgtlem  40009  liminfval4  40021  liminfvaluz2  40027  limsupvaluz4  40032  liminflimsupclim  40039  xlimxrre  40057  xlimmnfvlem1  40058  xlimmnfv  40060  xlimpnfvlem1  40062  xlimpnfv  40064  sinaover2ne0  40079  ioccncflimc  40098  icccncfext  40100  icocncflimc  40102  cncfiooicclem1  40106  cncfiooicc  40107  cncfiooiccre  40108  cncfioobdlem  40109  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc1  40148  ioodvbdlimc2lem  40149  ioodvbdlimc2  40150  ditgeqiooicc  40176  iblsplit  40182  itgcoscmulx  40185  ibliooicc  40187  iblspltprt  40189  itgsincmulx  40190  itgsubsticc  40192  itgioocnicc  40193  iblcncfioo  40194  itgspltprt  40195  itgiccshift  40196  volioore  40207  voliooico  40209  voliooicof  40213  voliccico  40216  stoweidlem34  40251  stoweidlem52  40269  stirlinglem5  40295  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem10  40334  fourierdlem19  40343  fourierdlem20  40344  fourierdlem24  40348  fourierdlem25  40349  fourierdlem26  40350  fourierdlem27  40351  fourierdlem28  40352  fourierdlem31  40355  fourierdlem32  40356  fourierdlem33  40357  fourierdlem35  40359  fourierdlem37  40361  fourierdlem40  40364  fourierdlem41  40365  fourierdlem43  40367  fourierdlem44  40368  fourierdlem46  40369  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem52  40375  fourierdlem54  40377  fourierdlem57  40380  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem68  40391  fourierdlem69  40392  fourierdlem70  40393  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem84  40407  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem97  40420  fourierdlem100  40423  fourierdlem101  40424  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem109  40432  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fourierdlem114  40437  sqwvfoura  40445  fouriersw  40448  etransclem23  40474  etransclem46  40497  qndenserrnbllem  40514  rrxsnicc  40520  ioorrnopnlem  40524  ioorrnopnxrlem  40526  salgencntex  40561  sge0cl  40598  sge0fsum  40604  sge0iunmptlemre  40632  sge0isum  40644  sge0ad2en  40648  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0reuz  40664  voliunsge0lem  40689  meassre  40694  omessre  40724  omeiunltfirp  40733  hoissre  40758  hoiprodcl  40761  ovnsubaddlem1  40784  hoiprodcl3  40794  hoidmvcl  40796  hsphoidmvle2  40799  hsphoidmvle  40800  sge0hsphoire  40803  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  ovnhoilem1  40815  ovnhoilem2  40816  ovnhoi  40817  ovnlecvr2  40824  hspdifhsp  40830  hoidifhspdmvle  40834  hoiqssbllem1  40836  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem1  40840  hspmbllem2  40841  volicorege0  40851  ovolval5lem1  40866  ovolval5lem2  40867  iinhoiicclem  40887  iinhoiicc  40888  iunhoiioolem  40889  iunhoiioo  40890  vonioolem2  40895  vonicclem2  40898  vonsn  40905  pimltmnf2  40911  pimconstlt0  40914  pimgtpnf2  40917  salpreimagelt  40918  salpreimalegt  40920  preimageiingt  40930  preimaleiinlt  40931  pimrecltneg  40933  issmflem  40936  issmflelem  40953  issmfgtlem  40964  issmfgt  40965  smfaddlem1  40971  issmfgelem  40977  issmfge  40978  smfpimioompt  40993  smfresal  40995  smfrec  40996  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  smfmullem4  41001  smfpimbor1lem1  41005  smfsuplem1  41017  smflimsuplem4  41029  smfliminflem  41036  bgoldbtbnd  41697