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

Theorem rpred 11222
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 11193 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3439 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   RRcr 9441   RR+crp 11183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-in 3420  df-ss 3427  df-rp 11184
This theorem is referenced by:  rpxrd  11223  rpcnd  11224  rpregt0d  11228  rprege0d  11229  rprene0d  11230  rprecred  11233  ltmulgt11d  11253  ltmulgt12d  11254  gt0divd  11255  ge0divd  11256  lediv12ad  11277  xlemul1  11453  xov1plusxeqvd  11637  ltexp2a  12172  expcan  12173  ltexp2  12174  leexp2a  12176  expnlbnd2  12251  expmulnbnd  12252  sqrlem6  13137  cau3lem  13243  rlimcld2  13457  addcn2  13472  mulcn2  13474  reccn2  13475  o1rlimmul  13497  rlimno1  13532  caucvgrlem  13551  isumrpcl  13713  isumltss  13718  expcnv  13734  mertenslem1  13752  effsumlt  13947  recoshcl  13994  eirrlem  14038  rpnnen2lem11  14059  bitsmod  14187  prmreclem3  14537  prmreclem5  14539  4sqlem7  14563  ssblex  21115  metss2lem  21198  methaus  21207  met1stc  21208  met2ndci  21209  metusttoOLD  21244  metustto  21245  metustexhalfOLD  21250  metustexhalf  21251  nlmvscnlem2  21378  nlmvscnlem1  21379  nrginvrcnlem  21383  nmoi2  21421  nghmcn  21436  reperflem  21507  iccntr  21510  icccmplem2  21512  reconnlem2  21516  opnreen  21520  metdcnlem  21525  metnrmlem3  21549  addcnlem  21552  cnheibor  21639  cnllycmp  21640  lebnumlem3  21647  lebnumii  21650  nmoleub2lem  21781  nmoleub2lem3  21782  nmoleub2lem2  21783  nmoleub3  21786  nmhmcn  21787  ipcnlem2  21868  ipcnlem1  21869  lmnn  21886  iscfil3  21896  cfilfcls  21897  iscmet3lem1  21914  iscmet3lem2  21915  bcthlem4  21950  bcthlem5  21951  minveclem3b  22027  minveclem3  22028  ivthlem2  22048  ovolgelb  22075  ovollb2lem  22083  ovolunlem1a  22091  ovolunlem1  22092  ovoliunlem1  22097  ovoliunlem2  22098  ovolscalem1  22108  ioombl1lem2  22153  ioombl1lem4  22155  uniioombllem1  22174  uniioombllem3  22178  uniioombllem4  22179  uniioombllem5  22180  opnmbllem  22194  volcn  22199  vitalilem4  22204  itg2mulclem  22337  itg2monolem3  22343  itg2cnlem2  22353  itg2cn  22354  itggt0  22432  dveflem  22564  dvferm1lem  22569  dvferm2lem  22571  lhop1lem  22598  lhop1  22599  lhop  22601  dvcnvrelem1  22602  dvcnvrelem2  22603  dvcnvre  22604  dvfsumrlim  22616  ftc1a  22622  ftc1lem4  22624  plyeq0lem  22791  aalioulem2  22913  aalioulem4  22915  aalioulem5  22916  aalioulem6  22917  aaliou  22918  aaliou2b  22921  aaliou3lem1  22922  aaliou3lem2  22923  aaliou3lem8  22925  aaliou3lem5  22927  aaliou3lem7  22929  aaliou3lem9  22930  ulmcn  22978  ulmdvlem1  22979  mtest  22983  itgulm  22987  psercn  23005  pserdvlem1  23006  pserdvlem2  23007  pserdv  23008  abelthlem7  23017  pilem2  23031  divlogrlim  23202  logcnlem3  23211  logcnlem4  23212  logccv  23230  divcxp  23254  cxplt  23261  cxple2  23264  cxpcn3lem  23309  cxpaddlelem  23313  cxpaddle  23314  loglesqrt  23320  leibpi  23490  rlimcnp3  23515  cxplim  23519  rlimcxp  23521  cxp2limlem  23523  cxp2lim  23524  cxploglim  23525  cxploglim2  23526  divsqrtsumlem  23527  jensenlem2  23535  logdifbnd  23541  emcllem4  23546  harmonicbnd4  23558  fsumharmonic  23559  zetacvg  23562  lgamgulmlem2  23577  lgamgulmlem5  23580  lgamucov  23585  regamcl  23608  relgamcl  23609  ftalem1  23619  ftalem2  23620  ftalem3  23621  ftalem5  23623  basellem1  23627  basellem3  23629  basellem4  23630  basellem8  23634  chtwordi  23703  chpchtsum  23767  logfacrlim  23772  logexprlim  23773  bclbnd  23828  efexple  23829  bposlem1  23832  bposlem2  23833  bposlem6  23837  bposlem7  23838  chebbnd1lem3  23929  chebbnd1  23930  chtppilimlem1  23931  chtppilimlem2  23932  chpo1ubb  23939  rplogsumlem1  23942  rplogsumlem2  23943  dchrisum0lem1a  23944  rpvmasumlem  23945  dchrisumlem2  23948  dchrisumlem3  23949  dchrmusumlema  23951  dchrmusum2  23952  dchrvmasumlem1  23953  dchrvmasum2lem  23954  dchrvmasumlema  23958  dchrvmasumiflem1  23959  dchrisum0fno1  23969  dchrisum0lem1b  23973  dchrisum0lem1  23974  dchrisum0lem2  23976  dchrisum0lem3  23977  dchrisum0  23978  mulogsumlem  23989  logdivsum  23991  mulog2sumlem2  23993  vmalogdivsum2  23996  2vmadivsumlem  23998  log2sumbnd  24002  selberglem2  24004  selberg  24006  selberg2lem  24008  chpdifbndlem1  24011  chpdifbndlem2  24012  selberg3lem1  24015  selberg4lem1  24018  pntrsumbnd2  24025  pntrlog2bndlem2  24036  pntrlog2bndlem3  24037  pntrlog2bndlem5  24039  pntrlog2bndlem6a  24040  pntrlog2bndlem6  24041  pntrlog2bnd  24042  pntpbnd1a  24043  pntpbnd1  24044  pntpbnd2  24045  pntibndlem1  24047  pntibndlem2  24049  pntibndlem3  24050  pntibnd  24051  pntlemc  24053  pntlema  24054  pntlemb  24055  pntlemg  24056  pntlemh  24057  pntlemn  24058  pntlemq  24059  pntlemr  24060  pntlemj  24061  pntlemi  24062  pntlemf  24063  pntlemk  24064  pntlemo  24065  pntleme  24066  pntlem3  24067  pntlemp  24068  pntleml  24069  ostth2lem1  24076  ostth2lem3  24093  ostth2  24095  ostth3  24096  smcnlem  25901  blocnilem  26013  blocni  26014  ubthlem2  26081  minvecolem3  26086  minvecolem4  26090  minvecolem5  26091  nmcexi  27238  lnconi  27245  rpxdivcld  27962  sqsscirc1  28223  cnre2csqlem  28225  tpr2rico  28227  xrmulc1cn  28245  xrge0iifiso  28250  xrge0iifhom  28252  esumcst  28390  esumdivc  28410  dya2icoseg  28605  omssubaddlem  28627  omssubadd  28628  probmeasb  28755  sgnmulrp2  28868  signsply0  28894  signshf  28931  heicant  31402  opnmbllem0  31403  mblfinlem3  31406  itg2addnclem3  31422  itg2addnc  31423  itggt0cn  31441  ftc1cnnclem  31442  ftc1anclem6  31449  ftc1anclem7  31450  geomcau  31515  sstotbnd2  31533  isbnd3  31543  equivbnd  31549  prdsbnd2  31554  cntotbnd  31555  heibor1lem  31568  heiborlem6  31575  bfplem1  31581  bfplem2  31582  bfp  31583  rrndstprj2  31590  rrnequiv  31594  irrapxlem4  35103  irrapxlem5  35104  irrapx1  35106  pell1qrgaplem  35151  pell14qrgapw  35154  pellqrexplicit  35155  pellqrex  35157  pellfundge  35160  pellfundgt1  35161  rmspecfund  35187  rmxycomplete  35195  rpexpmord  35226  rmxypos  35227  binomcxplemnotnn0  36090  fmul01lt1lem1  36928  fmul01lt1lem2  36929  ltmod  36994  lptre2pt  36996  addlimc  37004  0ellimcdiv  37005  limclner  37007  dvdivbd  37070  ioodvbdlimc1lem2  37079  ioodvbdlimc2lem  37081  itgiccshift  37129  itgperiod  37130  stoweidlem1  37133  stoweidlem3  37135  stoweidlem5  37137  stoweidlem7  37139  stoweidlem11  37143  stoweidlem13  37145  stoweidlem14  37146  stoweidlem24  37156  stoweidlem25  37157  stoweidlem26  37158  stoweidlem34  37166  stoweidlem41  37173  stoweidlem42  37174  stoweidlem49  37181  stoweidlem51  37183  stoweidlem52  37184  stoweidlem59  37191  stoweidlem60  37192  stoweidlem62  37194  stoweid  37195  wallispilem5  37201  stirlinglem1  37206  stirlinglem4  37209  stirlinglem5  37210  stirlinglem6  37211  dirkercncflem1  37235  fourierdlem30  37269  fourierdlem39  37278  fourierdlem47  37286  fourierdlem73  37312  fourierdlem81  37320  fourierdlem87  37326  fourierdlem103  37342  fourierdlem104  37343  fourierdlem107  37346  modexp2m1d  37838  dignn0flhalflem1  38726
  Copyright terms: Public domain W3C validator