MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexrd Structured version   Unicode version

Theorem rexrd 9641
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
StepHypRef Expression
1 ressxr 9635 . 2  |-  RR  C_  RR*
2 rexrd.1 . 2  |-  ( ph  ->  A  e.  RR )
31, 2sseldi 3484 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   RRcr 9489   RR*cxr 9625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-in 3465  df-ss 3472  df-xr 9630
This theorem is referenced by:  rpxr  11231  rpxrd  11261  max0sub  11399  qextltlem  11405  xralrple  11408  xnegcl  11416  xaddf  11427  xmulf  11468  xadddi  11491  supxrre  11523  infmxrre  11531  ixxub  11554  ixxlb  11555  ioo0  11558  ico0  11579  ioc0  11580  iooshf  11607  icoshftf1o  11647  supicc  11672  supiccub  11673  supicclub  11674  hashnnn0genn0  12390  elicc4abs  13126  caucvgrlem  13469  pcxcl  14256  pcdvdsb  14264  pcaddlem  14279  ramcl2lem  14399  ramlb  14409  0ram  14410  prdsxmetlem  20737  xblss2ps  20770  xblss2  20771  blss2ps  20772  blss2  20773  blhalf  20774  metusttoOLD  20926  metustto  20927  metustexhalfOLD  20932  metustexhalf  20933  nmoi  21101  nmoix  21102  nmoi2  21103  nmoleub  21104  qdensere  21143  cnblcld  21148  ioo2blex  21165  tgioo  21167  blcvx  21169  zcld  21184  recld2  21185  iccntr  21192  icccmplem1  21193  reconnlem1  21197  reconnlem2  21198  opnreen  21202  metnrmlem3  21231  icoopnst  21305  cnheibor  21321  lebnumii  21332  nmoleub2lem  21463  lmnn  21568  iscau3  21583  minveclem4  21713  ivthlem1  21729  ivthlem2  21730  ivthlem3  21731  ivth2  21733  ivthle  21734  ivthle2  21735  ivthicc  21736  evthicc  21737  cniccbdd  21739  ovolgelb  21757  ovollb2lem  21765  ovolunlem1  21774  ovoliunlem1  21779  ovoliunlem2  21780  ovoliun  21782  ovolscalem1  21790  ovolicc1  21793  ovolicc2lem4  21797  ovolicc2lem5  21798  ovolicc2  21799  ovolicc  21800  nulmbl2  21813  voliunlem2  21827  ioombl1lem4  21837  ioorcl2  21847  uniioombllem1  21856  uniioombllem2a  21857  uniioombllem3  21860  dyaddisjlem  21870  dyadmaxlem  21872  opnmbllem  21876  volivth  21882  vitalilem4  21886  mbfmulc2lem  21920  mbfmax  21922  mbfposr  21925  ismbf3d  21927  mbfaddlem  21933  mbflimsup  21939  mbfi1fseqlem4  21991  itg2lcl  22000  xrge0f  22004  itg2itg1  22009  itg2const2  22014  itg2seq  22015  itg2uba  22016  itg2lea  22017  itg2mulclem  22019  itg2mulc  22020  itg2splitlem  22021  itg2split  22022  itg2monolem2  22024  itg2monolem3  22025  itg2mono  22026  itg2gt0  22033  itg2cnlem1  22034  itg2cnlem2  22035  itg2cn  22036  iblss  22077  itgle  22082  itgeqa  22086  itgioo  22088  ibladdlem  22092  iblabs  22101  iblabsr  22102  iblmulc2  22103  itgsplit  22108  itgspliticc  22109  itgsplitioo  22110  bddmulibl  22111  ditgcl  22128  ditgswap  22129  ditgsplitlem  22130  dvferm1lem  22251  dvferm2lem  22253  dvferm  22255  rollelem  22256  rolle  22257  cmvth  22258  mvth  22259  dvlip  22260  dvlip2  22262  c1liplem1  22263  c1lip1  22264  dveq0  22267  dvgt0lem1  22269  dvivthlem1  22275  dvivth  22277  lhop1lem  22280  lhop1  22281  lhop2  22282  lhop  22283  dvcnvrelem1  22284  dvcnvre  22286  dvcvx  22287  dvfsumle  22288  dvfsumge  22289  dvfsumabs  22290  dvfsumlem2  22294  dvfsumlem3  22295  dvfsumlem4  22296  dvfsumrlimge0  22297  dvfsumrlim2  22299  ftc1lem1  22302  ftc1lem2  22303  ftc1a  22304  ftc1lem4  22306  ftc2  22311  ftc2ditglem  22312  itgparts  22314  itgsubstlem  22315  itgsubst  22316  degltlem1  22338  deg1ge  22365  coe1mul3  22366  deg1sublt  22377  deg1mul2  22381  deg1tmle  22384  deg1tm  22385  plypf1  22475  taylfvallem1  22617  tayl0  22622  pserulm  22682  psercnlem1  22685  pserdvlem1  22687  pserdvlem2  22688  abelthlem3  22693  abelth  22701  efcvx  22709  logno1  22882  logtayl  22906  xrlimcnp  23163  logfacbnd3  23363  log2sumbnd  23594  pntpbnd2  23637  pntibndlem3  23642  ttgcontlem1  24053  nvlmle  25467  nmooge0  25547  nmoub3i  25553  isblo3i  25581  ubthlem1  25651  minvecolem4  25661  nmopge0  26695  nmfnge0  26711  nmophmi  26815  branmfn  26889  xaddeq0  27438  xlt2addrd  27443  xmulcand  27483  xreceu  27484  xdivrec  27489  fsumrp0cl  27551  xrge0slmod  27700  cnre2csqlem  27758  tpr2rico  27760  xrge0iifcnv  27781  xrge0iifhom  27785  lmxrge0  27800  esumfsup  27942  esumpcvgval  27950  esumcvg  27958  dya2iocress  28111  dya2iocbrsiga  28112  dya2icobrsiga  28113  dya2icoseg  28114  dya2iocucvr  28121  sxbrsigalem2  28123  orvcgteel  28272  dstrvprob  28276  orvclteel  28277  sgnmul  28347  sgnsub  28349  sgnmulsgn  28354  sgnmulsgp  28355  signstcl  28388  signstf  28389  signstf0  28391  signstfvn  28392  signsvtn0  28393  signstfvneq0  28395  signsvfn  28405  signsvfpn  28408  signsvfnn  28409  cvmliftlem6  28601  cvmliftlem7  28602  cvmliftlem8  28603  cvmliftlem9  28604  cvmliftlem10  28605  cvmliftlem13  28607  sin2h  30013  cos2h  30014  tan2h  30015  heicant  30017  opnmbllem0  30018  mblfinlem1  30019  mblfinlem2  30020  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  dvtanlem  30032  itg2addnclem  30034  itg2addnclem2  30035  itg2gt0cn  30038  ibladdnclem  30039  iblabsnclem  30046  iblabsnc  30047  iblmulc2nc  30048  bddiblnc  30053  ftc1cnnclem  30056  ftc1anclem1  30058  ftc1anclem4  30061  ftc1anclem5  30062  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  ftc2nc  30067  areacirclem1  30075  areacirclem5  30079  areacirc  30080  ivthALT  30121  isbnd3  30248  blbnd  30251  prdsbnd  30257  prdsbnd2  30259  cntotbnd  30260  idomrootle  31121  idomodle  31122  itgpowd  31151  cvgdvgrat  31163  radcnvrat  31164  rfcnpre3  31355  rfcnpre4  31356  nnxrd  31366  lefldiveq  31427  lttri5d  31444  gtnelioc  31455  ltnelicc  31462  iooabslt  31464  gtnelicc  31465  eliooshift  31473  iocopn  31492  eliccelioc  31493  iooshift  31494  icoopn  31497  limciccioolb  31531  lptioo1  31542  limcicciooub  31547  ltmod  31548  lptre2pt  31550  limsupre  31551  limcresiooub  31552  limcresioolb  31553  limcleqr  31554  sinaover2ne0  31571  ioccncflimc  31591  icccncfext  31593  icocncflimc  31595  cncfiooicclem1  31599  cncfiooicc  31600  cncfiooiccre  31601  cncfioobdlem  31602  dvbdfbdioolem1  31625  dvbdfbdioolem2  31626  dvbdfbdioo  31627  ioodvbdlimc1lem1  31628  ioodvbdlimc1lem2  31629  ioodvbdlimc1  31630  ioodvbdlimc2lem  31631  ioodvbdlimc2  31632  ditgeqiooicc  31645  iblsplit  31651  itgcoscmulx  31654  ibliooicc  31656  iblspltprt  31658  itgsincmulx  31659  itgsubsticc  31661  itgioocnicc  31662  iblcncfioo  31663  itgspltprt  31664  itgiccshift  31665  stoweidlem34  31701  stoweidlem52  31719  stirlinglem5  31745  dirkercncflem1  31770  dirkercncflem4  31773  fourierdlem4  31778  fourierdlem10  31784  fourierdlem19  31793  fourierdlem20  31794  fourierdlem24  31798  fourierdlem25  31799  fourierdlem26  31800  fourierdlem27  31801  fourierdlem28  31802  fourierdlem31  31805  fourierdlem32  31806  fourierdlem33  31807  fourierdlem35  31809  fourierdlem37  31811  fourierdlem40  31814  fourierdlem41  31815  fourierdlem43  31817  fourierdlem44  31818  fourierdlem46  31820  fourierdlem47  31821  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem51  31825  fourierdlem52  31826  fourierdlem54  31828  fourierdlem57  31831  fourierdlem59  31833  fourierdlem60  31834  fourierdlem61  31835  fourierdlem62  31836  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem68  31842  fourierdlem69  31843  fourierdlem70  31844  fourierdlem72  31846  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem76  31850  fourierdlem78  31852  fourierdlem79  31853  fourierdlem81  31855  fourierdlem82  31856  fourierdlem84  31858  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem92  31866  fourierdlem93  31867  fourierdlem94  31868  fourierdlem97  31871  fourierdlem100  31874  fourierdlem101  31875  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem107  31881  fourierdlem109  31883  fourierdlem111  31885  fourierdlem112  31886  fourierdlem113  31887  fourierdlem114  31888  sqwvfoura  31896  fouriersw  31899  imo72b2  37598
  Copyright terms: Public domain W3C validator