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

Theorem rpre 10618
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 10613 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3428 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3378 . 2  |-  RR+  C_  RR
43sseli 3344 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   {crab 2709   class class class wbr 4212   RRcr 8989   0cc0 8990    < clt 9120   RR+crp 10612
This theorem is referenced by:  rpxr  10619  rpcn  10620  rpssre  10622  rpge0  10624  rprege0  10626  rprene0  10628  rpaddcl  10632  rpmulcl  10633  rpdivcl  10634  rpgecl  10637  xralrple  10791  xlemul1  10869  iccdil  11034  modcl  11253  mod0  11255  modge0  11257  modlt  11258  modabs  11274  modabs2  11275  modcyc  11276  moddi  11284  modsubdir  11285  modirr  11286  expnlbnd  11509  rennim  12044  cnpart  12045  sqrlem1  12048  sqrlem2  12049  sqrlem4  12051  sqrlem5  12052  sqrlem6  12053  sqrlem7  12054  resqrex  12056  rpsqrcl  12070  sqreulem  12163  eqsqr2d  12172  2clim  12366  reccn2  12390  cn1lem  12391  climsqz  12434  climsqz2  12435  rlimsqzlem  12442  climsup  12463  climcau  12464  caucvgrlem2  12468  iseralt  12478  cvgcmp  12595  cvgcmpce  12597  divrcnv  12632  efgt1  12717  ef01bndlem  12785  sinltx  12790  prmreclem6  13289  stdbdmet  18546  stdbdmopn  18548  met2ndci  18552  cfilucfilOLD  18599  cfilucfil  18600  ngptgp  18677  reperflem  18849  iccntr  18852  reconnlem2  18858  opnreen  18862  metdseq0  18884  xlebnum  18990  cphsqrcl3  19150  iscmet3lem3  19243  iscmet3lem1  19244  iscmet3lem2  19245  caubl  19260  lmcau  19265  bcthlem4  19280  minveclem3b  19329  minveclem3  19330  ivthlem2  19349  ivthlem3  19350  nulmbl2  19431  opnmbllem  19493  itg2const2  19633  itg2mulclem  19638  dveflem  19863  lhop  19900  dvcnvre  19903  aalioulem2  20250  aaliou  20255  aaliou3lem4  20263  ulmcaulem  20310  ulmcau  20311  ulmcn  20315  itgulm  20324  reeff1o  20363  pilem2  20368  logleb  20498  logcj  20501  argimgt0  20507  logdmnrp  20532  logcnlem3  20535  logcnlem4  20536  advlog  20545  efopnlem1  20547  cxple2  20588  cxplt2  20589  cxple3  20592  cxpcn3  20632  resqrcn  20633  asinneg  20726  atanbndlem  20765  cxplim  20810  cxp2limlem  20814  cxp2lim  20815  cxploglim  20816  cxploglim2  20817  logdiflbnd  20833  harmoniclbnd  20847  harmonicbnd4  20849  chtrpcl  20958  ppiltx  20960  chtleppi  20994  logfacubnd  21005  logfaclbnd  21006  logfacbnd3  21007  logexprlim  21009  bposlem7  21074  bposlem8  21075  bposlem9  21076  chebbnd1  21166  chtppilim  21169  chto1ub  21170  chpo1ub  21174  vmadivsum  21176  rpvmasumlem  21181  dchrisumlem3  21185  dchrvmasumlem2  21192  dchrvmasumiflem1  21195  dchrisum0  21214  mudivsum  21224  mulogsumlem  21225  mulogsum  21226  mulog2sumlem2  21229  log2sumbnd  21238  selberglem2  21240  selberglem3  21241  selberg  21242  selberg2lem  21244  selberg2  21245  pntrf  21257  pntrmax  21258  pntrsumo1  21259  selbergr  21262  selbergs  21268  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntibndlem1  21283  pntlem3  21303  pntlemp  21304  pntleml  21305  pnt2  21307  padicabvcxp  21326  vacn  22190  nmcvcn  22191  smcnlem  22193  blocnilem  22305  chscllem2  23140  nmcexi  23529  nmcopexi  23530  nmcfnexi  23554  pnfinf  24253  sqsscirc1  24306  dya2icoseg2  24628  probfinmeasbOLD  24686  probfinmeasb  24687  subfacval3  24875  rprisefaccl  25339  opnmbllem0  26242  itg2addnclem  26256  itg2addnclem2  26257  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem5  26284  ftc1anclem7  26286  ftc1anc  26288  areacirclem1  26292  areacirclem4  26295  areacirc  26297  opnrebl  26323  opnrebl2  26324  geomcau  26465  isbnd2  26492  ssbnd  26497  heiborlem7  26526  heiborlem8  26527  bfplem2  26532  rrncmslem  26541  rrnequiv  26544  irrapxlem1  26885  irrapxlem2  26886  irrapxlem3  26887  irrapxlem5  26889  rpexpmord  27011  climinf  27708  stoweidlem7  27732  ltdifltdiv  28148  2submod  28152  modid0  28159  2txmodxeq0  28162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-in 3327  df-ss 3334  df-rp 10613
  Copyright terms: Public domain W3C validator