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

Theorem rpred 10604
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 10578 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3306 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   RRcr 8945   RR+crp 10568
This theorem is referenced by:  rpxrd  10605  rpcnd  10606  rpregt0d  10610  rprege0d  10611  rprene0d  10612  rprecred  10615  ltmulgt11d  10635  ltmulgt12d  10636  gt0divd  10637  ge0divd  10638  lediv12ad  10659  xlemul1  10825  xov1plusxeqvd  10997  ltexp2a  11386  expcan  11387  ltexp2  11388  leexp2a  11390  expnlbnd2  11465  expmulnbnd  11466  sqrlem6  12008  cau3lem  12113  rlimcld2  12327  addcn2  12342  mulcn2  12344  reccn2  12345  o1rlimmul  12367  rlimno1  12402  caucvgrlem  12421  isumrpcl  12578  isumltss  12583  expcnv  12598  mertenslem1  12616  effsumlt  12667  recoshcl  12714  eirrlem  12758  rpnnen2lem11  12779  bitsmod  12903  prmreclem3  13241  prmreclem5  13243  4sqlem7  13267  ssblex  18411  metss2lem  18494  methaus  18503  met1stc  18504  met2ndci  18505  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  nlmvscnlem2  18674  nlmvscnlem1  18675  nrginvrcnlem  18679  nmoi2  18717  nghmcn  18732  reperflem  18802  iccntr  18805  icccmplem2  18807  reconnlem2  18811  opnreen  18815  metdcnlem  18820  metnrmlem3  18844  addcnlem  18847  cnheibor  18933  cnllycmp  18934  lebnumlem3  18941  lebnumii  18944  nmoleub2lem  19075  nmoleub2lem3  19076  nmoleub2lem2  19077  nmoleub3  19080  nmhmcn  19081  ipcnlem2  19151  ipcnlem1  19152  lmnn  19169  iscfil3  19179  cfilfcls  19180  iscmet3lem1  19197  iscmet3lem2  19198  bcthlem4  19233  bcthlem5  19234  minveclem3b  19282  minveclem3  19283  ivthlem2  19302  ovolgelb  19329  ovollb2lem  19337  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovolscalem1  19362  ioombl1lem2  19406  ioombl1lem4  19408  uniioombllem1  19426  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  opnmbllem  19446  volcn  19451  vitalilem4  19456  itg2mulclem  19591  itg2monolem3  19597  itg2cnlem2  19607  itg2cn  19608  itggt0  19686  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  lhop1lem  19850  lhop1  19851  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  dvfsumrlim  19868  ftc1a  19874  ftc1lem4  19876  plyeq0lem  20082  aalioulem2  20203  aalioulem4  20205  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou2b  20211  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem5  20217  aaliou3lem7  20219  aaliou3lem9  20220  ulmcn  20268  ulmdvlem1  20269  mtest  20273  itgulm  20277  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  abelthlem7  20307  pilem2  20321  divlogrlim  20479  logcnlem3  20488  logcnlem4  20489  logccv  20507  divcxp  20531  cxplt  20538  cxple2  20541  cxpcn3lem  20584  cxpaddlelem  20588  cxpaddle  20589  loglesqr  20595  leibpi  20735  rlimcnp3  20759  cxplim  20763  rlimcxp  20765  cxp2limlem  20767  cxp2lim  20768  cxploglim  20769  cxploglim2  20770  divsqrsumlem  20771  jensenlem2  20779  logdifbnd  20785  emcllem4  20790  harmonicbnd4  20802  fsumharmonic  20803  ftalem1  20808  ftalem2  20809  ftalem3  20810  ftalem5  20812  basellem1  20816  basellem3  20818  basellem4  20819  basellem8  20823  chtwordi  20892  chpchtsum  20956  logfacrlim  20961  logexprlim  20962  bclbnd  21017  efexple  21018  bposlem1  21021  bposlem2  21022  bposlem6  21026  bposlem7  21027  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  chtppilimlem2  21121  chpo1ubb  21128  rplogsumlem1  21131  rplogsumlem2  21132  dchrisum0lem1a  21133  rpvmasumlem  21134  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasumlema  21147  dchrvmasumiflem1  21148  dchrisum0fno1  21158  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrisum0  21167  mulogsumlem  21178  logdivsum  21180  mulog2sumlem2  21182  vmalogdivsum2  21185  vmalogdivsum  21186  2vmadivsumlem  21187  log2sumbnd  21191  selberglem2  21193  selberg  21195  selberg2lem  21197  chpdifbndlem1  21200  chpdifbndlem2  21201  selberg3lem1  21204  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrsumbnd2  21214  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6a  21229  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem1  21236  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemc  21242  pntlema  21243  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemn  21247  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemi  21251  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntleme  21255  pntlem3  21256  pntlemp  21257  pntleml  21258  ostth2lem1  21265  ostth2lem3  21282  ostth2  21284  ostth3  21285  smcnlem  22146  blocnilem  22258  blocni  22259  ubthlem2  22326  minvecolem3  22331  minvecolem4  22335  minvecolem5  22336  nmcexi  23482  lnconi  23489  rpxdivcld  24133  sqsscirc1  24259  cnre2csqlem  24261  tpr2rico  24263  xrmulc1cn  24269  xrge0iifiso  24274  xrge0iifhom  24276  esumcst  24408  esumdivc  24426  dya2icoseg  24580  probmeasb  24641  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem5  24770  lgamucov  24775  regamcl  24798  relgamcl  24799  mblfinlem  26143  mblfinlem2  26144  itg2addnclem3  26157  itg2addnc  26158  itggt0cn  26176  ftc1cnnclem  26177  geomcau  26355  sstotbnd2  26373  isbnd3  26383  equivbnd  26389  prdsbnd2  26394  cntotbnd  26395  heibor1lem  26408  heiborlem6  26415  bfplem1  26421  bfplem2  26422  bfp  26423  rrndstprj2  26430  rrnequiv  26434  irrapxlem4  26778  irrapxlem5  26779  irrapx1  26781  pell1qrgaplem  26826  pell14qrgapw  26829  pellqrexplicit  26830  pellqrex  26832  pellfundge  26835  pellfundgt1  26836  rmspecfund  26862  rmxycomplete  26870  rpexpmord  26901  rmxypos  26902  fmul01lt1lem1  27581  fmul01lt1lem2  27582  stoweidlem1  27617  stoweidlem3  27619  stoweidlem5  27621  stoweidlem7  27623  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem24  27640  stoweidlem25  27641  stoweidlem26  27642  stoweidlem34  27650  stoweidlem41  27657  stoweidlem42  27658  stoweidlem49  27665  stoweidlem51  27667  stoweidlem52  27668  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  stoweid  27679  wallispilem5  27685  stirlinglem1  27690  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-in 3287  df-ss 3294  df-rp 10569
  Copyright terms: Public domain W3C validator