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

Theorem rpre 10376
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 10371 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3271 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3221 . 2  |-  RR+  C_  RR
43sseli 3189 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   {crab 2560   class class class wbr 4039   RRcr 8752   0cc0 8753    < clt 8883   RR+crp 10370
This theorem is referenced by:  rpxr  10377  rpcn  10378  rpssre  10380  rpge0  10382  rprege0  10384  rprene0  10386  rpaddcl  10390  rpmulcl  10391  rpdivcl  10392  rpgecl  10395  xralrple  10548  xlemul1  10626  iccdil  10789  modcl  10992  mod0  10994  modge0  10996  modlt  10997  modabs  11013  modabs2  11014  modcyc  11015  moddi  11023  modsubdir  11024  modirr  11025  expnlbnd  11247  rennim  11740  cnpart  11741  sqrlem1  11744  sqrlem2  11745  sqrlem4  11747  sqrlem5  11748  sqrlem6  11749  sqrlem7  11750  resqrex  11752  rpsqrcl  11766  sqreulem  11859  eqsqr2d  11868  2clim  12062  reccn2  12086  cn1lem  12087  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  climsup  12159  climcau  12160  caucvgrlem2  12163  iseralt  12173  cvgcmp  12290  cvgcmpce  12292  divrcnv  12327  efgt1  12412  ef01bndlem  12480  sinltx  12485  prmreclem6  12984  stdbdmet  18078  stdbdmopn  18080  met2ndci  18084  ngptgp  18168  reperflem  18339  iccntr  18342  reconnlem2  18348  opnreen  18352  metdseq0  18374  xlebnum  18479  cphsqrcl3  18639  iscmet3lem3  18732  iscmet3lem1  18733  iscmet3lem2  18734  caubl  18749  lmcau  18754  bcthlem4  18765  minveclem3b  18808  minveclem3  18809  ivthlem2  18828  ivthlem3  18829  nulmbl2  18910  opnmbllem  18972  itg2const2  19112  itg2mulclem  19117  dveflem  19342  lhop  19379  dvcnvre  19382  aalioulem2  19729  aaliou  19734  aaliou3lem4  19742  ulmcaulem  19787  ulmcau  19788  ulmcn  19792  itgulm  19800  reeff1o  19839  pilem2  19844  logleb  19973  logcj  19976  argimgt0  19982  logdmnrp  20004  logcnlem3  20007  logcnlem4  20008  advlog  20017  efopnlem1  20019  cxple2  20060  cxplt2  20061  cxple3  20064  cxpcn3  20104  resqrcn  20105  asinneg  20198  atanbndlem  20237  cxplim  20282  cxp2limlem  20286  cxp2lim  20287  cxploglim  20288  cxploglim2  20289  harmoniclbnd  20318  harmonicbnd4  20320  chtrpcl  20429  ppiltx  20431  chtleppi  20465  logfacubnd  20476  logfaclbnd  20477  logfacbnd3  20478  logexprlim  20480  bposlem7  20545  bposlem8  20546  bposlem9  20547  chebbnd1  20637  chtppilim  20640  chto1ub  20641  chpo1ub  20645  vmadivsum  20647  rpvmasumlem  20652  dchrisumlem3  20656  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  dchrisum0  20685  mudivsum  20695  mulogsumlem  20696  mulogsum  20697  mulog2sumlem2  20700  log2sumbnd  20709  selberglem2  20711  selberglem3  20712  selberg  20713  selberg2lem  20715  selberg2  20716  pntrf  20728  pntrmax  20729  pntrsumo1  20730  selbergr  20733  selbergs  20739  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntibndlem1  20754  pntlem3  20774  pntlemp  20775  pntleml  20776  pnt2  20778  padicabvcxp  20797  vacn  21283  nmcvcn  21284  smcnlem  21286  blocnilem  21398  chscllem2  22233  nmcexi  22622  nmcopexi  22623  nmcfnexi  22647  sqsscirc1  23307  probfinmeasbOLD  23646  probfinmeasb  23647  probmeasb  23648  subfacval3  23735  faclimlem5  24121  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  areacirclem2  25028  areacirclem3  25029  areacirclem5  25032  areacirc  25034  cbci  25611  altretop  25703  iintlem1  25713  opnrebl  26338  opnrebl2  26339  blhalfOLD  26575  geomcau  26578  isbnd2  26610  ssbnd  26615  equivbnd  26617  heiborlem7  26644  heiborlem8  26645  bfplem2  26650  rrncmslem  26659  rrnequiv  26662  irrapxlem1  27010  irrapxlem2  27011  irrapxlem3  27012  irrapxlem5  27014  rpexpmord  27136  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climinf  27835  stoweidlem1  27853  stoweidlem3  27855  stoweidlem5  27857  stoweidlem7  27859  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem18  27870  stoweidlem24  27876  stoweidlem25  27877  stoweidlem26  27878  stoweidlem34  27886  stoweidlem41  27893  stoweidlem42  27894  stoweidlem49  27901  stoweidlem51  27903  stoweidlem52  27904  stoweidlem59  27911  stoweidlem60  27912  stoweid  27915  wallispilem4  27920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-in 3172  df-ss 3179  df-rp 10371
  Copyright terms: Public domain W3C validator