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

Theorem rpre 11255
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 11250 . . 3
2 ssrab2 3584 . . 3
31, 2eqsstri 3533 . 2
43sseli 3499 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  {crab 2811   class class class wbr 4452   cr 9512  0cc0 9513   clt 9649   crp 11249
This theorem is referenced by:  rpxr  11256  rpcn  11257  rpssre  11259  rpge0  11261  rprege0  11263  rprene0  11265  rpaddcl  11269  rpmulcl  11270  rpdivcl  11271  rpgecl  11274  xralrple  11433  xlemul1  11511  iccdil  11687  ltdifltdiv  11966  modcl  12000  mod0  12003  modge0  12005  modlt  12006  modid0  12021  modabs  12029  modabs2  12030  modcyc  12031  modltm1p1mod  12039  2txmodxeq0  12047  2submod  12048  moddi  12054  modsubdir  12055  modeqmodmin  12056  modirr  12057  expnlbnd  12296  rennim  13072  cnpart  13073  sqrlem1  13076  sqrlem2  13077  sqrlem4  13079  sqrlem5  13080  sqrlem6  13081  sqrlem7  13082  resqrex  13084  rpsqrtcl  13098  sqreulem  13192  eqsqrt2d  13201  2clim  13395  reccn2  13419  cn1lem  13420  climsqz  13463  climsqz2  13464  rlimsqzlem  13471  climsup  13492  climcau  13493  caucvgrlem2  13497  iseralt  13507  cvgcmp  13630  cvgcmpce  13632  divrcnv  13664  efgt1  13851  ef01bndlem  13919  sinltx  13924  stdbdmet  21019  stdbdmopn  21021  met2ndci  21025  cfilucfilOLD  21072  cfilucfil  21073  ngptgp  21150  reperflem  21323  iccntr  21326  reconnlem2  21332  opnreen  21336  metdseq0  21358  xlebnum  21465  cphsqrtcl3  21634  iscmet3lem3  21729  iscmet3lem1  21730  iscmet3lem2  21731  caubl  21746  lmcau  21751  bcthlem4  21766  minveclem3b  21843  minveclem3  21844  ivthlem2  21864  ivthlem3  21865  nulmbl2  21947  opnmbllem  22010  itg2const2  22148  itg2mulclem  22153  dveflem  22380  lhop  22417  dvcnvre  22420  aalioulem2  22729  aaliou  22734  aaliou3lem4  22742  ulmcaulem  22789  ulmcau  22790  ulmcn  22794  itgulm  22803  reeff1o  22842  pilem2  22847  logleb  22988  logcj  22991  argimgt0  22997  logdmnrp  23022  logcnlem3  23025  logcnlem4  23026  advlog  23035  efopnlem1  23037  cxple2  23078  cxplt2  23079  cxple3  23082  cxpcn3  23122  resqrtcn  23123  asinneg  23217  atanbndlem  23256  cxplim  23301  cxp2limlem  23305  cxp2lim  23306  cxploglim  23307  cxploglim2  23308  logdiflbnd  23324  harmoniclbnd  23338  harmonicbnd4  23340  chtrpcl  23449  ppiltx  23451  chtleppi  23485  logfacubnd  23496  logfaclbnd  23497  logfacbnd3  23498  logexprlim  23500  bposlem7  23565  bposlem8  23566  bposlem9  23567  chebbnd1  23657  chtppilim  23660  chto1ub  23661  chpo1ub  23665  vmadivsum  23667  rpvmasumlem  23672  dchrisumlem3  23676  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  dchrisum0  23705  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  mulog2sumlem2  23720  log2sumbnd  23729  selberglem2  23731  selberglem3  23732  selberg  23733  selberg2lem  23735  selberg2  23736  pntrf  23748  pntrmax  23749  pntrsumo1  23750  selbergr  23753  selbergs  23759  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntibndlem1  23774  pntlem3  23794  pntlemp  23795  pntleml  23796  pnt2  23798  padicabvcxp  23817  vacn  25604  nmcvcn  25605  smcnlem  25607  blocnilem  25719  chscllem2  26556  nmcexi  26945  nmcopexi  26946  nmcfnexi  26970  pnfinf  27727  sqsscirc1  27890  dya2icoseg2  28249  probfinmeasbOLD  28367  probfinmeasb  28368  subfacval3  28633  rprisefaccl  29145  opnmbllem0  30050  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anc  30098  areacirclem1  30107  areacirclem4  30110  areacirc  30112  opnrebl  30138  opnrebl2  30139  geomcau  30252  isbnd2  30279  ssbnd  30284  heiborlem7  30313  heiborlem8  30314  bfplem2  30319  rrncmslem  30328  rrnequiv  30331  irrapxlem1  30758  irrapxlem2  30759  irrapxlem3  30760  irrapxlem5  30762  rpexpmord  30884  neglt  31467  2timesgt  31475  climinf  31612  mullimc  31622  mullimcf  31629  limcrecl  31635  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  limclner  31657  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem7  31789  fourierdlem73  31962  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  taupilem1  37696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3482  df-ss 3489  df-rp 11250
  Copyright terms: Public domain W3C validator