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

Theorem rpred 10581
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 10555 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3290 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   RRcr 8923   RR+crp 10545
This theorem is referenced by:  rpxrd  10582  rpcnd  10583  rpregt0d  10587  rprege0d  10588  rprene0d  10589  rprecred  10592  ltmulgt11d  10612  ltmulgt12d  10613  gt0divd  10614  ge0divd  10615  lediv12ad  10636  xlemul1  10802  xov1plusxeqvd  10974  ltexp2a  11359  expcan  11360  ltexp2  11361  leexp2a  11363  expnlbnd2  11438  expmulnbnd  11439  sqrlem6  11981  cau3lem  12086  rlimcld2  12300  addcn2  12315  mulcn2  12317  reccn2  12318  o1rlimmul  12340  rlimno1  12375  caucvgrlem  12394  isumrpcl  12551  isumltss  12556  expcnv  12571  mertenslem1  12589  effsumlt  12640  recoshcl  12687  eirrlem  12731  rpnnen2lem11  12752  bitsmod  12876  prmreclem3  13214  prmreclem5  13216  4sqlem7  13240  ssblex  18349  metss2lem  18432  methaus  18441  met1stc  18442  met2ndci  18443  metustto  18474  metustexhalf  18477  nlmvscnlem2  18593  nlmvscnlem1  18594  nrginvrcnlem  18598  nmoi2  18636  nghmcn  18651  reperflem  18721  iccntr  18724  icccmplem2  18726  reconnlem2  18730  opnreen  18734  metdcnlem  18739  metnrmlem3  18763  addcnlem  18766  cnheibor  18852  cnllycmp  18853  lebnumlem3  18860  lebnumii  18863  nmoleub2lem  18994  nmoleub2lem3  18995  nmoleub2lem2  18996  nmoleub3  18999  nmhmcn  19000  ipcnlem2  19070  ipcnlem1  19071  lmnn  19088  iscfil3  19098  cfilfcls  19099  iscmet3lem1  19116  iscmet3lem2  19117  bcthlem4  19150  bcthlem5  19151  minveclem3b  19197  minveclem3  19198  ivthlem2  19217  ovolgelb  19244  ovollb2lem  19252  ovolunlem1a  19260  ovolunlem1  19261  ovoliunlem1  19266  ovoliunlem2  19267  ovolscalem1  19277  ioombl1lem2  19321  ioombl1lem4  19323  uniioombllem1  19341  uniioombllem3  19345  uniioombllem4  19346  uniioombllem5  19347  opnmbllem  19361  volcn  19366  vitalilem4  19371  itg2mulclem  19506  itg2monolem3  19512  itg2cnlem2  19522  itg2cn  19523  itggt0  19601  dveflem  19731  dvferm1lem  19736  dvferm2lem  19738  lhop1lem  19765  lhop1  19766  lhop  19768  dvcnvrelem1  19769  dvcnvrelem2  19770  dvcnvre  19771  dvfsumrlim  19783  ftc1a  19789  ftc1lem4  19791  plyeq0lem  19997  aalioulem2  20118  aalioulem4  20120  aalioulem5  20121  aalioulem6  20122  aaliou  20123  aaliou2b  20126  aaliou3lem1  20127  aaliou3lem2  20128  aaliou3lem8  20130  aaliou3lem5  20132  aaliou3lem7  20134  aaliou3lem9  20135  ulmcn  20183  ulmdvlem1  20184  mtest  20188  itgulm  20192  psercn  20210  pserdvlem1  20211  pserdvlem2  20212  pserdv  20213  abelthlem7  20222  pilem2  20236  divlogrlim  20394  logcnlem3  20403  logcnlem4  20404  logccv  20422  divcxp  20446  cxplt  20453  cxple2  20456  cxpcn3lem  20499  cxpaddlelem  20503  cxpaddle  20504  loglesqr  20510  leibpi  20650  rlimcnp3  20674  cxplim  20678  rlimcxp  20680  cxp2limlem  20682  cxp2lim  20683  cxploglim  20684  cxploglim2  20685  divsqrsumlem  20686  jensenlem2  20694  logdifbnd  20700  emcllem4  20705  harmonicbnd4  20717  fsumharmonic  20718  ftalem1  20723  ftalem2  20724  ftalem3  20725  ftalem5  20727  basellem1  20731  basellem3  20733  basellem4  20734  basellem8  20738  chtwordi  20807  chpchtsum  20871  logfacrlim  20876  logexprlim  20877  bclbnd  20932  efexple  20933  bposlem1  20936  bposlem2  20937  bposlem6  20941  bposlem7  20942  chebbnd1lem3  21033  chebbnd1  21034  chtppilimlem1  21035  chtppilimlem2  21036  chpo1ubb  21043  rplogsumlem1  21046  rplogsumlem2  21047  dchrisum0lem1a  21048  rpvmasumlem  21049  dchrisumlem2  21052  dchrisumlem3  21053  dchrmusumlema  21055  dchrmusum2  21056  dchrvmasumlem1  21057  dchrvmasum2lem  21058  dchrvmasumlema  21062  dchrvmasumiflem1  21063  dchrisum0fno1  21073  dchrisum0lem1b  21077  dchrisum0lem1  21078  dchrisum0lem2  21080  dchrisum0lem3  21081  dchrisum0  21082  mulogsumlem  21093  logdivsum  21095  mulog2sumlem2  21097  vmalogdivsum2  21100  vmalogdivsum  21101  2vmadivsumlem  21102  log2sumbnd  21106  selberglem2  21108  selberg  21110  selberg2lem  21112  chpdifbndlem1  21115  chpdifbndlem2  21116  selberg3lem1  21119  selberg3  21121  selberg4lem1  21122  selberg4  21123  pntrsumbnd2  21129  selberg3r  21131  selberg4r  21132  selberg34r  21133  pntrlog2bndlem1  21139  pntrlog2bndlem2  21140  pntrlog2bndlem3  21141  pntrlog2bndlem5  21143  pntrlog2bndlem6a  21144  pntrlog2bndlem6  21145  pntrlog2bnd  21146  pntpbnd1a  21147  pntpbnd1  21148  pntpbnd2  21149  pntibndlem1  21151  pntibndlem2  21153  pntibndlem3  21154  pntibnd  21155  pntlemc  21157  pntlema  21158  pntlemb  21159  pntlemg  21160  pntlemh  21161  pntlemn  21162  pntlemq  21163  pntlemr  21164  pntlemj  21165  pntlemi  21166  pntlemf  21167  pntlemk  21168  pntlemo  21169  pntleme  21170  pntlem3  21171  pntlemp  21172  pntleml  21173  ostth2lem1  21180  ostth2lem3  21197  ostth2  21199  ostth3  21200  smcnlem  22042  blocnilem  22154  blocni  22155  ubthlem2  22222  minvecolem3  22227  minvecolem4  22231  minvecolem5  22232  nmcexi  23378  lnconi  23385  rpxdivcld  24020  sqsscirc1  24111  cnre2csqlem  24113  tpr2rico  24115  xrmulc1cn  24121  xrge0iifiso  24126  xrge0iifhom  24128  esumcst  24252  esumdivc  24270  dya2icoseg  24422  probmeasb  24468  zetacvg  24579  lgamgulmlem2  24594  lgamgulmlem5  24597  lgamucov  24602  regamcl  24625  relgamcl  24626  itg2addnclem  25958  itg2addnc  25960  itggt0cn  25978  ftc1cnnclem  25979  geomcau  26157  sstotbnd2  26175  isbnd3  26185  equivbnd  26191  prdsbnd2  26196  cntotbnd  26197  heibor1lem  26210  heiborlem6  26217  bfplem1  26223  bfplem2  26224  bfp  26225  rrndstprj2  26232  rrnequiv  26236  irrapxlem4  26580  irrapxlem5  26581  irrapx1  26583  pell1qrgaplem  26628  pell14qrgapw  26631  pellqrexplicit  26632  pellqrex  26634  pellfundge  26637  pellfundgt1  26638  rmspecfund  26664  rmxycomplete  26672  rpexpmord  26703  rmxypos  26704  fmul01lt1lem1  27383  fmul01lt1lem2  27384  stoweidlem1  27419  stoweidlem3  27421  stoweidlem5  27423  stoweidlem7  27425  stoweidlem11  27429  stoweidlem13  27431  stoweidlem14  27432  stoweidlem24  27442  stoweidlem25  27443  stoweidlem26  27444  stoweidlem34  27452  stoweidlem41  27459  stoweidlem42  27460  stoweidlem49  27467  stoweidlem51  27469  stoweidlem52  27470  stoweidlem59  27477  stoweidlem60  27478  stoweidlem62  27480  stoweid  27481  wallispilem5  27487  stirlinglem1  27492  stirlinglem4  27495  stirlinglem5  27496  stirlinglem6  27497
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rab 2659  df-in 3271  df-ss 3278  df-rp 10546
  Copyright terms: Public domain W3C validator