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

Theorem rpred 10653
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 10627 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3348 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RRcr 8994   RR+crp 10617
This theorem is referenced by:  rpxrd  10654  rpcnd  10655  rpregt0d  10659  rprege0d  10660  rprene0d  10661  rprecred  10664  ltmulgt11d  10684  ltmulgt12d  10685  gt0divd  10686  ge0divd  10687  lediv12ad  10708  xlemul1  10874  xov1plusxeqvd  11046  ltexp2a  11436  expcan  11437  ltexp2  11438  leexp2a  11440  expnlbnd2  11515  expmulnbnd  11516  sqrlem6  12058  cau3lem  12163  rlimcld2  12377  addcn2  12392  mulcn2  12394  reccn2  12395  o1rlimmul  12417  rlimno1  12452  caucvgrlem  12471  isumrpcl  12628  isumltss  12633  expcnv  12648  mertenslem1  12666  effsumlt  12717  recoshcl  12764  eirrlem  12808  rpnnen2lem11  12829  bitsmod  12953  prmreclem3  13291  prmreclem5  13293  4sqlem7  13317  ssblex  18463  metss2lem  18546  methaus  18555  met1stc  18556  met2ndci  18557  metusttoOLD  18592  metustto  18593  metustexhalfOLD  18598  metustexhalf  18599  nlmvscnlem2  18726  nlmvscnlem1  18727  nrginvrcnlem  18731  nmoi2  18769  nghmcn  18784  reperflem  18854  iccntr  18857  icccmplem2  18859  reconnlem2  18863  opnreen  18867  metdcnlem  18872  metnrmlem3  18896  addcnlem  18899  cnheibor  18985  cnllycmp  18986  lebnumlem3  18993  lebnumii  18996  nmoleub2lem  19127  nmoleub2lem3  19128  nmoleub2lem2  19129  nmoleub3  19132  nmhmcn  19133  ipcnlem2  19203  ipcnlem1  19204  lmnn  19221  iscfil3  19231  cfilfcls  19232  iscmet3lem1  19249  iscmet3lem2  19250  bcthlem4  19285  bcthlem5  19286  minveclem3b  19334  minveclem3  19335  ivthlem2  19354  ovolgelb  19381  ovollb2lem  19389  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovoliunlem2  19404  ovolscalem1  19414  ioombl1lem2  19458  ioombl1lem4  19460  uniioombllem1  19478  uniioombllem3  19482  uniioombllem4  19483  uniioombllem5  19484  opnmbllem  19498  volcn  19503  vitalilem4  19508  itg2mulclem  19641  itg2monolem3  19647  itg2cnlem2  19657  itg2cn  19658  itggt0  19736  dveflem  19868  dvferm1lem  19873  dvferm2lem  19875  lhop1lem  19902  lhop1  19903  lhop  19905  dvcnvrelem1  19906  dvcnvrelem2  19907  dvcnvre  19908  dvfsumrlim  19920  ftc1a  19926  ftc1lem4  19928  plyeq0lem  20134  aalioulem2  20255  aalioulem4  20257  aalioulem5  20258  aalioulem6  20259  aaliou  20260  aaliou2b  20263  aaliou3lem1  20264  aaliou3lem2  20265  aaliou3lem8  20267  aaliou3lem5  20269  aaliou3lem7  20271  aaliou3lem9  20272  ulmcn  20320  ulmdvlem1  20321  mtest  20325  itgulm  20329  psercn  20347  pserdvlem1  20348  pserdvlem2  20349  pserdv  20350  abelthlem7  20359  pilem2  20373  divlogrlim  20531  logcnlem3  20540  logcnlem4  20541  logccv  20559  divcxp  20583  cxplt  20590  cxple2  20593  cxpcn3lem  20636  cxpaddlelem  20640  cxpaddle  20641  loglesqr  20647  leibpi  20787  rlimcnp3  20811  cxplim  20815  rlimcxp  20817  cxp2limlem  20819  cxp2lim  20820  cxploglim  20821  cxploglim2  20822  divsqrsumlem  20823  jensenlem2  20831  logdifbnd  20837  emcllem4  20842  harmonicbnd4  20854  fsumharmonic  20855  ftalem1  20860  ftalem2  20861  ftalem3  20862  ftalem5  20864  basellem1  20868  basellem3  20870  basellem4  20871  basellem8  20875  chtwordi  20944  chpchtsum  21008  logfacrlim  21013  logexprlim  21014  bclbnd  21069  efexple  21070  bposlem1  21073  bposlem2  21074  bposlem6  21078  bposlem7  21079  chebbnd1lem3  21170  chebbnd1  21171  chtppilimlem1  21172  chtppilimlem2  21173  chpo1ubb  21180  rplogsumlem1  21183  rplogsumlem2  21184  dchrisum0lem1a  21185  rpvmasumlem  21186  dchrisumlem2  21189  dchrisumlem3  21190  dchrmusumlema  21192  dchrmusum2  21193  dchrvmasumlem1  21194  dchrvmasum2lem  21195  dchrvmasumlema  21199  dchrvmasumiflem1  21200  dchrisum0fno1  21210  dchrisum0lem1b  21214  dchrisum0lem1  21215  dchrisum0lem2  21217  dchrisum0lem3  21218  dchrisum0  21219  mulogsumlem  21230  logdivsum  21232  mulog2sumlem2  21234  vmalogdivsum2  21237  vmalogdivsum  21238  2vmadivsumlem  21239  log2sumbnd  21243  selberglem2  21245  selberg  21247  selberg2lem  21249  chpdifbndlem1  21252  chpdifbndlem2  21253  selberg3lem1  21256  selberg3  21258  selberg4lem1  21259  selberg4  21260  pntrsumbnd2  21266  selberg3r  21268  selberg4r  21269  selberg34r  21270  pntrlog2bndlem1  21276  pntrlog2bndlem2  21277  pntrlog2bndlem3  21278  pntrlog2bndlem5  21280  pntrlog2bndlem6a  21281  pntrlog2bndlem6  21282  pntrlog2bnd  21283  pntpbnd1a  21284  pntpbnd1  21285  pntpbnd2  21286  pntibndlem1  21288  pntibndlem2  21290  pntibndlem3  21291  pntibnd  21292  pntlemc  21294  pntlema  21295  pntlemb  21296  pntlemg  21297  pntlemh  21298  pntlemn  21299  pntlemq  21300  pntlemr  21301  pntlemj  21302  pntlemi  21303  pntlemf  21304  pntlemk  21305  pntlemo  21306  pntleme  21307  pntlem3  21308  pntlemp  21309  pntleml  21310  ostth2lem1  21317  ostth2lem3  21334  ostth2  21336  ostth3  21337  smcnlem  22198  blocnilem  22310  blocni  22311  ubthlem2  22378  minvecolem3  22383  minvecolem4  22387  minvecolem5  22388  nmcexi  23534  lnconi  23541  rpxdivcld  24185  sqsscirc1  24311  cnre2csqlem  24313  tpr2rico  24315  xrmulc1cn  24321  xrge0iifiso  24326  xrge0iifhom  24328  esumcst  24460  esumdivc  24478  dya2icoseg  24632  probmeasb  24693  zetacvg  24804  lgamgulmlem2  24819  lgamgulmlem5  24822  lgamucov  24827  regamcl  24850  relgamcl  24851  heicant  26253  opnmbllem0  26254  mblfinlem3  26257  itg2addnclem3  26272  itg2addnc  26273  itggt0cn  26291  ftc1cnnclem  26292  ftc1anclem6  26299  ftc1anclem7  26300  geomcau  26479  sstotbnd2  26497  isbnd3  26507  equivbnd  26513  prdsbnd2  26518  cntotbnd  26519  heibor1lem  26532  heiborlem6  26539  bfplem1  26545  bfplem2  26546  bfp  26547  rrndstprj2  26554  rrnequiv  26558  irrapxlem4  26902  irrapxlem5  26903  irrapx1  26905  pell1qrgaplem  26950  pell14qrgapw  26953  pellqrexplicit  26954  pellqrex  26956  pellfundge  26959  pellfundgt1  26960  rmspecfund  26986  rmxycomplete  26994  rpexpmord  27025  rmxypos  27026  fmul01lt1lem1  27704  fmul01lt1lem2  27705  stoweidlem1  27740  stoweidlem3  27742  stoweidlem5  27744  stoweidlem7  27746  stoweidlem11  27750  stoweidlem13  27752  stoweidlem14  27753  stoweidlem24  27763  stoweidlem25  27764  stoweidlem26  27765  stoweidlem34  27773  stoweidlem41  27780  stoweidlem42  27781  stoweidlem49  27788  stoweidlem51  27790  stoweidlem52  27791  stoweidlem59  27798  stoweidlem60  27799  stoweidlem62  27801  stoweid  27802  wallispilem5  27808  stirlinglem1  27813  stirlinglem4  27816  stirlinglem5  27817  stirlinglem6  27818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-in 3329  df-ss 3336  df-rp 10618
  Copyright terms: Public domain W3C validator