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

Theorem rpred 11015
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 10989 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3342 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   RRcr 9269   RR+crp 10979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323  df-ss 3330  df-rp 10980
This theorem is referenced by:  rpxrd  11016  rpcnd  11017  rpregt0d  11021  rprege0d  11022  rprene0d  11023  rprecred  11026  ltmulgt11d  11046  ltmulgt12d  11047  gt0divd  11048  ge0divd  11049  lediv12ad  11070  xlemul1  11241  xov1plusxeqvd  11418  ltexp2a  11899  expcan  11900  ltexp2  11901  leexp2a  11903  expnlbnd2  11979  expmulnbnd  11980  sqrlem6  12721  cau3lem  12826  rlimcld2  13040  addcn2  13055  mulcn2  13057  reccn2  13058  o1rlimmul  13080  rlimno1  13115  caucvgrlem  13134  isumrpcl  13289  isumltss  13294  expcnv  13309  mertenslem1  13327  effsumlt  13378  recoshcl  13425  eirrlem  13469  rpnnen2lem11  13490  bitsmod  13615  prmreclem3  13962  prmreclem5  13964  4sqlem7  13988  ssblex  19845  metss2lem  19928  methaus  19937  met1stc  19938  met2ndci  19939  metusttoOLD  19974  metustto  19975  metustexhalfOLD  19980  metustexhalf  19981  nlmvscnlem2  20108  nlmvscnlem1  20109  nrginvrcnlem  20113  nmoi2  20151  nghmcn  20166  reperflem  20237  iccntr  20240  icccmplem2  20242  reconnlem2  20246  opnreen  20250  metdcnlem  20255  metnrmlem3  20279  addcnlem  20282  cnheibor  20369  cnllycmp  20370  lebnumlem3  20377  lebnumii  20380  nmoleub2lem  20511  nmoleub2lem3  20512  nmoleub2lem2  20513  nmoleub3  20516  nmhmcn  20517  ipcnlem2  20598  ipcnlem1  20599  lmnn  20616  iscfil3  20626  cfilfcls  20627  iscmet3lem1  20644  iscmet3lem2  20645  bcthlem4  20680  bcthlem5  20681  minveclem3b  20757  minveclem3  20758  ivthlem2  20778  ovolgelb  20805  ovollb2lem  20813  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliunlem2  20828  ovolscalem1  20838  ioombl1lem2  20882  ioombl1lem4  20884  uniioombllem1  20903  uniioombllem3  20907  uniioombllem4  20908  uniioombllem5  20909  opnmbllem  20923  volcn  20928  vitalilem4  20933  itg2mulclem  21066  itg2monolem3  21072  itg2cnlem2  21082  itg2cn  21083  itggt0  21161  dveflem  21293  dvferm1lem  21298  dvferm2lem  21300  lhop1lem  21327  lhop1  21328  lhop  21330  dvcnvrelem1  21331  dvcnvrelem2  21332  dvcnvre  21333  dvfsumrlim  21345  ftc1a  21351  ftc1lem4  21353  plyeq0lem  21563  aalioulem2  21684  aalioulem4  21686  aalioulem5  21687  aalioulem6  21688  aaliou  21689  aaliou2b  21692  aaliou3lem1  21693  aaliou3lem2  21694  aaliou3lem8  21696  aaliou3lem5  21698  aaliou3lem7  21700  aaliou3lem9  21701  ulmcn  21749  ulmdvlem1  21750  mtest  21754  itgulm  21758  psercn  21776  pserdvlem1  21777  pserdvlem2  21778  pserdv  21779  abelthlem7  21788  pilem2  21802  divlogrlim  21965  logcnlem3  21974  logcnlem4  21975  logccv  21993  divcxp  22017  cxplt  22024  cxple2  22027  cxpcn3lem  22070  cxpaddlelem  22074  cxpaddle  22075  loglesqr  22081  leibpi  22222  rlimcnp3  22246  cxplim  22250  rlimcxp  22252  cxp2limlem  22254  cxp2lim  22255  cxploglim  22256  cxploglim2  22257  divsqrsumlem  22258  jensenlem2  22266  logdifbnd  22272  emcllem4  22277  harmonicbnd4  22289  fsumharmonic  22290  ftalem1  22295  ftalem2  22296  ftalem3  22297  ftalem5  22299  basellem1  22303  basellem3  22305  basellem4  22306  basellem8  22310  chtwordi  22379  chpchtsum  22443  logfacrlim  22448  logexprlim  22449  bclbnd  22504  efexple  22505  bposlem1  22508  bposlem2  22509  bposlem6  22513  bposlem7  22514  chebbnd1lem3  22605  chebbnd1  22606  chtppilimlem1  22607  chtppilimlem2  22608  chpo1ubb  22615  rplogsumlem1  22618  rplogsumlem2  22619  dchrisum0lem1a  22620  rpvmasumlem  22621  dchrisumlem2  22624  dchrisumlem3  22625  dchrmusumlema  22627  dchrmusum2  22628  dchrvmasumlem1  22629  dchrvmasum2lem  22630  dchrvmasumlema  22634  dchrvmasumiflem1  22635  dchrisum0fno1  22645  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2  22652  dchrisum0lem3  22653  dchrisum0  22654  mulogsumlem  22665  logdivsum  22667  mulog2sumlem2  22669  vmalogdivsum2  22672  2vmadivsumlem  22674  log2sumbnd  22678  selberglem2  22680  selberg  22682  selberg2lem  22684  chpdifbndlem1  22687  chpdifbndlem2  22688  selberg3lem1  22691  selberg4lem1  22694  pntrsumbnd2  22701  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem5  22715  pntrlog2bndlem6a  22716  pntrlog2bndlem6  22717  pntrlog2bnd  22718  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntibndlem1  22723  pntibndlem2  22725  pntibndlem3  22726  pntibnd  22727  pntlemc  22729  pntlema  22730  pntlemb  22731  pntlemg  22732  pntlemh  22733  pntlemn  22734  pntlemq  22735  pntlemr  22736  pntlemj  22737  pntlemi  22738  pntlemf  22739  pntlemk  22740  pntlemo  22741  pntleme  22742  pntlem3  22743  pntlemp  22744  pntleml  22745  ostth2lem1  22752  ostth2lem3  22769  ostth2  22771  ostth3  22772  smcnlem  23915  blocnilem  24027  blocni  24028  ubthlem2  24095  minvecolem3  24100  minvecolem4  24104  minvecolem5  24105  nmcexi  25253  lnconi  25260  rpxdivcld  25932  sqsscirc1  26192  cnre2csqlem  26194  tpr2rico  26196  xrmulc1cn  26214  xrge0iifiso  26219  xrge0iifhom  26221  esumcst  26368  esumdivc  26386  dya2icoseg  26546  probmeasb  26661  sgnmulrp2  26774  signshf  26837  zetacvg  26849  lgamgulmlem2  26864  lgamgulmlem5  26867  lgamucov  26872  regamcl  26895  relgamcl  26896  heicant  28270  opnmbllem0  28271  mblfinlem3  28274  itg2addnclem3  28289  itg2addnc  28290  itggt0cn  28308  ftc1cnnclem  28309  ftc1anclem6  28316  ftc1anclem7  28317  geomcau  28499  sstotbnd2  28517  isbnd3  28527  equivbnd  28533  prdsbnd2  28538  cntotbnd  28539  heibor1lem  28552  heiborlem6  28559  bfplem1  28565  bfplem2  28566  bfp  28567  rrndstprj2  28574  rrnequiv  28578  irrapxlem4  29011  irrapxlem5  29012  irrapx1  29014  pell1qrgaplem  29059  pell14qrgapw  29062  pellqrexplicit  29063  pellqrex  29065  pellfundge  29068  pellfundgt1  29069  rmspecfund  29095  rmxycomplete  29103  rpexpmord  29134  rmxypos  29135  fmul01lt1lem1  29610  fmul01lt1lem2  29611  stoweidlem1  29642  stoweidlem3  29644  stoweidlem5  29646  stoweidlem7  29648  stoweidlem11  29652  stoweidlem13  29654  stoweidlem14  29655  stoweidlem24  29665  stoweidlem25  29666  stoweidlem26  29667  stoweidlem34  29675  stoweidlem41  29682  stoweidlem42  29683  stoweidlem49  29690  stoweidlem51  29692  stoweidlem52  29693  stoweidlem59  29700  stoweidlem60  29701  stoweidlem62  29703  stoweid  29704  wallispilem5  29710  stirlinglem1  29715  stirlinglem4  29718  stirlinglem5  29719  stirlinglem6  29720
  Copyright terms: Public domain W3C validator