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

Theorem rpred 10386
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 10360 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3180 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   RRcr 8732   RR+crp 10350
This theorem is referenced by:  rpxrd  10387  rpcnd  10388  rpregt0d  10392  rprege0d  10393  rprene0d  10394  rprecred  10397  ltmulgt11d  10417  ltmulgt12d  10418  gt0divd  10419  ge0divd  10420  lediv12ad  10441  xlemul1  10605  xov1plusxeqvd  10775  ltexp2a  11148  expcan  11149  ltexp2  11150  leexp2a  11152  expnlbnd2  11227  expmulnbnd  11228  sqrlem6  11728  cau3lem  11833  rlimcld2  12047  addcn2  12062  mulcn2  12064  reccn2  12065  o1rlimmul  12087  rlimno1  12122  caucvgrlem  12140  isumrpcl  12297  isumltss  12302  expcnv  12317  mertenslem1  12335  effsumlt  12386  recoshcl  12433  eirrlem  12477  rpnnen2lem11  12498  bitsmod  12622  prmreclem3  12960  prmreclem5  12962  4sqlem7  12986  ssblex  17969  metss2lem  18052  methaus  18061  met1stc  18062  met2ndci  18063  nlmvscnlem2  18191  nlmvscnlem1  18192  nrginvrcnlem  18196  nmoi2  18234  nghmcn  18249  reperflem  18318  iccntr  18321  icccmplem2  18323  reconnlem2  18327  opnreen  18331  metdcnlem  18336  metnrmlem3  18360  addcnlem  18363  cnheibor  18448  cnllycmp  18449  lebnumlem3  18456  lebnumii  18459  nmoleub2lem  18590  nmoleub2lem3  18591  nmoleub2lem2  18592  nmoleub3  18595  nmhmcn  18596  ipcnlem2  18666  ipcnlem1  18667  lmnn  18684  iscfil3  18694  cfilfcls  18695  iscmet3lem1  18712  iscmet3lem2  18713  bcthlem4  18744  bcthlem5  18745  minveclem3b  18787  minveclem3  18788  ivthlem2  18807  ovolgelb  18834  ovollb2lem  18842  ovolunlem1a  18850  ovolunlem1  18851  ovoliunlem1  18856  ovoliunlem2  18857  ovolscalem1  18867  ioombl1lem2  18911  ioombl1lem4  18913  uniioombllem1  18931  uniioombllem3  18935  uniioombllem4  18936  uniioombllem5  18937  opnmbllem  18951  volcn  18956  vitalilem4  18961  itg2mulclem  19096  itg2monolem3  19102  itg2cnlem2  19112  itg2cn  19113  itggt0  19191  dveflem  19321  dvferm1lem  19326  dvferm2lem  19328  lhop1lem  19355  lhop1  19356  lhop  19358  dvcnvrelem1  19359  dvcnvrelem2  19360  dvcnvre  19361  dvfsumrlim  19373  ftc1a  19379  ftc1lem4  19381  plyeq0lem  19587  aalioulem2  19708  aalioulem4  19710  aalioulem5  19711  aalioulem6  19712  aaliou  19713  aaliou2b  19716  aaliou3lem1  19717  aaliou3lem2  19718  aaliou3lem8  19720  aaliou3lem5  19722  aaliou3lem7  19724  aaliou3lem9  19725  ulmcn  19771  ulmdvlem1  19772  mtest  19776  itgulm  19779  psercn  19797  pserdvlem1  19798  pserdvlem2  19799  pserdv  19800  abelthlem7  19809  pilem2  19823  divlogrlim  19977  logcnlem3  19986  logcnlem4  19987  logccv  20005  divcxp  20029  cxplt  20036  cxple2  20039  cxpcn3lem  20082  cxpaddlelem  20086  cxpaddle  20087  loglesqr  20093  leibpi  20233  rlimcnp3  20257  cxplim  20261  rlimcxp  20263  cxp2limlem  20265  cxp2lim  20266  cxploglim  20267  cxploglim2  20268  divsqrsumlem  20269  jensenlem2  20277  logdifbnd  20283  emcllem4  20287  harmonicbnd4  20299  fsumharmonic  20300  ftalem1  20305  ftalem2  20306  ftalem3  20307  ftalem5  20309  basellem1  20313  basellem3  20315  basellem4  20316  basellem8  20320  chtwordi  20389  chpchtsum  20453  logfacrlim  20458  logexprlim  20459  bclbnd  20514  efexple  20515  bposlem1  20518  bposlem2  20519  bposlem6  20523  bposlem7  20524  chebbnd1lem3  20615  chebbnd1  20616  chtppilimlem1  20617  chtppilimlem2  20618  chpo1ubb  20625  rplogsumlem1  20628  rplogsumlem2  20629  dchrisum0lem1a  20630  rpvmasumlem  20631  dchrisumlem2  20634  dchrisumlem3  20635  dchrmusumlema  20637  dchrmusum2  20638  dchrvmasumlem1  20639  dchrvmasum2lem  20640  dchrvmasumlema  20644  dchrvmasumiflem1  20645  dchrisum0fno1  20655  dchrisum0lem1b  20659  dchrisum0lem1  20660  dchrisum0lem2  20662  dchrisum0lem3  20663  dchrisum0  20664  mulogsumlem  20675  logdivsum  20677  mulog2sumlem2  20679  vmalogdivsum2  20682  vmalogdivsum  20683  2vmadivsumlem  20684  log2sumbnd  20688  selberglem2  20690  selberg  20692  selberg2lem  20694  chpdifbndlem1  20697  chpdifbndlem2  20698  selberg3lem1  20701  selberg3  20703  selberg4lem1  20704  selberg4  20705  pntrsumbnd2  20711  selberg3r  20713  selberg4r  20714  selberg34r  20715  pntrlog2bndlem1  20721  pntrlog2bndlem2  20722  pntrlog2bndlem3  20723  pntrlog2bndlem5  20725  pntrlog2bndlem6a  20726  pntrlog2bndlem6  20727  pntrlog2bnd  20728  pntpbnd1a  20729  pntpbnd1  20730  pntpbnd2  20731  pntibndlem1  20733  pntibndlem2  20735  pntibndlem3  20736  pntibnd  20737  pntlemc  20739  pntlema  20740  pntlemb  20741  pntlemg  20742  pntlemh  20743  pntlemn  20744  pntlemq  20745  pntlemr  20746  pntlemj  20747  pntlemi  20748  pntlemf  20749  pntlemk  20750  pntlemo  20751  pntleme  20752  pntlem3  20753  pntlemp  20754  pntleml  20755  ostth2lem1  20762  ostth2lem3  20779  ostth2  20781  ostth3  20782  smcnlem  21263  blocnilem  21375  blocni  21376  ubthlem2  21443  minvecolem3  21448  minvecolem4  21452  minvecolem5  21453  nmcexi  22599  lnconi  22606  zetacvg  23094  geomcau  25875  sstotbnd2  25898  isbnd3  25908  prdsbnd2  25919  cntotbnd  25920  heibor1lem  25933  heiborlem6  25940  bfplem1  25946  bfplem2  25947  bfp  25948  rrndstprj2  25955  rrnequiv  25959  irrapxlem4  26310  irrapxlem5  26311  irrapx1  26313  pell1qrgaplem  26358  pell14qrgapw  26361  pellqrexplicit  26362  pellqrex  26364  pellfundge  26367  pellfundgt1  26368  rmspecfund  26394  rmxycomplete  26402  rpexpmord  26433  rmxypos  26434  stoweidlem62  27211  wallispilem5  27218  stirlinglem1  27223  stirlinglem4  27226  stirlinglem5  27227  stirlinglem6  27228  stirlinglem12  27234
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-in 3161  df-ss 3168  df-rp 10351
  Copyright terms: Public domain W3C validator