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

Theorem rpre 11668
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 11662 . . 3 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2 ssrab2 3646 . . 3 {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
31, 2eqsstri 3594 . 2 + ⊆ ℝ
43sseli 3560 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  {crab 2896   class class class wbr 4574  cr 9788  0cc0 9789   < clt 9927  +crp 11661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-in 3543  df-ss 3550  df-rp 11662
This theorem is referenced by:  rpxr  11669  rpcn  11670  rpssre  11672  rpge0  11674  rprege0  11676  rprene0  11678  rpaddcl  11683  rpmulcl  11684  rpdivcl  11685  rpgecl  11688  ledivge1le  11730  addlelt  11771  xralrple  11866  xlemul1  11946  infmrp1  11998  iccdil  12134  ltdifltdiv  12449  modcl  12486  mod0  12489  mulmod0  12490  modge0  12492  modlt  12493  modid0  12510  modabs  12517  modabs2  12518  modcyc  12519  modmuladd  12526  modmuladdnn0  12528  modltm1p1mod  12536  2txmodxeq0  12544  2submod  12545  moddi  12552  modsubdir  12553  modeqmodmin  12554  modirr  12555  expnlbnd  12808  rennim  13770  cnpart  13771  sqrlem1  13774  sqrlem2  13775  sqrlem4  13777  sqrlem5  13778  sqrlem6  13779  sqrlem7  13780  resqrex  13782  rpsqrtcl  13796  sqreulem  13890  eqsqrt2d  13899  2clim  14094  reccn2  14118  cn1lem  14119  climsqz  14162  climsqz2  14163  rlimsqzlem  14170  climsup  14191  climcau  14192  caucvgrlem2  14196  iseralt  14206  cvgcmp  14332  cvgcmpce  14334  divrcnv  14366  rprisefaccl  14536  efgt1  14628  ef01bndlem  14696  sinltx  14701  stdbdmet  22069  stdbdmopn  22071  met2ndci  22075  cfilucfil  22112  ngptgp  22185  reperflem  22358  iccntr  22361  reconnlem2  22367  opnreen  22371  metdseq0  22393  xlebnum  22500  cphsqrtcl3  22716  iscmet3lem3  22811  iscmet3lem1  22812  iscmet3lem2  22813  caubl  22828  lmcau  22833  bcthlem4  22846  minveclem3b  22921  minveclem3  22922  ivthlem2  22942  ivthlem3  22943  nulmbl2  23025  opnmbllem  23089  itg2const2  23228  itg2mulclem  23233  dveflem  23460  lhop  23497  dvcnvre  23500  aalioulem2  23806  aaliou  23811  aaliou3lem4  23819  ulmcaulem  23866  ulmcau  23867  ulmcn  23871  itgulm  23880  reeff1o  23919  pilem2  23924  logleb  24067  logcj  24070  argimgt0  24076  logdmnrp  24101  logcnlem3  24104  logcnlem4  24105  advlog  24114  efopnlem1  24116  cxple2  24157  cxplt2  24158  cxple3  24161  cxpcn3  24203  resqrtcn  24204  relogbf  24243  asinneg  24327  atanbndlem  24366  cxplim  24412  cxp2limlem  24416  cxp2lim  24417  cxploglim  24418  cxploglim2  24419  logdiflbnd  24435  harmoniclbnd  24449  harmonicbnd4  24451  chtrpcl  24615  ppiltx  24617  chtleppi  24649  logfacubnd  24660  logfaclbnd  24661  logfacbnd3  24662  logexprlim  24664  bposlem7  24729  bposlem8  24730  bposlem9  24731  chebbnd1  24875  chtppilim  24878  chto1ub  24879  chpo1ub  24883  vmadivsum  24885  rpvmasumlem  24890  dchrisumlem3  24894  dchrvmasumlem2  24901  dchrvmasumiflem1  24904  dchrisum0  24923  mudivsum  24933  mulogsumlem  24934  mulogsum  24935  mulog2sumlem2  24938  log2sumbnd  24947  selberglem2  24949  selberglem3  24950  selberg  24951  selberg2lem  24953  selberg2  24954  pntrf  24966  pntrmax  24967  pntrsumo1  24968  selbergr  24971  selbergs  24977  pntrlog2bndlem4  24983  pntrlog2bndlem5  24984  pntibndlem1  24992  pntlem3  25012  pntlemp  25013  pntleml  25014  pnt2  25016  padicabvcxp  25035  vacn  26731  nmcvcn  26732  smcnlem  26734  blocnilem  26846  chscllem2  27684  nmcexi  28072  nmcopexi  28073  nmcfnexi  28097  pnfinf  28871  sqsscirc1  29085  dya2icoseg2  29470  probfinmeasbOLD  29620  probfinmeasb  29621  subfacval3  30228  opnrebl  31288  opnrebl2  31289  taupilem1  32144  opnmbllem0  32415  itg2addnclem  32431  itg2addnclem2  32432  itg2addnclem3  32433  itg2addnc  32434  itg2gt0cn  32435  ftc1anclem5  32459  ftc1anclem7  32461  ftc1anc  32463  areacirclem1  32470  areacirclem4  32473  areacirc  32475  geomcau  32525  isbnd2  32552  ssbnd  32557  heiborlem7  32586  heiborlem8  32587  bfplem2  32592  rrncmslem  32601  rrnequiv  32604  irrapxlem1  36204  irrapxlem2  36205  irrapxlem3  36206  irrapxlem5  36208  rpexpmord  36331  neglt  38237  2timesgt  38241  supxrge  38296  suplesup  38297  xrlexaddrp  38310  xralrple2  38312  infleinflem1  38328  xralrple4  38331  xralrple3  38332  xrralrecnnle  38344  climinf  38474  mullimc  38484  mullimcf  38491  limcrecl  38497  limcleqr  38512  addlimc  38516  0ellimcdiv  38517  limclner  38519  ioodvbdlimc1lem1  38622  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  stoweidlem7  38701  fourierdlem73  38873  fourierdlem87  38887  fourierdlem103  38903  fourierdlem104  38904  sge0iunmptlemre  39109  smflimlem4  39461  fldivexpfllog2  42156  blenre  42165  amgmwlem  42317
  Copyright terms: Public domain W3C validator