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

Theorem rpred 11128
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 11102 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3452 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   RRcr 9382   RR+crp 11092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-in 3433  df-ss 3440  df-rp 11093
This theorem is referenced by:  rpxrd  11129  rpcnd  11130  rpregt0d  11134  rprege0d  11135  rprene0d  11136  rprecred  11139  ltmulgt11d  11159  ltmulgt12d  11160  gt0divd  11161  ge0divd  11162  lediv12ad  11183  xlemul1  11354  xov1plusxeqvd  11532  ltexp2a  12016  expcan  12017  ltexp2  12018  leexp2a  12020  expnlbnd2  12096  expmulnbnd  12097  sqrlem6  12839  cau3lem  12944  rlimcld2  13158  addcn2  13173  mulcn2  13175  reccn2  13176  o1rlimmul  13198  rlimno1  13233  caucvgrlem  13252  isumrpcl  13408  isumltss  13413  expcnv  13428  mertenslem1  13446  effsumlt  13497  recoshcl  13544  eirrlem  13588  rpnnen2lem11  13609  bitsmod  13734  prmreclem3  14081  prmreclem5  14083  4sqlem7  14107  ssblex  20119  metss2lem  20202  methaus  20211  met1stc  20212  met2ndci  20213  metusttoOLD  20248  metustto  20249  metustexhalfOLD  20254  metustexhalf  20255  nlmvscnlem2  20382  nlmvscnlem1  20383  nrginvrcnlem  20387  nmoi2  20425  nghmcn  20440  reperflem  20511  iccntr  20514  icccmplem2  20516  reconnlem2  20520  opnreen  20524  metdcnlem  20529  metnrmlem3  20553  addcnlem  20556  cnheibor  20643  cnllycmp  20644  lebnumlem3  20651  lebnumii  20654  nmoleub2lem  20785  nmoleub2lem3  20786  nmoleub2lem2  20787  nmoleub3  20790  nmhmcn  20791  ipcnlem2  20872  ipcnlem1  20873  lmnn  20890  iscfil3  20900  cfilfcls  20901  iscmet3lem1  20918  iscmet3lem2  20919  bcthlem4  20954  bcthlem5  20955  minveclem3b  21031  minveclem3  21032  ivthlem2  21052  ovolgelb  21079  ovollb2lem  21087  ovolunlem1a  21095  ovolunlem1  21096  ovoliunlem1  21101  ovoliunlem2  21102  ovolscalem1  21112  ioombl1lem2  21156  ioombl1lem4  21158  uniioombllem1  21177  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  opnmbllem  21197  volcn  21202  vitalilem4  21207  itg2mulclem  21340  itg2monolem3  21346  itg2cnlem2  21356  itg2cn  21357  itggt0  21435  dveflem  21567  dvferm1lem  21572  dvferm2lem  21574  lhop1lem  21601  lhop1  21602  lhop  21604  dvcnvrelem1  21605  dvcnvrelem2  21606  dvcnvre  21607  dvfsumrlim  21619  ftc1a  21625  ftc1lem4  21627  plyeq0lem  21794  aalioulem2  21915  aalioulem4  21917  aalioulem5  21918  aalioulem6  21919  aaliou  21920  aaliou2b  21923  aaliou3lem1  21924  aaliou3lem2  21925  aaliou3lem8  21927  aaliou3lem5  21929  aaliou3lem7  21931  aaliou3lem9  21932  ulmcn  21980  ulmdvlem1  21981  mtest  21985  itgulm  21989  psercn  22007  pserdvlem1  22008  pserdvlem2  22009  pserdv  22010  abelthlem7  22019  pilem2  22033  divlogrlim  22196  logcnlem3  22205  logcnlem4  22206  logccv  22224  divcxp  22248  cxplt  22255  cxple2  22258  cxpcn3lem  22301  cxpaddlelem  22305  cxpaddle  22306  loglesqr  22312  leibpi  22453  rlimcnp3  22477  cxplim  22481  rlimcxp  22483  cxp2limlem  22485  cxp2lim  22486  cxploglim  22487  cxploglim2  22488  divsqrsumlem  22489  jensenlem2  22497  logdifbnd  22503  emcllem4  22508  harmonicbnd4  22520  fsumharmonic  22521  ftalem1  22526  ftalem2  22527  ftalem3  22528  ftalem5  22530  basellem1  22534  basellem3  22536  basellem4  22537  basellem8  22541  chtwordi  22610  chpchtsum  22674  logfacrlim  22679  logexprlim  22680  bclbnd  22735  efexple  22736  bposlem1  22739  bposlem2  22740  bposlem6  22744  bposlem7  22745  chebbnd1lem3  22836  chebbnd1  22837  chtppilimlem1  22838  chtppilimlem2  22839  chpo1ubb  22846  rplogsumlem1  22849  rplogsumlem2  22850  dchrisum0lem1a  22851  rpvmasumlem  22852  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusumlema  22858  dchrmusum2  22859  dchrvmasumlem1  22860  dchrvmasum2lem  22861  dchrvmasumlema  22865  dchrvmasumiflem1  22866  dchrisum0fno1  22876  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2  22883  dchrisum0lem3  22884  dchrisum0  22885  mulogsumlem  22896  logdivsum  22898  mulog2sumlem2  22900  vmalogdivsum2  22903  2vmadivsumlem  22905  log2sumbnd  22909  selberglem2  22911  selberg  22913  selberg2lem  22915  chpdifbndlem1  22918  chpdifbndlem2  22919  selberg3lem1  22922  selberg4lem1  22925  pntrsumbnd2  22932  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem5  22946  pntrlog2bndlem6a  22947  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem1  22954  pntibndlem2  22956  pntibndlem3  22957  pntibnd  22958  pntlemc  22960  pntlema  22961  pntlemb  22962  pntlemg  22963  pntlemh  22964  pntlemn  22965  pntlemq  22966  pntlemr  22967  pntlemj  22968  pntlemi  22969  pntlemf  22970  pntlemk  22971  pntlemo  22972  pntleme  22973  pntlem3  22974  pntlemp  22975  pntleml  22976  ostth2lem1  22983  ostth2lem3  23000  ostth2  23002  ostth3  23003  smcnlem  24227  blocnilem  24339  blocni  24340  ubthlem2  24407  minvecolem3  24412  minvecolem4  24416  minvecolem5  24417  nmcexi  25565  lnconi  25572  rpxdivcld  26243  sqsscirc1  26472  cnre2csqlem  26474  tpr2rico  26476  xrmulc1cn  26494  xrge0iifiso  26499  xrge0iifhom  26501  esumcst  26648  esumdivc  26666  dya2icoseg  26826  probmeasb  26947  sgnmulrp2  27060  signshf  27123  zetacvg  27135  lgamgulmlem2  27150  lgamgulmlem5  27153  lgamucov  27158  regamcl  27181  relgamcl  27182  heicant  28564  opnmbllem0  28565  mblfinlem3  28568  itg2addnclem3  28583  itg2addnc  28584  itggt0cn  28602  ftc1cnnclem  28603  ftc1anclem6  28610  ftc1anclem7  28611  geomcau  28793  sstotbnd2  28811  isbnd3  28821  equivbnd  28827  prdsbnd2  28832  cntotbnd  28833  heibor1lem  28846  heiborlem6  28853  bfplem1  28859  bfplem2  28860  bfp  28861  rrndstprj2  28868  rrnequiv  28872  irrapxlem4  29304  irrapxlem5  29305  irrapx1  29307  pell1qrgaplem  29352  pell14qrgapw  29355  pellqrexplicit  29356  pellqrex  29358  pellfundge  29361  pellfundgt1  29362  rmspecfund  29388  rmxycomplete  29396  rpexpmord  29427  rmxypos  29428  fmul01lt1lem1  29903  fmul01lt1lem2  29904  stoweidlem1  29934  stoweidlem3  29936  stoweidlem5  29938  stoweidlem7  29940  stoweidlem11  29944  stoweidlem13  29946  stoweidlem14  29947  stoweidlem24  29957  stoweidlem25  29958  stoweidlem26  29959  stoweidlem34  29967  stoweidlem41  29974  stoweidlem42  29975  stoweidlem49  29982  stoweidlem51  29984  stoweidlem52  29985  stoweidlem59  29992  stoweidlem60  29993  stoweidlem62  29995  stoweid  29996  wallispilem5  30002  stirlinglem1  30007  stirlinglem4  30010  stirlinglem5  30011  stirlinglem6  30012
  Copyright terms: Public domain W3C validator