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

Theorem rpre 12924
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.)
Assertion
Ref Expression
rpre (𝐴 ∈ ℝ+𝐴 ∈ ℝ)

Proof of Theorem rpre
StepHypRef Expression
1 rpssre 12923 . 2 + ⊆ ℝ
21sseli 3941 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  +crp 12916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918  df-ss 3928  df-rp 12917
This theorem is referenced by:  rpxr  12925  rpcn  12926  rpge0  12929  rprege0  12931  rprene0  12933  rpaddcl  12938  rpmulcl  12939  rpdivcl  12941  rpgecl  12944  ledivge1le  12987  addlelt  13030  xralrple  13125  xlemul1  13210  infmrp1  13264  iccdil  13408  ltdifltdiv  13740  modcl  13779  mod0  13782  mulmod0  13783  modge0  13785  modlt  13786  modid0  13803  modabs  13810  modabs2  13811  modcyc  13812  modmuladd  13819  modmuladdnn0  13821  modltm1p1mod  13829  2txmodxeq0  13837  2submod  13838  moddi  13845  modsubdir  13846  modeqmodmin  13847  modirr  13848  rpexpmord  14074  expnlbnd  14137  rennim  15125  cnpart  15126  01sqrexlem1  15128  01sqrexlem2  15129  01sqrexlem4  15131  01sqrexlem5  15132  01sqrexlem6  15133  01sqrexlem7  15134  resqrex  15136  rpsqrtcl  15150  sqreulem  15245  eqsqrt2d  15254  2clim  15455  reccn2  15480  cn1lem  15481  climsqz  15524  climsqz2  15525  rlimsqzlem  15534  climsup  15555  climcau  15556  caucvgrlem2  15560  iseralt  15570  cvgcmp  15702  cvgcmpce  15704  divrcnv  15738  rprisefaccl  15907  efgt1  15999  ef01bndlem  16067  sinltx  16072  stdbdmet  23875  stdbdmopn  23877  met2ndci  23881  cfilucfil  23918  ngptgp  23995  reperflem  24184  iccntr  24187  reconnlem2  24193  opnreen  24197  metdseq0  24220  xlebnum  24331  cphsqrtcl3  24554  iscmet3lem3  24657  iscmet3lem1  24658  iscmet3lem2  24659  caubl  24675  lmcau  24680  bcthlem4  24694  minveclem3b  24795  minveclem3  24796  ivthlem2  24819  ivthlem3  24820  nulmbl2  24903  opnmbllem  24968  itg2const2  25109  itg2mulclem  25114  dveflem  25346  lhop  25383  dvcnvre  25386  aalioulem2  25696  aaliou  25701  aaliou3lem4  25709  ulmcaulem  25756  ulmcau  25757  ulmcn  25761  itgulm  25770  reeff1o  25809  pilem2  25814  logleb  25961  logcj  25964  argimgt0  25970  logdmnrp  25999  logcnlem3  26002  logcnlem4  26003  advlog  26012  efopnlem1  26014  cxple2  26055  cxplt2  26056  cxple3  26059  2irrexpq  26088  cxpcn3  26104  resqrtcn  26105  relogbf  26144  asinneg  26239  atanbndlem  26278  cxplim  26324  cxp2limlem  26328  cxp2lim  26329  cxploglim  26330  cxploglim2  26331  logdiflbnd  26347  harmoniclbnd  26361  harmonicbnd4  26363  chtrpcl  26527  ppiltx  26529  chtleppi  26561  logfacubnd  26572  logfaclbnd  26573  logfacbnd3  26574  logexprlim  26576  bposlem7  26641  bposlem8  26642  bposlem9  26643  chebbnd1  26823  chtppilim  26826  chto1ub  26827  chpo1ub  26831  vmadivsum  26833  rpvmasumlem  26838  dchrisumlem3  26842  dchrvmasumlem2  26849  dchrvmasumiflem1  26852  dchrisum0  26871  mudivsum  26881  mulogsumlem  26882  mulogsum  26883  mulog2sumlem2  26886  log2sumbnd  26895  selberglem2  26897  selberglem3  26898  selberg  26899  selberg2lem  26901  selberg2  26902  pntrf  26914  pntrmax  26915  pntrsumo1  26916  selbergr  26919  selbergs  26925  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntibndlem1  26940  pntlem3  26960  pntlemp  26961  pntleml  26962  pnt2  26964  padicabvcxp  26983  vacn  29639  nmcvcn  29640  smcnlem  29642  blocnilem  29749  chscllem2  30583  nmcexi  30971  nmcopexi  30972  nmcfnexi  30996  dp2ltsuc  31745  dpval3rp  31759  dplti  31764  dpgti  31765  dpexpp1  31767  dpadd2  31769  pnfinf  32022  sqsscirc1  32492  dya2icoseg2  32881  probfinmeasb  33031  probfinmeasbALTV  33032  signshf  33203  divsqrtid  33210  logdivsqrle  33266  hgt750lem2  33268  subfacval3  33786  opnrebl  34795  opnrebl2  34796  taupilem1  35795  opnmbllem0  36117  itg2addnclem  36132  itg2addnclem2  36133  itg2addnclem3  36134  itg2addnc  36135  itg2gt0cn  36136  ftc1anclem5  36158  ftc1anclem7  36160  ftc1anc  36162  areacirclem1  36169  areacirclem4  36172  areacirc  36174  geomcau  36221  isbnd2  36245  ssbnd  36250  heiborlem7  36279  heiborlem8  36280  bfplem2  36285  rrncmslem  36294  rrnequiv  36297  dvrelog3  40525  aks4d1p1p6  40533  irrapxlem1  41148  irrapxlem2  41149  irrapxlem3  41150  irrapxlem5  41152  neglt  43525  2timesgt  43529  supxrge  43579  suplesup  43580  xrlexaddrp  43593  xralrple2  43595  infleinflem1  43611  xralrple4  43614  xralrple3  43615  xrralrecnnle  43624  climinf  43854  mullimc  43864  mullimcf  43871  limcrecl  43877  limcleqr  43892  addlimc  43896  0ellimcdiv  43897  limclner  43899  liminflimsupclim  44055  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  stoweidlem7  44255  fourierdlem73  44427  fourierdlem87  44441  fourierdlem103  44457  fourierdlem104  44458  sge0iunmptlemre  44663  smflimlem4  45022  fldivexpfllog2  46658  blenre  46667  itscnhlc0yqe  46852  itscnhlc0xyqsol  46858  itschlc0xyqsol  46860  itsclc0xyqsolr  46862  itsclinecirc0in  46868  itsclquadb  46869  itscnhlinecirc02plem3  46877  itscnhlinecirc02p  46878  inlinecirc02plem  46879  inlinecirc02p  46880  amgmwlem  47256
  Copyright terms: Public domain W3C validator