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

Theorem rpred 10406
Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpred  |-  ( ph  ->  A  e.  RR )

Proof of Theorem rpred
StepHypRef Expression
1 rpssre 10380 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3191 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   RRcr 8752   RR+crp 10370
This theorem is referenced by:  rpxrd  10407  rpcnd  10408  rpregt0d  10412  rprege0d  10413  rprene0d  10414  rprecred  10417  ltmulgt11d  10437  ltmulgt12d  10438  gt0divd  10439  ge0divd  10440  lediv12ad  10461  xlemul1  10626  xov1plusxeqvd  10796  ltexp2a  11169  expcan  11170  ltexp2  11171  leexp2a  11173  expnlbnd2  11248  expmulnbnd  11249  sqrlem6  11749  cau3lem  11854  rlimcld2  12068  addcn2  12083  mulcn2  12085  reccn2  12086  o1rlimmul  12108  rlimno1  12143  caucvgrlem  12161  isumrpcl  12318  isumltss  12323  expcnv  12338  mertenslem1  12356  effsumlt  12407  recoshcl  12454  eirrlem  12498  rpnnen2lem11  12519  bitsmod  12643  prmreclem3  12981  prmreclem5  12983  4sqlem7  13007  ssblex  17990  metss2lem  18073  methaus  18082  met1stc  18083  met2ndci  18084  nlmvscnlem2  18212  nlmvscnlem1  18213  nrginvrcnlem  18217  nmoi2  18255  nghmcn  18270  reperflem  18339  iccntr  18342  icccmplem2  18344  reconnlem2  18348  opnreen  18352  metdcnlem  18357  metnrmlem3  18381  addcnlem  18384  cnheibor  18469  cnllycmp  18470  lebnumlem3  18477  lebnumii  18480  nmoleub2lem  18611  nmoleub2lem3  18612  nmoleub2lem2  18613  nmoleub3  18616  nmhmcn  18617  ipcnlem2  18687  ipcnlem1  18688  lmnn  18705  iscfil3  18715  cfilfcls  18716  iscmet3lem1  18733  iscmet3lem2  18734  bcthlem4  18765  bcthlem5  18766  minveclem3b  18808  minveclem3  18809  ivthlem2  18828  ovolgelb  18855  ovollb2lem  18863  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovolscalem1  18888  ioombl1lem2  18932  ioombl1lem4  18934  uniioombllem1  18952  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  opnmbllem  18972  volcn  18977  vitalilem4  18982  itg2mulclem  19117  itg2monolem3  19123  itg2cnlem2  19133  itg2cn  19134  itggt0  19212  dveflem  19342  dvferm1lem  19347  dvferm2lem  19349  lhop1lem  19376  lhop1  19377  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  dvfsumrlim  19394  ftc1a  19400  ftc1lem4  19402  plyeq0lem  19608  aalioulem2  19729  aalioulem4  19731  aalioulem5  19732  aalioulem6  19733  aaliou  19734  aaliou2b  19737  aaliou3lem1  19738  aaliou3lem2  19739  aaliou3lem8  19741  aaliou3lem5  19743  aaliou3lem7  19745  aaliou3lem9  19746  ulmcn  19792  ulmdvlem1  19793  mtest  19797  itgulm  19800  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  pserdv  19821  abelthlem7  19830  pilem2  19844  divlogrlim  19998  logcnlem3  20007  logcnlem4  20008  logccv  20026  divcxp  20050  cxplt  20057  cxple2  20060  cxpcn3lem  20103  cxpaddlelem  20107  cxpaddle  20108  loglesqr  20114  leibpi  20254  rlimcnp3  20278  cxplim  20282  rlimcxp  20284  cxp2limlem  20286  cxp2lim  20287  cxploglim  20288  cxploglim2  20289  divsqrsumlem  20290  jensenlem2  20298  logdifbnd  20304  emcllem4  20308  harmonicbnd4  20320  fsumharmonic  20321  ftalem1  20326  ftalem2  20327  ftalem3  20328  ftalem5  20330  basellem1  20334  basellem3  20336  basellem4  20337  basellem8  20341  chtwordi  20410  chpchtsum  20474  logfacrlim  20479  logexprlim  20480  bclbnd  20535  efexple  20536  bposlem1  20539  bposlem2  20540  bposlem6  20544  bposlem7  20545  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem1  20638  chtppilimlem2  20639  chpo1ubb  20646  rplogsumlem1  20649  rplogsumlem2  20650  dchrisum0lem1a  20651  rpvmasumlem  20652  dchrisumlem2  20655  dchrisumlem3  20656  dchrmusumlema  20658  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasumlema  20665  dchrvmasumiflem1  20666  dchrisum0fno1  20676  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2  20683  dchrisum0lem3  20684  dchrisum0  20685  mulogsumlem  20696  logdivsum  20698  mulog2sumlem2  20700  vmalogdivsum2  20703  vmalogdivsum  20704  2vmadivsumlem  20705  log2sumbnd  20709  selberglem2  20711  selberg  20713  selberg2lem  20715  chpdifbndlem1  20718  chpdifbndlem2  20719  selberg3lem1  20722  selberg3  20724  selberg4lem1  20725  selberg4  20726  pntrsumbnd2  20732  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntrlog2bndlem6a  20747  pntrlog2bndlem6  20748  pntrlog2bnd  20749  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntibndlem1  20754  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemc  20760  pntlema  20761  pntlemb  20762  pntlemg  20763  pntlemh  20764  pntlemn  20765  pntlemq  20766  pntlemr  20767  pntlemj  20768  pntlemi  20769  pntlemf  20770  pntlemk  20771  pntlemo  20772  pntleme  20773  pntlem3  20774  pntlemp  20775  pntleml  20776  ostth2lem1  20783  ostth2lem3  20800  ostth2  20802  ostth3  20803  smcnlem  21286  blocnilem  21398  blocni  21399  ubthlem2  21466  minvecolem3  21471  minvecolem4  21475  minvecolem5  21476  nmcexi  22622  lnconi  22629  rpxdivcld  23134  sqsscirc1  23307  cnre2csqlem  23309  cnre2csqima  23310  tpr2rico  23311  xrmulc1cn  23318  xrge0iifiso  23332  xrge0iifhom  23334  esumcst  23451  esumdivc  23466  dya2iocress  23592  dya2iocseg  23594  zetacvg  23704  itg2addnclem  25003  itg2addnc  25005  itggt0cn  25023  ftc1cnnclem  25024  geomcau  26578  sstotbnd2  26601  isbnd3  26611  prdsbnd2  26622  cntotbnd  26623  heibor1lem  26636  heiborlem6  26643  bfplem1  26649  bfplem2  26650  bfp  26651  rrndstprj2  26658  rrnequiv  26662  irrapxlem4  27013  irrapxlem5  27014  irrapx1  27016  pell1qrgaplem  27061  pell14qrgapw  27064  pellqrexplicit  27065  pellqrex  27067  pellfundge  27070  pellfundgt1  27071  rmspecfund  27097  rmxycomplete  27105  rpexpmord  27136  rmxypos  27137  stoweidlem62  27914  wallispilem5  27921  stirlinglem1  27926  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem12  27937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-in 3172  df-ss 3179  df-rp 10371
  Copyright terms: Public domain W3C validator