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

Theorem rpre 11824
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 11818 . . 3 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2 ssrab2 3679 . . 3 {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
31, 2eqsstri 3627 . 2 + ⊆ ℝ
43sseli 3591 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  {crab 2913   class class class wbr 4644  cr 9920  0cc0 9921   < clt 10059  +crp 11817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-in 3574  df-ss 3581  df-rp 11818
This theorem is referenced by:  rpxr  11825  rpcn  11826  rpssre  11828  rpge0  11830  rprege0  11832  rprene0  11834  rpaddcl  11839  rpmulcl  11840  rpdivcl  11841  rpgecl  11844  ledivge1le  11886  addlelt  11927  xralrple  12021  xlemul1  12105  infmrp1  12159  iccdil  12295  ltdifltdiv  12618  modcl  12655  mod0  12658  mulmod0  12659  modge0  12661  modlt  12662  modid0  12679  modabs  12686  modabs2  12687  modcyc  12688  modmuladd  12695  modmuladdnn0  12697  modltm1p1mod  12705  2txmodxeq0  12713  2submod  12714  moddi  12721  modsubdir  12722  modeqmodmin  12723  modirr  12724  expnlbnd  12977  rennim  13960  cnpart  13961  sqrlem1  13964  sqrlem2  13965  sqrlem4  13967  sqrlem5  13968  sqrlem6  13969  sqrlem7  13970  resqrex  13972  rpsqrtcl  13986  sqreulem  14080  eqsqrt2d  14089  2clim  14284  reccn2  14308  cn1lem  14309  climsqz  14352  climsqz2  14353  rlimsqzlem  14360  climsup  14381  climcau  14382  caucvgrlem2  14386  iseralt  14396  cvgcmp  14529  cvgcmpce  14531  divrcnv  14565  rprisefaccl  14735  efgt1  14827  ef01bndlem  14895  sinltx  14900  stdbdmet  22302  stdbdmopn  22304  met2ndci  22308  cfilucfil  22345  ngptgp  22421  reperflem  22602  iccntr  22605  reconnlem2  22611  opnreen  22615  metdseq0  22638  xlebnum  22745  cphsqrtcl3  22968  iscmet3lem3  23069  iscmet3lem1  23070  iscmet3lem2  23071  caubl  23087  lmcau  23092  bcthlem4  23105  minveclem3b  23180  minveclem3  23181  ivthlem2  23202  ivthlem3  23203  nulmbl2  23285  opnmbllem  23350  itg2const2  23489  itg2mulclem  23494  dveflem  23723  lhop  23760  dvcnvre  23763  aalioulem2  24069  aaliou  24074  aaliou3lem4  24082  ulmcaulem  24129  ulmcau  24130  ulmcn  24134  itgulm  24143  reeff1o  24182  pilem2  24187  logleb  24330  logcj  24333  argimgt0  24339  logdmnrp  24368  logcnlem3  24371  logcnlem4  24372  advlog  24381  efopnlem1  24383  cxple2  24424  cxplt2  24425  cxple3  24428  cxpcn3  24470  resqrtcn  24471  relogbf  24510  asinneg  24594  atanbndlem  24633  cxplim  24679  cxp2limlem  24683  cxp2lim  24684  cxploglim  24685  cxploglim2  24686  logdiflbnd  24702  harmoniclbnd  24716  harmonicbnd4  24718  chtrpcl  24882  ppiltx  24884  chtleppi  24916  logfacubnd  24927  logfaclbnd  24928  logfacbnd3  24929  logexprlim  24931  bposlem7  24996  bposlem8  24997  bposlem9  24998  chebbnd1  25142  chtppilim  25145  chto1ub  25146  chpo1ub  25150  vmadivsum  25152  rpvmasumlem  25157  dchrisumlem3  25161  dchrvmasumlem2  25168  dchrvmasumiflem1  25171  dchrisum0  25190  mudivsum  25200  mulogsumlem  25201  mulogsum  25202  mulog2sumlem2  25205  log2sumbnd  25214  selberglem2  25216  selberglem3  25217  selberg  25218  selberg2lem  25220  selberg2  25221  pntrf  25233  pntrmax  25234  pntrsumo1  25235  selbergr  25238  selbergs  25244  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  pntibndlem1  25259  pntlem3  25279  pntlemp  25280  pntleml  25281  pnt2  25283  padicabvcxp  25302  vacn  27519  nmcvcn  27520  smcnlem  27522  blocnilem  27629  chscllem2  28467  nmcexi  28855  nmcopexi  28856  nmcfnexi  28880  dp2ltsuc  29567  dpval3rp  29582  dplti  29587  dpgti  29588  dpexpp1  29590  dpadd2  29592  pnfinf  29711  sqsscirc1  29928  dya2icoseg2  30314  probfinmeasbOLD  30464  probfinmeasb  30465  divsqrtid  30646  logdivsqrle  30702  hgt750lem2  30704  subfacval3  31145  opnrebl  32290  opnrebl2  32291  taupilem1  33138  opnmbllem0  33416  itg2addnclem  33432  itg2addnclem2  33433  itg2addnclem3  33434  itg2addnc  33435  itg2gt0cn  33436  ftc1anclem5  33460  ftc1anclem7  33462  ftc1anc  33464  areacirclem1  33471  areacirclem4  33474  areacirc  33476  geomcau  33526  isbnd2  33553  ssbnd  33558  heiborlem7  33587  heiborlem8  33588  bfplem2  33593  rrncmslem  33602  rrnequiv  33605  irrapxlem1  37205  irrapxlem2  37206  irrapxlem3  37207  irrapxlem5  37209  rpexpmord  37332  neglt  39309  2timesgt  39313  supxrge  39367  suplesup  39368  xrlexaddrp  39381  xralrple2  39383  infleinflem1  39399  xralrple4  39402  xralrple3  39403  xrralrecnnle  39415  climinf  39638  mullimc  39648  mullimcf  39655  limcrecl  39661  limcleqr  39676  addlimc  39680  0ellimcdiv  39681  limclner  39683  liminflimsupclim  39833  ioodvbdlimc1lem1  39909  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  stoweidlem7  39987  fourierdlem73  40159  fourierdlem87  40173  fourierdlem103  40189  fourierdlem104  40190  sge0iunmptlemre  40395  smflimlem4  40745  fldivexpfllog2  42124  blenre  42133  amgmwlem  42313
  Copyright terms: Public domain W3C validator