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

Theorem rpre 10362
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 10357 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3260 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3210 . 2  |-  RR+  C_  RR
43sseli 3178 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   {crab 2549   class class class wbr 4025   RRcr 8738   0cc0 8739    < clt 8869   RR+crp 10356
This theorem is referenced by:  rpxr  10363  rpcn  10364  rpssre  10366  rpge0  10368  rprege0  10370  rprene0  10372  rpaddcl  10376  rpmulcl  10377  rpdivcl  10378  rpgecl  10381  xralrple  10534  xlemul1  10612  iccdil  10775  modcl  10978  mod0  10980  modge0  10982  modlt  10983  modabs  10999  modabs2  11000  modcyc  11001  moddi  11009  modsubdir  11010  modirr  11011  expnlbnd  11233  rennim  11726  cnpart  11727  sqrlem1  11730  sqrlem2  11731  sqrlem4  11733  sqrlem5  11734  sqrlem6  11735  sqrlem7  11736  resqrex  11738  rpsqrcl  11752  sqreulem  11845  eqsqr2d  11854  2clim  12048  reccn2  12072  cn1lem  12073  climsqz  12116  climsqz2  12117  rlimsqzlem  12124  climsup  12145  climcau  12146  caucvgrlem2  12149  iseralt  12159  cvgcmp  12276  cvgcmpce  12278  divrcnv  12313  efgt1  12398  ef01bndlem  12466  sinltx  12471  prmreclem6  12970  stdbdmet  18064  stdbdmopn  18066  met2ndci  18070  ngptgp  18154  reperflem  18325  iccntr  18328  reconnlem2  18334  opnreen  18338  metdseq0  18360  xlebnum  18465  cphsqrcl3  18625  iscmet3lem3  18718  iscmet3lem1  18719  iscmet3lem2  18720  caubl  18735  lmcau  18740  bcthlem4  18751  minveclem3b  18794  minveclem3  18795  ivthlem2  18814  ivthlem3  18815  nulmbl2  18896  opnmbllem  18958  itg2const2  19098  itg2mulclem  19103  dveflem  19328  lhop  19365  dvcnvre  19368  aalioulem2  19715  aaliou  19720  aaliou3lem4  19728  ulmcaulem  19773  ulmcau  19774  ulmcn  19778  itgulm  19786  reeff1o  19825  pilem2  19830  logleb  19959  logcj  19962  argimgt0  19968  logdmnrp  19990  logcnlem3  19993  logcnlem4  19994  advlog  20003  efopnlem1  20005  cxple2  20046  cxplt2  20047  cxple3  20050  cxpcn3  20090  resqrcn  20091  asinneg  20184  atanbndlem  20223  cxplim  20268  cxp2limlem  20272  cxp2lim  20273  cxploglim  20274  cxploglim2  20275  harmoniclbnd  20304  harmonicbnd4  20306  chtrpcl  20415  ppiltx  20417  chtleppi  20451  logfacubnd  20462  logfaclbnd  20463  logfacbnd3  20464  logexprlim  20466  bposlem7  20531  bposlem8  20532  bposlem9  20533  chebbnd1  20623  chtppilim  20626  chto1ub  20627  chpo1ub  20631  vmadivsum  20633  rpvmasumlem  20638  dchrisumlem3  20642  dchrvmasumlem2  20649  dchrvmasumiflem1  20652  dchrisum0  20671  mudivsum  20681  mulogsumlem  20682  mulogsum  20683  mulog2sumlem2  20686  log2sumbnd  20695  selberglem2  20697  selberglem3  20698  selberg  20699  selberg2lem  20701  selberg2  20702  pntrf  20714  pntrmax  20715  pntrsumo1  20716  selbergr  20719  selbergs  20725  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntibndlem1  20740  pntlem3  20760  pntlemp  20761  pntleml  20762  pnt2  20764  padicabvcxp  20783  vacn  21269  nmcvcn  21270  smcnlem  21272  blocnilem  21384  chscllem2  22219  nmcexi  22608  nmcopexi  22609  nmcfnexi  22633  sqsscirc1  23294  probfinmeasbOLD  23633  probfinmeasb  23634  probmeasb  23635  subfacval3  23722  itg2addnclem2  24934  itg2addnc  24935  areacirclem2  24936  areacirclem3  24937  areacirclem5  24940  areacirc  24942  cbci  25519  altretop  25611  iintlem1  25621  opnrebl  26246  opnrebl2  26247  blhalfOLD  26483  geomcau  26486  isbnd2  26518  ssbnd  26523  equivbnd  26525  heiborlem7  26552  heiborlem8  26553  bfplem2  26558  rrncmslem  26567  rrnequiv  26570  irrapxlem1  26918  irrapxlem2  26919  irrapxlem3  26920  irrapxlem5  26922  rpexpmord  27044  fmul01lt1lem1  27725  fmul01lt1lem2  27726  climinf  27743  stoweidlem1  27761  stoweidlem3  27763  stoweidlem5  27765  stoweidlem7  27767  stoweidlem11  27771  stoweidlem13  27773  stoweidlem14  27774  stoweidlem18  27778  stoweidlem24  27784  stoweidlem25  27785  stoweidlem26  27786  stoweidlem34  27794  stoweidlem41  27801  stoweidlem42  27802  stoweidlem49  27809  stoweidlem51  27811  stoweidlem52  27812  stoweidlem59  27819  stoweidlem60  27820  stoweid  27823  wallispilem4  27828
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-in 3161  df-ss 3168  df-rp 10357
  Copyright terms: Public domain W3C validator