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

Theorem rexrd 10669
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
StepHypRef Expression
1 ressxr 10663 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3944 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  cr 10514  *cxr 10652
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-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-un 3918  df-in 3920  df-ss 3930  df-xr 10657
This theorem is referenced by:  xnn0xr  11951  rpxr  12377  rpxrd  12411  max0sub  12568  qextltlem  12574  xralrple  12577  xnegcl  12585  xaddf  12596  xnn0lem1lt  12616  xnn0lenn0nn0  12617  xmulf  12644  xadddi  12667  xrub  12684  supxrre  12699  infxrre  12708  ixxub  12738  ixxlb  12739  ioo0  12742  ico0  12763  ioc0  12764  iooshf  12795  icoshftf1o  12843  supicc  12870  supiccub  12871  supicclub  12872  xnn0xrge0  12875  ssfzunsn  12937  addmodid  13271  hashnnn0genn0  13688  hashunsnggt  13740  elicc4abs  14659  caucvgrlem  15009  fprodge1  15329  pcxcl  16175  pcdvdsb  16183  pcaddlem  16202  ramcl2lem  16323  ramlb  16333  0ram  16334  setsstruct  16502  prdsxmetlem  22954  xblss2ps  22987  xblss2  22988  blss2ps  22989  blss2  22990  blhalf  22991  metustto  23139  metustexhalf  23142  nmoi  23313  nmoix  23314  nmoi2  23315  nmoleub  23316  qdensere  23354  cnblcld  23359  ioo2blex  23378  tgioo  23380  blcvx  23382  zcld  23397  recld2  23398  iccntr  23405  icccmplem1  23406  reconnlem1  23410  reconnlem2  23411  opnreen  23415  metnrmlem3  23445  icoopnst  23523  iocopnst  23524  cnheibor  23539  lebnumii  23550  nmoleub2lem  23698  lmnn  23846  iscau3  23861  minveclem4  24015  ivthlem1  24034  ivthlem2  24035  ivthlem3  24036  ivth2  24038  ivthle  24039  ivthle2  24040  ivthicc  24041  evthicc  24042  cniccbdd  24044  ovolgelb  24063  ovollb2lem  24071  ovolunlem1  24080  ovoliunlem1  24085  ovoliunlem2  24086  ovoliun  24088  ovolscalem1  24096  ovolicc1  24099  ovolicc2lem4  24103  ovolicc2lem5  24104  ovolicc2  24105  ovolicc  24106  nulmbl2  24119  voliunlem2  24134  ioombl1lem4  24144  ioorcl2  24155  uniioombllem1  24164  uniioombllem2a  24165  uniioombllem3  24168  dyaddisjlem  24178  dyadmaxlem  24180  opnmbllem  24184  volivth  24190  vitalilem4  24194  mbfmulc2lem  24230  mbfmax  24232  mbfposr  24235  ismbf3d  24237  mbfaddlem  24243  mbflimsup  24249  mbfi1fseqlem4  24301  itg2lcl  24310  xrge0f  24314  itg2itg1  24319  itg2const2  24324  itg2seq  24325  itg2uba  24326  itg2lea  24327  itg2mulclem  24329  itg2mulc  24330  itg2splitlem  24331  itg2split  24332  itg2monolem2  24334  itg2monolem3  24335  itg2mono  24336  itg2gt0  24343  itg2cnlem1  24344  itg2cnlem2  24345  itg2cn  24346  iblss  24387  itgle  24392  itgeqa  24396  itgioo  24398  ibladdlem  24402  iblabs  24411  iblabsr  24412  iblmulc2  24413  itgsplit  24418  itgspliticc  24419  itgsplitioo  24420  bddmulibl  24421  bddiblnc  24424  ditgcl  24440  ditgswap  24441  ditgsplitlem  24442  dvferm1lem  24566  dvferm2lem  24568  dvferm  24570  rollelem  24571  rolle  24572  cmvth  24573  mvth  24574  dvlip  24575  dvlip2  24577  c1liplem1  24578  c1lip1  24579  dveq0  24582  dvgt0lem1  24584  dvivthlem1  24590  dvivth  24592  lhop1lem  24595  lhop1  24596  lhop2  24597  lhop  24598  dvcnvrelem1  24599  dvcnvre  24601  dvcvx  24602  dvfsumle  24603  dvfsumge  24604  dvfsumabs  24605  dvfsumlem2  24609  dvfsumlem3  24610  dvfsumlem4  24611  dvfsumrlimge0  24612  dvfsumrlim2  24614  ftc1lem1  24617  ftc1lem2  24618  ftc1a  24619  ftc1lem4  24621  ftc2  24626  ftc2ditglem  24627  itgparts  24629  itgsubstlem  24630  itgsubst  24631  itgpowd  24632  degltlem1  24652  deg1ge  24678  coe1mul3  24679  deg1sublt  24690  deg1mul2  24694  deg1tmle  24697  deg1tm  24698  plypf1  24788  taylfvallem1  24931  tayl0  24936  pserulm  24996  psercnlem1  24999  pserdvlem1  25001  pserdvlem2  25002  abelthlem3  25007  abelth  25015  efcvx  25023  logno1  25206  logtayl  25230  xrlimcnp  25533  logfacbnd3  25786  log2sumbnd  26107  pntpbnd2  26150  pntibndlem3  26155  ttgcontlem1  26658  nmooge0  28529  nmoub3i  28535  isblo3i  28563  ubthlem1  28632  minvecolem4  28642  nmopge0  29673  nmfnge0  29689  nmophmi  29793  branmfn  29867  xaddeq0  30464  xlt2addrd  30469  xmulcand  30584  xreceu  30585  xdivrec  30590  fsumrp0cl  30690  xrge0slmod  30925  cnre2csqlem  31161  tpr2rico  31163  xrge0iifcnv  31184  xrge0iifhom  31188  lmxrge0  31203  esumfsup  31337  esumpcvgval  31345  esumcvg  31353  dya2iocress  31540  dya2iocbrsiga  31541  dya2icobrsiga  31542  dya2icoseg  31543  dya2iocucvr  31550  sxbrsigalem2  31552  omssubaddlem  31565  omssubadd  31566  orvcgteel  31733  dstrvprob  31737  orvclteel  31738  sgnmul  31808  sgnsub  31810  sgnmulsgn  31815  sgnmulsgp  31816  signstcl  31843  signstf  31844  signstf0  31846  signstfvn  31847  signsvtn0  31848  signsvfn  31860  signsvfpn  31863  signsvfnn  31864  ftc2re  31877  cvmliftlem6  32545  cvmliftlem7  32546  cvmliftlem8  32547  cvmliftlem9  32548  cvmliftlem10  32549  cvmliftlem13  32551  ivthALT  33691  iooelexlt  34660  relowlssretop  34661  relowlpssretop  34662  sin2h  34923  cos2h  34924  tan2h  34925  poimirlem30  34963  poimir  34966  heicant  34968  opnmbllem0  34969  mblfinlem1  34970  mblfinlem2  34971  mblfinlem3  34972  mblfinlem4  34973  ismblfin  34974  itg2addnclem  34984  itg2addnclem2  34985  itg2gt0cn  34988  ibladdnclem  34989  iblabsnclem  34996  iblabsnc  34997  iblmulc2nc  34998  ftc1cnnclem  35004  ftc1anclem1  35006  ftc1anclem4  35009  ftc1anclem5  35010  ftc1anclem6  35011  ftc1anclem7  35012  ftc1anclem8  35013  ftc1anc  35014  ftc2nc  35015  areacirclem1  35021  areacirclem5  35025  areacirc  35026  isbnd3  35098  blbnd  35101  prdsbnd  35107  prdsbnd2  35109  cntotbnd  35110  idomrootle  39932  idomodle  39933  imo72b2  40660  cvgdvgrat  40800  radcnvrat  40801  rfcnpre3  41445  rfcnpre4  41446  nnxrd  41454  absfico  41635  lefldiveq  41713  lttri5d  41720  supxrgere  41755  supxrgelem  41759  supxrge  41760  xralrple2  41776  infxr  41789  infleinflem1  41792  infleinflem2  41793  xralrple4  41795  xralrple3  41796  xrralrecnnle  41807  xrralrecnnge  41816  supxrunb3  41826  unb2ltle  41843  zxrd  41883  gtnelioc  41919  ltnelicc  41925  iooabslt  41927  gtnelicc  41928  eliooshift  41934  iocopn  41948  eliccelioc  41949  iooshift  41950  icoopn  41953  ge0lere  41960  iooiinicc  41970  sqrlearg  41981  iooiinioc  41984  uzinico  41988  preimaiocmnf  41989  uzubioo  41995  fsumge0cl  42006  limciccioolb  42054  lptioo1  42065  limcicciooub  42070  ltmod  42071  lptre2pt  42073  limsupre  42074  limcresiooub  42075  limcresioolb  42076  limcleqr  42077  limsupresico  42133  limsuppnfdlem  42134  limsupub  42137  limsupequzlem  42155  limsupre2lem  42157  limsupre3lem  42165  limsupvaluz2  42171  supcnvlimsup  42173  liminfresico  42204  limsup10exlem  42205  liminflelimsuplem  42208  limsupgtlem  42210  liminfval4  42222  liminfvaluz2  42228  limsupvaluz4  42233  liminflimsupclim  42240  xlimxrre  42264  xlimmnfvlem1  42265  xlimmnfv  42267  xlimpnfvlem1  42269  xlimpnfv  42271  sinaover2ne0  42301  ioccncflimc  42318  icccncfext  42320  icocncflimc  42322  cncfiooicclem1  42326  cncfiooicc  42327  cncfiooiccre  42328  cncfioobdlem  42329  dvbdfbdioolem1  42361  dvbdfbdioolem2  42362  dvbdfbdioo  42363  ioodvbdlimc1lem1  42364  ioodvbdlimc1lem2  42365  ioodvbdlimc1  42366  ioodvbdlimc2lem  42367  ioodvbdlimc2  42368  ditgeqiooicc  42393  iblsplit  42399  itgcoscmulx  42402  ibliooicc  42404  iblspltprt  42406  itgsincmulx  42407  itgsubsticc  42409  itgioocnicc  42410  iblcncfioo  42411  itgspltprt  42412  itgiccshift  42413  volioore  42423  voliooico  42425  voliooicof  42429  voliccico  42432  stoweidlem34  42467  stoweidlem52  42485  stirlinglem5  42511  dirkercncflem1  42536  dirkercncflem4  42539  fourierdlem4  42544  fourierdlem10  42550  fourierdlem19  42559  fourierdlem20  42560  fourierdlem24  42564  fourierdlem25  42565  fourierdlem26  42566  fourierdlem27  42567  fourierdlem28  42568  fourierdlem31  42571  fourierdlem32  42572  fourierdlem33  42573  fourierdlem35  42575  fourierdlem37  42577  fourierdlem40  42580  fourierdlem41  42581  fourierdlem43  42583  fourierdlem44  42584  fourierdlem46  42585  fourierdlem47  42586  fourierdlem48  42587  fourierdlem49  42588  fourierdlem50  42589  fourierdlem51  42590  fourierdlem52  42591  fourierdlem54  42593  fourierdlem57  42596  fourierdlem59  42598  fourierdlem60  42599  fourierdlem61  42600  fourierdlem62  42601  fourierdlem63  42602  fourierdlem64  42603  fourierdlem65  42604  fourierdlem68  42607  fourierdlem69  42608  fourierdlem70  42609  fourierdlem72  42611  fourierdlem73  42612  fourierdlem74  42613  fourierdlem75  42614  fourierdlem76  42615  fourierdlem78  42617  fourierdlem79  42618  fourierdlem81  42620  fourierdlem82  42621  fourierdlem84  42623  fourierdlem89  42628  fourierdlem90  42629  fourierdlem91  42630  fourierdlem92  42631  fourierdlem93  42632  fourierdlem94  42633  fourierdlem97  42636  fourierdlem100  42639  fourierdlem101  42640  fourierdlem102  42641  fourierdlem103  42642  fourierdlem104  42643  fourierdlem107  42646  fourierdlem109  42648  fourierdlem111  42650  fourierdlem112  42651  fourierdlem113  42652  fourierdlem114  42653  sqwvfoura  42661  fouriersw  42664  etransclem23  42690  etransclem46  42713  qndenserrnbllem  42727  rrxsnicc  42733  ioorrnopnlem  42737  ioorrnopnxrlem  42739  salgencntex  42774  sge0cl  42811  sge0fsum  42817  sge0iunmptlemre  42845  sge0isum  42857  sge0ad2en  42861  sge0xaddlem1  42863  sge0xaddlem2  42864  sge0reuz  42877  voliunsge0lem  42902  meassre  42907  omessre  42940  omeiunltfirp  42949  hoissre  42974  hoiprodcl  42977  ovnsubaddlem1  43000  hoiprodcl3  43010  hoidmvcl  43012  hsphoidmvle2  43015  hsphoidmvle  43016  sge0hsphoire  43019  hoidmv1lelem1  43021  hoidmv1lelem2  43022  hoidmv1lelem3  43023  hoidmv1le  43024  hoidmvlelem1  43025  hoidmvlelem2  43026  hoidmvlelem3  43027  hoidmvlelem4  43028  ovnhoilem1  43031  ovnhoilem2  43032  ovnhoi  43033  ovnlecvr2  43040  hspdifhsp  43046  hoidifhspdmvle  43050  hoiqssbllem1  43052  hoiqssbllem2  43053  hoiqssbllem3  43054  hspmbllem1  43056  hspmbllem2  43057  volicorege0  43067  ovolval5lem1  43082  ovolval5lem2  43083  iinhoiicclem  43103  iinhoiicc  43104  iunhoiioolem  43105  iunhoiioo  43106  vonioolem2  43111  vonicclem2  43114  vonsn  43121  pimltmnf2  43127  pimconstlt0  43130  pimgtpnf2  43133  salpreimagelt  43134  salpreimalegt  43136  preimageiingt  43146  preimaleiinlt  43147  pimrecltneg  43149  issmflem  43152  issmflelem  43169  issmfgtlem  43180  issmfgt  43181  smfaddlem1  43187  issmfgelem  43193  issmfge  43194  smfpimioompt  43209  smfresal  43211  smfrec  43212  smfmullem1  43214  smfmullem2  43215  smfmullem3  43216  smfmullem4  43217  smfpimbor1lem1  43221  smfsuplem1  43233  smflimsuplem4  43245  smfliminflem  43252  bgoldbtbnd  44119  eenglngeehlnmlem2  44912
  Copyright terms: Public domain W3C validator