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

Theorem rpred 10637
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 10611 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3338 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RRcr 8978   RR+crp 10601
This theorem is referenced by:  rpxrd  10638  rpcnd  10639  rpregt0d  10643  rprege0d  10644  rprene0d  10645  rprecred  10648  ltmulgt11d  10668  ltmulgt12d  10669  gt0divd  10670  ge0divd  10671  lediv12ad  10692  xlemul1  10858  xov1plusxeqvd  11030  ltexp2a  11419  expcan  11420  ltexp2  11421  leexp2a  11423  expnlbnd2  11498  expmulnbnd  11499  sqrlem6  12041  cau3lem  12146  rlimcld2  12360  addcn2  12375  mulcn2  12377  reccn2  12378  o1rlimmul  12400  rlimno1  12435  caucvgrlem  12454  isumrpcl  12611  isumltss  12616  expcnv  12631  mertenslem1  12649  effsumlt  12700  recoshcl  12747  eirrlem  12791  rpnnen2lem11  12812  bitsmod  12936  prmreclem3  13274  prmreclem5  13276  4sqlem7  13300  ssblex  18446  metss2lem  18529  methaus  18538  met1stc  18539  met2ndci  18540  metusttoOLD  18575  metustto  18576  metustexhalfOLD  18581  metustexhalf  18582  nlmvscnlem2  18709  nlmvscnlem1  18710  nrginvrcnlem  18714  nmoi2  18752  nghmcn  18767  reperflem  18837  iccntr  18840  icccmplem2  18842  reconnlem2  18846  opnreen  18850  metdcnlem  18855  metnrmlem3  18879  addcnlem  18882  cnheibor  18968  cnllycmp  18969  lebnumlem3  18976  lebnumii  18979  nmoleub2lem  19110  nmoleub2lem3  19111  nmoleub2lem2  19112  nmoleub3  19115  nmhmcn  19116  ipcnlem2  19186  ipcnlem1  19187  lmnn  19204  iscfil3  19214  cfilfcls  19215  iscmet3lem1  19232  iscmet3lem2  19233  bcthlem4  19268  bcthlem5  19269  minveclem3b  19317  minveclem3  19318  ivthlem2  19337  ovolgelb  19364  ovollb2lem  19372  ovolunlem1a  19380  ovolunlem1  19381  ovoliunlem1  19386  ovoliunlem2  19387  ovolscalem1  19397  ioombl1lem2  19441  ioombl1lem4  19443  uniioombllem1  19461  uniioombllem3  19465  uniioombllem4  19466  uniioombllem5  19467  opnmbllem  19481  volcn  19486  vitalilem4  19491  itg2mulclem  19626  itg2monolem3  19632  itg2cnlem2  19642  itg2cn  19643  itggt0  19721  dveflem  19851  dvferm1lem  19856  dvferm2lem  19858  lhop1lem  19885  lhop1  19886  lhop  19888  dvcnvrelem1  19889  dvcnvrelem2  19890  dvcnvre  19891  dvfsumrlim  19903  ftc1a  19909  ftc1lem4  19911  plyeq0lem  20117  aalioulem2  20238  aalioulem4  20240  aalioulem5  20241  aalioulem6  20242  aaliou  20243  aaliou2b  20246  aaliou3lem1  20247  aaliou3lem2  20248  aaliou3lem8  20250  aaliou3lem5  20252  aaliou3lem7  20254  aaliou3lem9  20255  ulmcn  20303  ulmdvlem1  20304  mtest  20308  itgulm  20312  psercn  20330  pserdvlem1  20331  pserdvlem2  20332  pserdv  20333  abelthlem7  20342  pilem2  20356  divlogrlim  20514  logcnlem3  20523  logcnlem4  20524  logccv  20542  divcxp  20566  cxplt  20573  cxple2  20576  cxpcn3lem  20619  cxpaddlelem  20623  cxpaddle  20624  loglesqr  20630  leibpi  20770  rlimcnp3  20794  cxplim  20798  rlimcxp  20800  cxp2limlem  20802  cxp2lim  20803  cxploglim  20804  cxploglim2  20805  divsqrsumlem  20806  jensenlem2  20814  logdifbnd  20820  emcllem4  20825  harmonicbnd4  20837  fsumharmonic  20838  ftalem1  20843  ftalem2  20844  ftalem3  20845  ftalem5  20847  basellem1  20851  basellem3  20853  basellem4  20854  basellem8  20858  chtwordi  20927  chpchtsum  20991  logfacrlim  20996  logexprlim  20997  bclbnd  21052  efexple  21053  bposlem1  21056  bposlem2  21057  bposlem6  21061  bposlem7  21062  chebbnd1lem3  21153  chebbnd1  21154  chtppilimlem1  21155  chtppilimlem2  21156  chpo1ubb  21163  rplogsumlem1  21166  rplogsumlem2  21167  dchrisum0lem1a  21168  rpvmasumlem  21169  dchrisumlem2  21172  dchrisumlem3  21173  dchrmusumlema  21175  dchrmusum2  21176  dchrvmasumlem1  21177  dchrvmasum2lem  21178  dchrvmasumlema  21182  dchrvmasumiflem1  21183  dchrisum0fno1  21193  dchrisum0lem1b  21197  dchrisum0lem1  21198  dchrisum0lem2  21200  dchrisum0lem3  21201  dchrisum0  21202  mulogsumlem  21213  logdivsum  21215  mulog2sumlem2  21217  vmalogdivsum2  21220  vmalogdivsum  21221  2vmadivsumlem  21222  log2sumbnd  21226  selberglem2  21228  selberg  21230  selberg2lem  21232  chpdifbndlem1  21235  chpdifbndlem2  21236  selberg3lem1  21239  selberg3  21241  selberg4lem1  21242  selberg4  21243  pntrsumbnd2  21249  selberg3r  21251  selberg4r  21252  selberg34r  21253  pntrlog2bndlem1  21259  pntrlog2bndlem2  21260  pntrlog2bndlem3  21261  pntrlog2bndlem5  21263  pntrlog2bndlem6a  21264  pntrlog2bndlem6  21265  pntrlog2bnd  21266  pntpbnd1a  21267  pntpbnd1  21268  pntpbnd2  21269  pntibndlem1  21271  pntibndlem2  21273  pntibndlem3  21274  pntibnd  21275  pntlemc  21277  pntlema  21278  pntlemb  21279  pntlemg  21280  pntlemh  21281  pntlemn  21282  pntlemq  21283  pntlemr  21284  pntlemj  21285  pntlemi  21286  pntlemf  21287  pntlemk  21288  pntlemo  21289  pntleme  21290  pntlem3  21291  pntlemp  21292  pntleml  21293  ostth2lem1  21300  ostth2lem3  21317  ostth2  21319  ostth3  21320  smcnlem  22181  blocnilem  22293  blocni  22294  ubthlem2  22361  minvecolem3  22366  minvecolem4  22370  minvecolem5  22371  nmcexi  23517  lnconi  23524  rpxdivcld  24168  sqsscirc1  24294  cnre2csqlem  24296  tpr2rico  24298  xrmulc1cn  24304  xrge0iifiso  24309  xrge0iifhom  24311  esumcst  24443  esumdivc  24461  dya2icoseg  24615  probmeasb  24676  zetacvg  24787  lgamgulmlem2  24802  lgamgulmlem5  24805  lgamucov  24810  regamcl  24833  relgamcl  24834  mblfinlem  26190  mblfinlem2  26191  itg2addnclem3  26204  itg2addnc  26205  itggt0cn  26223  ftc1cnnclem  26224  geomcau  26402  sstotbnd2  26420  isbnd3  26430  equivbnd  26436  prdsbnd2  26441  cntotbnd  26442  heibor1lem  26455  heiborlem6  26462  bfplem1  26468  bfplem2  26469  bfp  26470  rrndstprj2  26477  rrnequiv  26481  irrapxlem4  26825  irrapxlem5  26826  irrapx1  26828  pell1qrgaplem  26873  pell14qrgapw  26876  pellqrexplicit  26877  pellqrex  26879  pellfundge  26882  pellfundgt1  26883  rmspecfund  26909  rmxycomplete  26917  rpexpmord  26948  rmxypos  26949  fmul01lt1lem1  27628  fmul01lt1lem2  27629  stoweidlem1  27664  stoweidlem3  27666  stoweidlem5  27668  stoweidlem7  27670  stoweidlem11  27674  stoweidlem13  27676  stoweidlem14  27677  stoweidlem24  27687  stoweidlem25  27688  stoweidlem26  27689  stoweidlem34  27697  stoweidlem41  27704  stoweidlem42  27705  stoweidlem49  27712  stoweidlem51  27714  stoweidlem52  27715  stoweidlem59  27722  stoweidlem60  27723  stoweidlem62  27725  stoweid  27726  wallispilem5  27732  stirlinglem1  27737  stirlinglem4  27740  stirlinglem5  27741  stirlinglem6  27742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326  df-rp 10602
  Copyright terms: Public domain W3C validator