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

Theorem rpre 10607
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 10602 . . 3  |-  RR+  =  { x  e.  RR  |  0  <  x }
2 ssrab2 3420 . . 3  |-  { x  e.  RR  |  0  < 
x }  C_  RR
31, 2eqsstri 3370 . 2  |-  RR+  C_  RR
43sseli 3336 1  |-  ( A  e.  RR+  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   {crab 2701   class class class wbr 4204   RRcr 8978   0cc0 8979    < clt 9109   RR+crp 10601
This theorem is referenced by:  rpxr  10608  rpcn  10609  rpssre  10611  rpge0  10613  rprege0  10615  rprene0  10617  rpaddcl  10621  rpmulcl  10622  rpdivcl  10623  rpgecl  10626  xralrple  10780  xlemul1  10858  iccdil  11023  modcl  11241  mod0  11243  modge0  11245  modlt  11246  modabs  11262  modabs2  11263  modcyc  11264  moddi  11272  modsubdir  11273  modirr  11274  expnlbnd  11497  rennim  12032  cnpart  12033  sqrlem1  12036  sqrlem2  12037  sqrlem4  12039  sqrlem5  12040  sqrlem6  12041  sqrlem7  12042  resqrex  12044  rpsqrcl  12058  sqreulem  12151  eqsqr2d  12160  2clim  12354  reccn2  12378  cn1lem  12379  climsqz  12422  climsqz2  12423  rlimsqzlem  12430  climsup  12451  climcau  12452  caucvgrlem2  12456  iseralt  12466  cvgcmp  12583  cvgcmpce  12585  divrcnv  12620  efgt1  12705  ef01bndlem  12773  sinltx  12778  prmreclem6  13277  stdbdmet  18534  stdbdmopn  18536  met2ndci  18540  cfilucfilOLD  18587  cfilucfil  18588  ngptgp  18665  reperflem  18837  iccntr  18840  reconnlem2  18846  opnreen  18850  metdseq0  18872  xlebnum  18978  cphsqrcl3  19138  iscmet3lem3  19231  iscmet3lem1  19232  iscmet3lem2  19233  caubl  19248  lmcau  19253  bcthlem4  19268  minveclem3b  19317  minveclem3  19318  ivthlem2  19337  ivthlem3  19338  nulmbl2  19419  opnmbllem  19481  itg2const2  19621  itg2mulclem  19626  dveflem  19851  lhop  19888  dvcnvre  19891  aalioulem2  20238  aaliou  20243  aaliou3lem4  20251  ulmcaulem  20298  ulmcau  20299  ulmcn  20303  itgulm  20312  reeff1o  20351  pilem2  20356  logleb  20486  logcj  20489  argimgt0  20495  logdmnrp  20520  logcnlem3  20523  logcnlem4  20524  advlog  20533  efopnlem1  20535  cxple2  20576  cxplt2  20577  cxple3  20580  cxpcn3  20620  resqrcn  20621  asinneg  20714  atanbndlem  20753  cxplim  20798  cxp2limlem  20802  cxp2lim  20803  cxploglim  20804  cxploglim2  20805  logdiflbnd  20821  harmoniclbnd  20835  harmonicbnd4  20837  chtrpcl  20946  ppiltx  20948  chtleppi  20982  logfacubnd  20993  logfaclbnd  20994  logfacbnd3  20995  logexprlim  20997  bposlem7  21062  bposlem8  21063  bposlem9  21064  chebbnd1  21154  chtppilim  21157  chto1ub  21158  chpo1ub  21162  vmadivsum  21164  rpvmasumlem  21169  dchrisumlem3  21173  dchrvmasumlem2  21180  dchrvmasumiflem1  21183  dchrisum0  21202  mudivsum  21212  mulogsumlem  21213  mulogsum  21214  mulog2sumlem2  21217  log2sumbnd  21226  selberglem2  21228  selberglem3  21229  selberg  21230  selberg2lem  21232  selberg2  21233  pntrf  21245  pntrmax  21246  pntrsumo1  21247  selbergr  21250  selbergs  21256  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  pntibndlem1  21271  pntlem3  21291  pntlemp  21292  pntleml  21293  pnt2  21295  padicabvcxp  21314  vacn  22178  nmcvcn  22179  smcnlem  22181  blocnilem  22293  chscllem2  23128  nmcexi  23517  nmcopexi  23518  nmcfnexi  23542  pnfinf  24241  sqsscirc1  24294  dya2icoseg2  24616  probfinmeasbOLD  24674  probfinmeasb  24675  subfacval3  24863  rprisefaccl  25328  mblfinlem  26190  itg2addnclem  26202  itg2addnclem2  26203  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  areacirclem2  26228  areacirclem3  26229  areacirclem5  26232  areacirc  26234  opnrebl  26260  opnrebl2  26261  geomcau  26402  isbnd2  26429  ssbnd  26434  heiborlem7  26463  heiborlem8  26464  bfplem2  26469  rrncmslem  26478  rrnequiv  26481  irrapxlem1  26822  irrapxlem2  26823  irrapxlem3  26824  irrapxlem5  26826  rpexpmord  26948  climinf  27646  stoweidlem7  27670  ltdifltdiv  28054  2submod  28058  modid0  28065
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326  df-rp 10602
  Copyright terms: Public domain W3C validator