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

Theorem rpre 11877
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
rpre (𝐴 ∈ ℝ+𝐴 ∈ ℝ)

Proof of Theorem rpre
StepHypRef Expression
1 df-rp 11871 . . 3 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2 ssrab2 3720 . . 3 {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
31, 2eqsstri 3668 . 2 + ⊆ ℝ
43sseli 3632 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  {crab 2945   class class class wbr 4685  cr 9973  0cc0 9974   < clt 10112  +crp 11870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-in 3614  df-ss 3621  df-rp 11871
This theorem is referenced by:  rpxr  11878  rpcn  11879  rpssre  11881  rpge0  11883  rprege0  11885  rprene0  11887  rpaddcl  11892  rpmulcl  11893  rpdivcl  11894  rpgecl  11897  ledivge1le  11939  addlelt  11980  xralrple  12074  xlemul1  12158  infmrp1  12212  iccdil  12348  ltdifltdiv  12675  modcl  12712  mod0  12715  mulmod0  12716  modge0  12718  modlt  12719  modid0  12736  modabs  12743  modabs2  12744  modcyc  12745  modmuladd  12752  modmuladdnn0  12754  modltm1p1mod  12762  2txmodxeq0  12770  2submod  12771  moddi  12778  modsubdir  12779  modeqmodmin  12780  modirr  12781  expnlbnd  13034  rennim  14023  cnpart  14024  sqrlem1  14027  sqrlem2  14028  sqrlem4  14030  sqrlem5  14031  sqrlem6  14032  sqrlem7  14033  resqrex  14035  rpsqrtcl  14049  sqreulem  14143  eqsqrt2d  14152  2clim  14347  reccn2  14371  cn1lem  14372  climsqz  14415  climsqz2  14416  rlimsqzlem  14423  climsup  14444  climcau  14445  caucvgrlem2  14449  iseralt  14459  cvgcmp  14592  cvgcmpce  14594  divrcnv  14628  rprisefaccl  14798  efgt1  14890  ef01bndlem  14958  sinltx  14963  stdbdmet  22368  stdbdmopn  22370  met2ndci  22374  cfilucfil  22411  ngptgp  22487  reperflem  22668  iccntr  22671  reconnlem2  22677  opnreen  22681  metdseq0  22704  xlebnum  22811  cphsqrtcl3  23033  iscmet3lem3  23134  iscmet3lem1  23135  iscmet3lem2  23136  caubl  23152  lmcau  23157  bcthlem4  23170  minveclem3b  23245  minveclem3  23246  ivthlem2  23267  ivthlem3  23268  nulmbl2  23350  opnmbllem  23415  itg2const2  23553  itg2mulclem  23558  dveflem  23787  lhop  23824  dvcnvre  23827  aalioulem2  24133  aaliou  24138  aaliou3lem4  24146  ulmcaulem  24193  ulmcau  24194  ulmcn  24198  itgulm  24207  reeff1o  24246  pilem2  24251  logleb  24394  logcj  24397  argimgt0  24403  logdmnrp  24432  logcnlem3  24435  logcnlem4  24436  advlog  24445  efopnlem1  24447  cxple2  24488  cxplt2  24489  cxple3  24492  cxpcn3  24534  resqrtcn  24535  relogbf  24574  asinneg  24658  atanbndlem  24697  cxplim  24743  cxp2limlem  24747  cxp2lim  24748  cxploglim  24749  cxploglim2  24750  logdiflbnd  24766  harmoniclbnd  24780  harmonicbnd4  24782  chtrpcl  24946  ppiltx  24948  chtleppi  24980  logfacubnd  24991  logfaclbnd  24992  logfacbnd3  24993  logexprlim  24995  bposlem7  25060  bposlem8  25061  bposlem9  25062  chebbnd1  25206  chtppilim  25209  chto1ub  25210  chpo1ub  25214  vmadivsum  25216  rpvmasumlem  25221  dchrisumlem3  25225  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0  25254  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  mulog2sumlem2  25269  log2sumbnd  25278  selberglem2  25280  selberglem3  25281  selberg  25282  selberg2lem  25284  selberg2  25285  pntrf  25297  pntrmax  25298  pntrsumo1  25299  selbergr  25302  selbergs  25308  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntibndlem1  25323  pntlem3  25343  pntlemp  25344  pntleml  25345  pnt2  25347  padicabvcxp  25366  vacn  27677  nmcvcn  27678  smcnlem  27680  blocnilem  27787  chscllem2  28625  nmcexi  29013  nmcopexi  29014  nmcfnexi  29038  dp2ltsuc  29721  dpval3rp  29736  dplti  29741  dpgti  29742  dpexpp1  29744  dpadd2  29746  pnfinf  29865  sqsscirc1  30082  dya2icoseg2  30468  probfinmeasbOLD  30618  probfinmeasb  30619  divsqrtid  30800  logdivsqrle  30856  hgt750lem2  30858  subfacval3  31297  opnrebl  32440  opnrebl2  32441  taupilem1  33297  opnmbllem0  33575  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anc  33623  areacirclem1  33630  areacirclem4  33633  areacirc  33635  geomcau  33685  isbnd2  33712  ssbnd  33717  heiborlem7  33746  heiborlem8  33747  bfplem2  33752  rrncmslem  33761  rrnequiv  33764  irrapxlem1  37703  irrapxlem2  37704  irrapxlem3  37705  irrapxlem5  37707  rpexpmord  37830  neglt  39810  2timesgt  39814  supxrge  39867  suplesup  39868  xrlexaddrp  39881  xralrple2  39883  infleinflem1  39899  xralrple4  39902  xralrple3  39903  xrralrecnnle  39915  climinf  40156  mullimc  40166  mullimcf  40173  limcrecl  40179  limcleqr  40194  addlimc  40198  0ellimcdiv  40199  limclner  40201  liminflimsupclim  40357  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem7  40542  fourierdlem73  40714  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  sge0iunmptlemre  40950  smflimlem4  41303  fldivexpfllog2  42684  blenre  42693  amgmwlem  42876
  Copyright terms: Public domain W3C validator