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

Theorem rpred 11252
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 11226 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3502 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   RRcr 9487   RR+crp 11216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-in 3483  df-ss 3490  df-rp 11217
This theorem is referenced by:  rpxrd  11253  rpcnd  11254  rpregt0d  11258  rprege0d  11259  rprene0d  11260  rprecred  11263  ltmulgt11d  11283  ltmulgt12d  11284  gt0divd  11285  ge0divd  11286  lediv12ad  11307  xlemul1  11478  xov1plusxeqvd  11662  ltexp2a  12179  expcan  12180  ltexp2  12181  leexp2a  12183  expnlbnd2  12259  expmulnbnd  12260  sqrlem6  13038  cau3lem  13143  rlimcld2  13357  addcn2  13372  mulcn2  13374  reccn2  13375  o1rlimmul  13397  rlimno1  13432  caucvgrlem  13451  isumrpcl  13611  isumltss  13616  expcnv  13631  mertenslem1  13649  effsumlt  13700  recoshcl  13747  eirrlem  13791  rpnnen2lem11  13812  bitsmod  13938  prmreclem3  14288  prmreclem5  14290  4sqlem7  14314  ssblex  20663  metss2lem  20746  methaus  20755  met1stc  20756  met2ndci  20757  metusttoOLD  20792  metustto  20793  metustexhalfOLD  20798  metustexhalf  20799  nlmvscnlem2  20926  nlmvscnlem1  20927  nrginvrcnlem  20931  nmoi2  20969  nghmcn  20984  reperflem  21055  iccntr  21058  icccmplem2  21060  reconnlem2  21064  opnreen  21068  metdcnlem  21073  metnrmlem3  21097  addcnlem  21100  cnheibor  21187  cnllycmp  21188  lebnumlem3  21195  lebnumii  21198  nmoleub2lem  21329  nmoleub2lem3  21330  nmoleub2lem2  21331  nmoleub3  21334  nmhmcn  21335  ipcnlem2  21416  ipcnlem1  21417  lmnn  21434  iscfil3  21444  cfilfcls  21445  iscmet3lem1  21462  iscmet3lem2  21463  bcthlem4  21498  bcthlem5  21499  minveclem3b  21575  minveclem3  21576  ivthlem2  21596  ovolgelb  21623  ovollb2lem  21631  ovolunlem1a  21639  ovolunlem1  21640  ovoliunlem1  21645  ovoliunlem2  21646  ovolscalem1  21656  ioombl1lem2  21701  ioombl1lem4  21703  uniioombllem1  21722  uniioombllem3  21726  uniioombllem4  21727  uniioombllem5  21728  opnmbllem  21742  volcn  21747  vitalilem4  21752  itg2mulclem  21885  itg2monolem3  21891  itg2cnlem2  21901  itg2cn  21902  itggt0  21980  dveflem  22112  dvferm1lem  22117  dvferm2lem  22119  lhop1lem  22146  lhop1  22147  lhop  22149  dvcnvrelem1  22150  dvcnvrelem2  22151  dvcnvre  22152  dvfsumrlim  22164  ftc1a  22170  ftc1lem4  22172  plyeq0lem  22339  aalioulem2  22460  aalioulem4  22462  aalioulem5  22463  aalioulem6  22464  aaliou  22465  aaliou2b  22468  aaliou3lem1  22469  aaliou3lem2  22470  aaliou3lem8  22472  aaliou3lem5  22474  aaliou3lem7  22476  aaliou3lem9  22477  ulmcn  22525  ulmdvlem1  22526  mtest  22530  itgulm  22534  psercn  22552  pserdvlem1  22553  pserdvlem2  22554  pserdv  22555  abelthlem7  22564  pilem2  22578  divlogrlim  22741  logcnlem3  22750  logcnlem4  22751  logccv  22769  divcxp  22793  cxplt  22800  cxple2  22803  cxpcn3lem  22846  cxpaddlelem  22850  cxpaddle  22851  loglesqrt  22857  leibpi  22998  rlimcnp3  23022  cxplim  23026  rlimcxp  23028  cxp2limlem  23030  cxp2lim  23031  cxploglim  23032  cxploglim2  23033  divsqrtsumlem  23034  jensenlem2  23042  logdifbnd  23048  emcllem4  23053  harmonicbnd4  23065  fsumharmonic  23066  ftalem1  23071  ftalem2  23072  ftalem3  23073  ftalem5  23075  basellem1  23079  basellem3  23081  basellem4  23082  basellem8  23086  chtwordi  23155  chpchtsum  23219  logfacrlim  23224  logexprlim  23225  bclbnd  23280  efexple  23281  bposlem1  23284  bposlem2  23285  bposlem6  23289  bposlem7  23290  chebbnd1lem3  23381  chebbnd1  23382  chtppilimlem1  23383  chtppilimlem2  23384  chpo1ubb  23391  rplogsumlem1  23394  rplogsumlem2  23395  dchrisum0lem1a  23396  rpvmasumlem  23397  dchrisumlem2  23400  dchrisumlem3  23401  dchrmusumlema  23403  dchrmusum2  23404  dchrvmasumlem1  23405  dchrvmasum2lem  23406  dchrvmasumlema  23410  dchrvmasumiflem1  23411  dchrisum0fno1  23421  dchrisum0lem1b  23425  dchrisum0lem1  23426  dchrisum0lem2  23428  dchrisum0lem3  23429  dchrisum0  23430  mulogsumlem  23441  logdivsum  23443  mulog2sumlem2  23445  vmalogdivsum2  23448  2vmadivsumlem  23450  log2sumbnd  23454  selberglem2  23456  selberg  23458  selberg2lem  23460  chpdifbndlem1  23463  chpdifbndlem2  23464  selberg3lem1  23467  selberg4lem1  23470  pntrsumbnd2  23477  pntrlog2bndlem2  23488  pntrlog2bndlem3  23489  pntrlog2bndlem5  23491  pntrlog2bndlem6a  23492  pntrlog2bndlem6  23493  pntrlog2bnd  23494  pntpbnd1a  23495  pntpbnd1  23496  pntpbnd2  23497  pntibndlem1  23499  pntibndlem2  23501  pntibndlem3  23502  pntibnd  23503  pntlemc  23505  pntlema  23506  pntlemb  23507  pntlemg  23508  pntlemh  23509  pntlemn  23510  pntlemq  23511  pntlemr  23512  pntlemj  23513  pntlemi  23514  pntlemf  23515  pntlemk  23516  pntlemo  23517  pntleme  23518  pntlem3  23519  pntlemp  23520  pntleml  23521  ostth2lem1  23528  ostth2lem3  23545  ostth2  23547  ostth3  23548  smcnlem  25280  blocnilem  25392  blocni  25393  ubthlem2  25460  minvecolem3  25465  minvecolem4  25469  minvecolem5  25470  nmcexi  26618  lnconi  26625  rpxdivcld  27295  sqsscirc1  27523  cnre2csqlem  27525  tpr2rico  27527  xrmulc1cn  27545  xrge0iifiso  27550  xrge0iifhom  27552  esumcst  27708  esumdivc  27726  dya2icoseg  27885  probmeasb  28006  sgnmulrp2  28119  signshf  28182  zetacvg  28194  lgamgulmlem2  28209  lgamgulmlem5  28212  lgamucov  28217  regamcl  28240  relgamcl  28241  heicant  29624  opnmbllem0  29625  mblfinlem3  29628  itg2addnclem3  29643  itg2addnc  29644  itggt0cn  29662  ftc1cnnclem  29663  ftc1anclem6  29670  ftc1anclem7  29671  geomcau  29853  sstotbnd2  29871  isbnd3  29881  equivbnd  29887  prdsbnd2  29892  cntotbnd  29893  heibor1lem  29906  heiborlem6  29913  bfplem1  29919  bfplem2  29920  bfp  29921  rrndstprj2  29928  rrnequiv  29932  irrapxlem4  30363  irrapxlem5  30364  irrapx1  30366  pell1qrgaplem  30411  pell14qrgapw  30414  pellqrexplicit  30415  pellqrex  30417  pellfundge  30420  pellfundgt1  30421  rmspecfund  30447  rmxycomplete  30455  rpexpmord  30486  rmxypos  30487  lefldiveq  31059  fmul01lt1lem1  31134  fmul01lt1lem2  31135  ltmod  31180  lptre2pt  31182  addlimc  31190  0ellimcdiv  31191  limclner  31193  dvdivbd  31253  itgiccshift  31298  itgperiod  31299  stoweidlem1  31301  stoweidlem3  31303  stoweidlem5  31305  stoweidlem7  31307  stoweidlem11  31311  stoweidlem13  31313  stoweidlem14  31314  stoweidlem24  31324  stoweidlem25  31325  stoweidlem26  31326  stoweidlem34  31334  stoweidlem41  31341  stoweidlem42  31342  stoweidlem49  31349  stoweidlem51  31351  stoweidlem52  31352  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  stoweid  31363  wallispilem5  31369  stirlinglem1  31374  stirlinglem4  31377  stirlinglem5  31378  stirlinglem6  31379  dirkercncflem1  31403  fourierdlem30  31437  fourierdlem39  31446  fourierdlem47  31454  fourierdlem73  31480  fourierdlem81  31488  fourierdlem87  31494  fourierdlem103  31510  fourierdlem104  31511  fourierdlem107  31514
  Copyright terms: Public domain W3C validator