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

Theorem rpre 10511
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 10506 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3344 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3294 . 2  |-  RR+  C_  RR
43sseli 3262 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715   {crab 2632   class class class wbr 4125   RRcr 8883   0cc0 8884    < clt 9014   RR+crp 10505
This theorem is referenced by:  rpxr  10512  rpcn  10513  rpssre  10515  rpge0  10517  rprege0  10519  rprene0  10521  rpaddcl  10525  rpmulcl  10526  rpdivcl  10527  rpgecl  10530  xralrple  10684  xlemul1  10762  iccdil  10926  modcl  11140  mod0  11142  modge0  11144  modlt  11145  modabs  11161  modabs2  11162  modcyc  11163  moddi  11171  modsubdir  11172  modirr  11173  expnlbnd  11396  rennim  11931  cnpart  11932  sqrlem1  11935  sqrlem2  11936  sqrlem4  11938  sqrlem5  11939  sqrlem6  11940  sqrlem7  11941  resqrex  11943  rpsqrcl  11957  sqreulem  12050  eqsqr2d  12059  2clim  12253  reccn2  12277  cn1lem  12278  climsqz  12321  climsqz2  12322  rlimsqzlem  12329  climsup  12350  climcau  12351  caucvgrlem2  12355  iseralt  12365  cvgcmp  12482  cvgcmpce  12484  divrcnv  12519  efgt1  12604  ef01bndlem  12672  sinltx  12677  prmreclem6  13176  stdbdmet  18275  stdbdmopn  18277  met2ndci  18281  ngptgp  18365  reperflem  18537  iccntr  18540  reconnlem2  18546  opnreen  18550  metdseq0  18572  xlebnum  18678  cphsqrcl3  18838  iscmet3lem3  18931  iscmet3lem1  18932  iscmet3lem2  18933  caubl  18948  lmcau  18953  bcthlem4  18964  minveclem3b  19007  minveclem3  19008  ivthlem2  19027  ivthlem3  19028  nulmbl2  19109  opnmbllem  19171  itg2const2  19311  itg2mulclem  19316  dveflem  19541  lhop  19578  dvcnvre  19581  aalioulem2  19928  aaliou  19933  aaliou3lem4  19941  ulmcaulem  19988  ulmcau  19989  ulmcn  19993  itgulm  20002  reeff1o  20041  pilem2  20046  logleb  20176  logcj  20179  argimgt0  20185  logdmnrp  20210  logcnlem3  20213  logcnlem4  20214  advlog  20223  efopnlem1  20225  cxple2  20266  cxplt2  20267  cxple3  20270  cxpcn3  20310  resqrcn  20311  asinneg  20404  atanbndlem  20443  cxplim  20488  cxp2limlem  20492  cxp2lim  20493  cxploglim  20494  cxploglim2  20495  logdiflbnd  20511  harmoniclbnd  20525  harmonicbnd4  20527  chtrpcl  20636  ppiltx  20638  chtleppi  20672  logfacubnd  20683  logfaclbnd  20684  logfacbnd3  20685  logexprlim  20687  bposlem7  20752  bposlem8  20753  bposlem9  20754  chebbnd1  20844  chtppilim  20847  chto1ub  20848  chpo1ub  20852  vmadivsum  20854  rpvmasumlem  20859  dchrisumlem3  20863  dchrvmasumlem2  20870  dchrvmasumiflem1  20873  dchrisum0  20892  mudivsum  20902  mulogsumlem  20903  mulogsum  20904  mulog2sumlem2  20907  log2sumbnd  20916  selberglem2  20918  selberglem3  20919  selberg  20920  selberg2lem  20922  selberg2  20923  pntrf  20935  pntrmax  20936  pntrsumo1  20937  selbergr  20940  selbergs  20946  pntrlog2bndlem4  20952  pntrlog2bndlem5  20953  pntibndlem1  20961  pntlem3  20981  pntlemp  20982  pntleml  20983  pnt2  20985  padicabvcxp  21004  vacn  21701  nmcvcn  21702  smcnlem  21704  blocnilem  21816  chscllem2  22651  nmcexi  23040  nmcopexi  23041  nmcfnexi  23065  sqsscirc1  23782  metustid  23918  cfilucfil  23923  dya2icoseg2  24212  probfinmeasbOLD  24255  probfinmeasb  24256  probmeasb  24257  subfacval3  24444  rprisefaccl  24897  itg2addnclem2  25761  itg2addnc  25762  itg2gt0cn  25763  areacirclem2  25785  areacirclem3  25786  areacirclem5  25789  areacirc  25791  opnrebl  25827  opnrebl2  25828  blhalfOLD  26064  geomcau  26067  isbnd2  26098  ssbnd  26103  equivbnd  26105  heiborlem7  26132  heiborlem8  26133  bfplem2  26138  rrncmslem  26147  rrnequiv  26150  irrapxlem1  26498  irrapxlem2  26499  irrapxlem3  26500  irrapxlem5  26502  rpexpmord  26624  fmul01lt1lem1  27305  fmul01lt1lem2  27306  climinf  27323  stoweidlem1  27341  stoweidlem3  27343  stoweidlem5  27345  stoweidlem7  27347  stoweidlem11  27351  stoweidlem13  27353  stoweidlem14  27354  stoweidlem18  27358  stoweidlem24  27364  stoweidlem25  27365  stoweidlem26  27366  stoweidlem34  27374  stoweidlem41  27381  stoweidlem42  27382  stoweidlem49  27389  stoweidlem51  27391  stoweidlem52  27392  stoweidlem59  27399  stoweidlem60  27400  stoweid  27403  wallispilem4  27408
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-in 3245  df-ss 3252  df-rp 10506
  Copyright terms: Public domain W3C validator