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

Theorem rpre 10356
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
rpre  |-  ( A  e.  RR+  ->  A  e.  RR )

Proof of Theorem rpre
StepHypRef Expression
1 df-rp 10351 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3259 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3209 . 2  |-  RR+  C_  RR
43sseli 3177 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1685   {crab 2548   class class class wbr 4024   RRcr 8732   0cc0 8733    < clt 8863   RR+crp 10350
This theorem is referenced by:  rpxr  10357  rpcn  10358  rpssre  10360  rpge0  10362  rprege0  10364  rprene0  10366  rpaddcl  10370  rpmulcl  10371  rpdivcl  10372  rpgecl  10375  xralrple  10528  xlemul1  10606  iccdil  10769  modcl  10972  mod0  10974  modge0  10976  modlt  10977  modabs  10993  modabs2  10994  modcyc  10995  moddi  11003  modsubdir  11004  modirr  11005  expnlbnd  11227  rennim  11720  cnpart  11721  sqrlem1  11724  sqrlem2  11725  sqrlem4  11727  sqrlem5  11728  sqrlem6  11729  sqrlem7  11730  resqrex  11732  rpsqrcl  11746  sqreulem  11839  eqsqr2d  11848  2clim  12042  reccn2  12066  cn1lem  12067  climsqz  12110  climsqz2  12111  rlimsqzlem  12118  climsup  12139  climcau  12140  caucvgrlem2  12143  iseralt  12153  cvgcmp  12270  cvgcmpce  12272  divrcnv  12307  efgt1  12392  ef01bndlem  12460  sinltx  12465  prmreclem6  12964  stdbdmet  18058  stdbdmopn  18060  met2ndci  18064  ngptgp  18148  reperflem  18319  iccntr  18322  reconnlem2  18328  opnreen  18332  metdseq0  18354  xlebnum  18459  cphsqrcl3  18619  iscmet3lem3  18712  iscmet3lem1  18713  iscmet3lem2  18714  caubl  18729  lmcau  18734  bcthlem4  18745  minveclem3b  18788  minveclem3  18789  ivthlem2  18808  ivthlem3  18809  nulmbl2  18890  opnmbllem  18952  itg2const2  19092  itg2mulclem  19097  dveflem  19322  lhop  19359  dvcnvre  19362  aalioulem2  19709  aaliou  19714  aaliou3lem4  19722  ulmcaulem  19767  ulmcau  19768  ulmcn  19772  itgulm  19780  reeff1o  19819  pilem2  19824  logleb  19953  logcj  19956  argimgt0  19962  logdmnrp  19984  logcnlem3  19987  logcnlem4  19988  advlog  19997  efopnlem1  19999  cxple2  20040  cxplt2  20041  cxple3  20044  cxpcn3  20084  resqrcn  20085  asinneg  20178  atanbndlem  20217  cxplim  20262  cxp2limlem  20266  cxp2lim  20267  cxploglim  20268  cxploglim2  20269  harmoniclbnd  20298  harmonicbnd4  20300  chtrpcl  20409  ppiltx  20411  chtleppi  20445  logfacubnd  20456  logfaclbnd  20457  logfacbnd3  20458  logexprlim  20460  bposlem7  20525  bposlem8  20526  bposlem9  20527  chebbnd1  20617  chtppilim  20620  chto1ub  20621  chpo1ub  20625  vmadivsum  20627  rpvmasumlem  20632  dchrisumlem3  20636  dchrvmasumlem2  20643  dchrvmasumiflem1  20646  dchrisum0  20665  mudivsum  20675  mulogsumlem  20676  mulogsum  20677  mulog2sumlem2  20680  log2sumbnd  20689  selberglem2  20691  selberglem3  20692  selberg  20693  selberg2lem  20695  selberg2  20696  pntrf  20708  pntrmax  20709  pntrsumo1  20710  selbergr  20713  selbergs  20719  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  pntibndlem1  20734  pntlem3  20754  pntlemp  20755  pntleml  20756  pnt2  20758  padicabvcxp  20777  vacn  21261  nmcvcn  21262  smcnlem  21264  blocnilem  21376  chscllem2  22213  nmcexi  22602  nmcopexi  22603  nmcfnexi  22627  subfacval3  23127  areacirclem2  24335  areacirclem3  24336  areacirclem5  24339  areacirc  24341  cbci  24919  altretop  25011  iintlem1  25021  opnrebl  25646  opnrebl2  25647  blhalfOLD  25883  geomcau  25886  isbnd2  25918  ssbnd  25923  equivbnd  25925  heiborlem7  25952  heiborlem8  25953  bfplem2  25958  rrncmslem  25967  rrnequiv  25970  irrapxlem1  26318  irrapxlem2  26319  irrapxlem3  26320  irrapxlem5  26322  rpexpmord  26444  fmul01lt1lem1  27125  fmul01lt1lem2  27126  climinf  27143  stoweidlem1  27161  stoweidlem3  27163  stoweidlem5  27165  stoweidlem7  27167  stoweidlem11  27171  stoweidlem13  27173  stoweidlem14  27174  stoweidlem18  27178  stoweidlem24  27184  stoweidlem25  27185  stoweidlem26  27186  stoweidlem34  27194  stoweidlem41  27201  stoweidlem42  27202  stoweidlem49  27209  stoweidlem51  27211  stoweidlem52  27212  stoweidlem59  27219  stoweidlem60  27220  stoweid  27223  wallispilem4  27228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-in 3160  df-ss 3167  df-rp 10351
  Copyright terms: Public domain W3C validator