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

Theorem rpred 10482
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 10456 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3254 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   RRcr 8826   RR+crp 10446
This theorem is referenced by:  rpxrd  10483  rpcnd  10484  rpregt0d  10488  rprege0d  10489  rprene0d  10490  rprecred  10493  ltmulgt11d  10513  ltmulgt12d  10514  gt0divd  10515  ge0divd  10516  lediv12ad  10537  xlemul1  10702  xov1plusxeqvd  10872  ltexp2a  11246  expcan  11247  ltexp2  11248  leexp2a  11250  expnlbnd2  11325  expmulnbnd  11326  sqrlem6  11829  cau3lem  11934  rlimcld2  12148  addcn2  12163  mulcn2  12165  reccn2  12166  o1rlimmul  12188  rlimno1  12223  caucvgrlem  12242  isumrpcl  12399  isumltss  12404  expcnv  12419  mertenslem1  12437  effsumlt  12488  recoshcl  12535  eirrlem  12579  rpnnen2lem11  12600  bitsmod  12724  prmreclem3  13062  prmreclem5  13064  4sqlem7  13088  ssblex  18076  metss2lem  18159  methaus  18168  met1stc  18169  met2ndci  18170  nlmvscnlem2  18298  nlmvscnlem1  18299  nrginvrcnlem  18303  nmoi2  18341  nghmcn  18356  reperflem  18426  iccntr  18429  icccmplem2  18431  reconnlem2  18435  opnreen  18439  metdcnlem  18444  metnrmlem3  18468  addcnlem  18471  cnheibor  18557  cnllycmp  18558  lebnumlem3  18565  lebnumii  18568  nmoleub2lem  18699  nmoleub2lem3  18700  nmoleub2lem2  18701  nmoleub3  18704  nmhmcn  18705  ipcnlem2  18775  ipcnlem1  18776  lmnn  18793  iscfil3  18803  cfilfcls  18804  iscmet3lem1  18821  iscmet3lem2  18822  bcthlem4  18853  bcthlem5  18854  minveclem3b  18896  minveclem3  18897  ivthlem2  18916  ovolgelb  18943  ovollb2lem  18951  ovolunlem1a  18959  ovolunlem1  18960  ovoliunlem1  18965  ovoliunlem2  18966  ovolscalem1  18976  ioombl1lem2  19020  ioombl1lem4  19022  uniioombllem1  19040  uniioombllem3  19044  uniioombllem4  19045  uniioombllem5  19046  opnmbllem  19060  volcn  19065  vitalilem4  19070  itg2mulclem  19205  itg2monolem3  19211  itg2cnlem2  19221  itg2cn  19222  itggt0  19300  dveflem  19430  dvferm1lem  19435  dvferm2lem  19437  lhop1lem  19464  lhop1  19465  lhop  19467  dvcnvrelem1  19468  dvcnvrelem2  19469  dvcnvre  19470  dvfsumrlim  19482  ftc1a  19488  ftc1lem4  19490  plyeq0lem  19696  aalioulem2  19817  aalioulem4  19819  aalioulem5  19820  aalioulem6  19821  aaliou  19822  aaliou2b  19825  aaliou3lem1  19826  aaliou3lem2  19827  aaliou3lem8  19829  aaliou3lem5  19831  aaliou3lem7  19833  aaliou3lem9  19834  ulmcn  19882  ulmdvlem1  19883  mtest  19887  itgulm  19891  psercn  19909  pserdvlem1  19910  pserdvlem2  19911  pserdv  19912  abelthlem7  19921  pilem2  19935  divlogrlim  20093  logcnlem3  20102  logcnlem4  20103  logccv  20121  divcxp  20145  cxplt  20152  cxple2  20155  cxpcn3lem  20198  cxpaddlelem  20202  cxpaddle  20203  loglesqr  20209  leibpi  20349  rlimcnp3  20373  cxplim  20377  rlimcxp  20379  cxp2limlem  20381  cxp2lim  20382  cxploglim  20383  cxploglim2  20384  divsqrsumlem  20385  jensenlem2  20393  logdifbnd  20399  emcllem4  20404  harmonicbnd4  20416  fsumharmonic  20417  ftalem1  20422  ftalem2  20423  ftalem3  20424  ftalem5  20426  basellem1  20430  basellem3  20432  basellem4  20433  basellem8  20437  chtwordi  20506  chpchtsum  20570  logfacrlim  20575  logexprlim  20576  bclbnd  20631  efexple  20632  bposlem1  20635  bposlem2  20636  bposlem6  20640  bposlem7  20641  chebbnd1lem3  20732  chebbnd1  20733  chtppilimlem1  20734  chtppilimlem2  20735  chpo1ubb  20742  rplogsumlem1  20745  rplogsumlem2  20746  dchrisum0lem1a  20747  rpvmasumlem  20748  dchrisumlem2  20751  dchrisumlem3  20752  dchrmusumlema  20754  dchrmusum2  20755  dchrvmasumlem1  20756  dchrvmasum2lem  20757  dchrvmasumlema  20761  dchrvmasumiflem1  20762  dchrisum0fno1  20772  dchrisum0lem1b  20776  dchrisum0lem1  20777  dchrisum0lem2  20779  dchrisum0lem3  20780  dchrisum0  20781  mulogsumlem  20792  logdivsum  20794  mulog2sumlem2  20796  vmalogdivsum2  20799  vmalogdivsum  20800  2vmadivsumlem  20801  log2sumbnd  20805  selberglem2  20807  selberg  20809  selberg2lem  20811  chpdifbndlem1  20814  chpdifbndlem2  20815  selberg3lem1  20818  selberg3  20820  selberg4lem1  20821  selberg4  20822  pntrsumbnd2  20828  selberg3r  20830  selberg4r  20831  selberg34r  20832  pntrlog2bndlem1  20838  pntrlog2bndlem2  20839  pntrlog2bndlem3  20840  pntrlog2bndlem5  20842  pntrlog2bndlem6a  20843  pntrlog2bndlem6  20844  pntrlog2bnd  20845  pntpbnd1a  20846  pntpbnd1  20847  pntpbnd2  20848  pntibndlem1  20850  pntibndlem2  20852  pntibndlem3  20853  pntibnd  20854  pntlemc  20856  pntlema  20857  pntlemb  20858  pntlemg  20859  pntlemh  20860  pntlemn  20861  pntlemq  20862  pntlemr  20863  pntlemj  20864  pntlemi  20865  pntlemf  20866  pntlemk  20867  pntlemo  20868  pntleme  20869  pntlem3  20870  pntlemp  20871  pntleml  20872  ostth2lem1  20879  ostth2lem3  20896  ostth2  20898  ostth3  20899  smcnlem  21384  blocnilem  21496  blocni  21497  ubthlem2  21564  minvecolem3  21569  minvecolem4  21573  minvecolem5  21574  nmcexi  22720  lnconi  22727  rpxdivcld  23385  sqsscirc1  23462  cnre2csqlem  23464  tpr2rico  23466  xrmulc1cn  23472  xrge0iifiso  23477  xrge0iifhom  23479  metustto  23597  metustexhalf  23600  esumcst  23721  esumdivc  23739  dya2iocress  23888  dya2icoseg  23891  zetacvg  24048  lgamgulmlem2  24063  lgamgulmlem3  24064  lgamgulmlem5  24066  lgamucov  24071  regamcl  24094  relgamcl  24095  gammacvglem1  24651  gammacvglem3  24653  itg2addnclem  25492  itg2addnc  25494  itggt0cn  25512  ftc1cnnclem  25513  geomcau  25799  sstotbnd2  25821  isbnd3  25831  prdsbnd2  25842  cntotbnd  25843  heibor1lem  25856  heiborlem6  25863  bfplem1  25869  bfplem2  25870  bfp  25871  rrndstprj2  25878  rrnequiv  25882  irrapxlem4  26233  irrapxlem5  26234  irrapx1  26236  pell1qrgaplem  26281  pell14qrgapw  26284  pellqrexplicit  26285  pellqrex  26287  pellfundge  26290  pellfundgt1  26291  rmspecfund  26317  rmxycomplete  26325  rpexpmord  26356  rmxypos  26357  stoweidlem62  27134  wallispilem5  27141  stirlinglem1  27146  stirlinglem4  27149  stirlinglem5  27150  stirlinglem6  27151  stirlinglem12  27157
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-in 3235  df-ss 3242  df-rp 10447
  Copyright terms: Public domain W3C validator