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

Theorem rpre 12389
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 12388 . 2 + ⊆ ℝ
21sseli 3914 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cr 10529  +crp 12381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-in 3891  df-ss 3901  df-rp 12382
This theorem is referenced by:  rpxr  12390  rpcn  12391  rpge0  12394  rprege0  12396  rprene0  12398  rpaddcl  12403  rpmulcl  12404  rpdivcl  12406  rpgecl  12409  ledivge1le  12452  addlelt  12495  xralrple  12590  xlemul1  12675  infmrp1  12729  iccdil  12872  ltdifltdiv  13203  modcl  13240  mod0  13243  mulmod0  13244  modge0  13246  modlt  13247  modid0  13264  modabs  13271  modabs2  13272  modcyc  13273  modmuladd  13280  modmuladdnn0  13282  modltm1p1mod  13290  2txmodxeq0  13298  2submod  13299  moddi  13306  modsubdir  13307  modeqmodmin  13308  modirr  13309  rpexpmord  13532  expnlbnd  13594  rennim  14593  cnpart  14594  sqrlem1  14597  sqrlem2  14598  sqrlem4  14600  sqrlem5  14601  sqrlem6  14602  sqrlem7  14603  resqrex  14605  rpsqrtcl  14619  sqreulem  14714  eqsqrt2d  14723  2clim  14924  reccn2  14948  cn1lem  14949  climsqz  14992  climsqz2  14993  rlimsqzlem  15000  climsup  15021  climcau  15022  caucvgrlem2  15026  iseralt  15036  cvgcmp  15166  cvgcmpce  15168  divrcnv  15202  rprisefaccl  15372  efgt1  15464  ef01bndlem  15532  sinltx  15537  stdbdmet  23126  stdbdmopn  23128  met2ndci  23132  cfilucfil  23169  ngptgp  23245  reperflem  23426  iccntr  23429  reconnlem2  23435  opnreen  23439  metdseq0  23462  xlebnum  23573  cphsqrtcl3  23795  iscmet3lem3  23897  iscmet3lem1  23898  iscmet3lem2  23899  caubl  23915  lmcau  23920  bcthlem4  23934  minveclem3b  24035  minveclem3  24036  ivthlem2  24059  ivthlem3  24060  nulmbl2  24143  opnmbllem  24208  itg2const2  24348  itg2mulclem  24353  dveflem  24585  lhop  24622  dvcnvre  24625  aalioulem2  24932  aaliou  24937  aaliou3lem4  24945  ulmcaulem  24992  ulmcau  24993  ulmcn  24997  itgulm  25006  reeff1o  25045  pilem2  25050  logleb  25197  logcj  25200  argimgt0  25206  logdmnrp  25235  logcnlem3  25238  logcnlem4  25239  advlog  25248  efopnlem1  25250  cxple2  25291  cxplt2  25292  cxple3  25295  2irrexpq  25324  cxpcn3  25340  resqrtcn  25341  relogbf  25380  asinneg  25475  atanbndlem  25514  cxplim  25560  cxp2limlem  25564  cxp2lim  25565  cxploglim  25566  cxploglim2  25567  logdiflbnd  25583  harmoniclbnd  25597  harmonicbnd4  25599  chtrpcl  25763  ppiltx  25765  chtleppi  25797  logfacubnd  25808  logfaclbnd  25809  logfacbnd3  25810  logexprlim  25812  bposlem7  25877  bposlem8  25878  bposlem9  25879  chebbnd1  26059  chtppilim  26062  chto1ub  26063  chpo1ub  26067  vmadivsum  26069  rpvmasumlem  26074  dchrisumlem3  26078  dchrvmasumlem2  26085  dchrvmasumiflem1  26088  dchrisum0  26107  mudivsum  26117  mulogsumlem  26118  mulogsum  26119  mulog2sumlem2  26122  log2sumbnd  26131  selberglem2  26133  selberglem3  26134  selberg  26135  selberg2lem  26137  selberg2  26138  pntrf  26150  pntrmax  26151  pntrsumo1  26152  selbergr  26155  selbergs  26161  pntrlog2bndlem4  26167  pntrlog2bndlem5  26168  pntibndlem1  26176  pntlem3  26196  pntlemp  26197  pntleml  26198  pnt2  26200  padicabvcxp  26219  vacn  28480  nmcvcn  28481  smcnlem  28483  blocnilem  28590  chscllem2  29424  nmcexi  29812  nmcopexi  29813  nmcfnexi  29837  dp2ltsuc  30591  dpval3rp  30605  dplti  30610  dpgti  30611  dpexpp1  30613  dpadd2  30615  pnfinf  30865  sqsscirc1  31259  dya2icoseg2  31644  probfinmeasb  31794  probfinmeasbALTV  31795  signshf  31966  divsqrtid  31973  logdivsqrle  32029  hgt750lem2  32031  subfacval3  32544  opnrebl  33776  opnrebl2  33777  taupilem1  34730  opnmbllem0  35086  itg2addnclem  35101  itg2addnclem2  35102  itg2addnclem3  35103  itg2addnc  35104  itg2gt0cn  35105  ftc1anclem5  35127  ftc1anclem7  35129  ftc1anc  35131  areacirclem1  35138  areacirclem4  35141  areacirc  35143  geomcau  35190  isbnd2  35214  ssbnd  35219  heiborlem7  35248  heiborlem8  35249  bfplem2  35254  rrncmslem  35263  rrnequiv  35266  irrapxlem1  39750  irrapxlem2  39751  irrapxlem3  39752  irrapxlem5  39754  neglt  41902  2timesgt  41906  supxrge  41957  suplesup  41958  xrlexaddrp  41971  xralrple2  41973  infleinflem1  41989  xralrple4  41992  xralrple3  41993  xrralrecnnle  42004  climinf  42235  mullimc  42245  mullimcf  42252  limcrecl  42258  limcleqr  42273  addlimc  42277  0ellimcdiv  42278  limclner  42280  liminflimsupclim  42436  ioodvbdlimc1lem1  42560  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  stoweidlem7  42636  fourierdlem73  42808  fourierdlem87  42822  fourierdlem103  42838  fourierdlem104  42839  sge0iunmptlemre  43041  smflimlem4  43394  fldivexpfllog2  44966  blenre  44975  itscnhlc0yqe  45160  itscnhlc0xyqsol  45166  itschlc0xyqsol  45168  itsclc0xyqsolr  45170  itsclinecirc0in  45176  itsclquadb  45177  itscnhlinecirc02plem3  45185  itscnhlinecirc02p  45186  inlinecirc02plem  45187  inlinecirc02p  45188  amgmwlem  45317
  Copyright terms: Public domain W3C validator