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

Theorem rpre 10360
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 10355 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3258 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3208 . 2  |-  RR+  C_  RR
43sseli 3176 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   {crab 2547   class class class wbr 4023   RRcr 8736   0cc0 8737    < clt 8867   RR+crp 10354
This theorem is referenced by:  rpxr  10361  rpcn  10362  rpssre  10364  rpge0  10366  rprege0  10368  rprene0  10370  rpaddcl  10374  rpmulcl  10375  rpdivcl  10376  rpgecl  10379  xralrple  10532  xlemul1  10610  iccdil  10773  modcl  10976  mod0  10978  modge0  10980  modlt  10981  modabs  10997  modabs2  10998  modcyc  10999  moddi  11007  modsubdir  11008  modirr  11009  expnlbnd  11231  rennim  11724  cnpart  11725  sqrlem1  11728  sqrlem2  11729  sqrlem4  11731  sqrlem5  11732  sqrlem6  11733  sqrlem7  11734  resqrex  11736  rpsqrcl  11750  sqreulem  11843  eqsqr2d  11852  2clim  12046  reccn2  12070  cn1lem  12071  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  climsup  12143  climcau  12144  caucvgrlem2  12147  iseralt  12157  cvgcmp  12274  cvgcmpce  12276  divrcnv  12311  efgt1  12396  ef01bndlem  12464  sinltx  12469  prmreclem6  12968  stdbdmet  18062  stdbdmopn  18064  met2ndci  18068  ngptgp  18152  reperflem  18323  iccntr  18326  reconnlem2  18332  opnreen  18336  metdseq0  18358  xlebnum  18463  cphsqrcl3  18623  iscmet3lem3  18716  iscmet3lem1  18717  iscmet3lem2  18718  caubl  18733  lmcau  18738  bcthlem4  18749  minveclem3b  18792  minveclem3  18793  ivthlem2  18812  ivthlem3  18813  nulmbl2  18894  opnmbllem  18956  itg2const2  19096  itg2mulclem  19101  dveflem  19326  lhop  19363  dvcnvre  19366  aalioulem2  19713  aaliou  19718  aaliou3lem4  19726  ulmcaulem  19771  ulmcau  19772  ulmcn  19776  itgulm  19784  reeff1o  19823  pilem2  19828  logleb  19957  logcj  19960  argimgt0  19966  logdmnrp  19988  logcnlem3  19991  logcnlem4  19992  advlog  20001  efopnlem1  20003  cxple2  20044  cxplt2  20045  cxple3  20048  cxpcn3  20088  resqrcn  20089  asinneg  20182  atanbndlem  20221  cxplim  20266  cxp2limlem  20270  cxp2lim  20271  cxploglim  20272  cxploglim2  20273  harmoniclbnd  20302  harmonicbnd4  20304  chtrpcl  20413  ppiltx  20415  chtleppi  20449  logfacubnd  20460  logfaclbnd  20461  logfacbnd3  20462  logexprlim  20464  bposlem7  20529  bposlem8  20530  bposlem9  20531  chebbnd1  20621  chtppilim  20624  chto1ub  20625  chpo1ub  20629  vmadivsum  20631  rpvmasumlem  20636  dchrisumlem3  20640  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0  20669  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  mulog2sumlem2  20684  log2sumbnd  20693  selberglem2  20695  selberglem3  20696  selberg  20697  selberg2lem  20699  selberg2  20700  pntrf  20712  pntrmax  20713  pntrsumo1  20714  selbergr  20717  selbergs  20723  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntibndlem1  20738  pntlem3  20758  pntlemp  20759  pntleml  20760  pnt2  20762  padicabvcxp  20781  vacn  21267  nmcvcn  21268  smcnlem  21270  blocnilem  21382  chscllem2  22217  nmcexi  22606  nmcopexi  22607  nmcfnexi  22631  sqsscirc1  23292  probfinmeasbOLD  23631  probfinmeasb  23632  probmeasb  23633  subfacval3  23720  areacirclem2  24925  areacirclem3  24926  areacirclem5  24929  areacirc  24931  cbci  25508  altretop  25600  iintlem1  25610  opnrebl  26235  opnrebl2  26236  blhalfOLD  26472  geomcau  26475  isbnd2  26507  ssbnd  26512  equivbnd  26514  heiborlem7  26541  heiborlem8  26542  bfplem2  26547  rrncmslem  26556  rrnequiv  26559  irrapxlem1  26907  irrapxlem2  26908  irrapxlem3  26909  irrapxlem5  26911  rpexpmord  27033  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climinf  27732  stoweidlem1  27750  stoweidlem3  27752  stoweidlem5  27754  stoweidlem7  27756  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem18  27767  stoweidlem24  27773  stoweidlem25  27774  stoweidlem26  27775  stoweidlem34  27783  stoweidlem41  27790  stoweidlem42  27791  stoweidlem49  27798  stoweidlem51  27800  stoweidlem52  27801  stoweidlem59  27808  stoweidlem60  27809  stoweid  27812  wallispilem4  27817
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166  df-rp 10355
  Copyright terms: Public domain W3C validator