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

Theorem rpred 11019
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 10993 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3349 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-in 3330  df-ss 3337  df-rp 10984
This theorem is referenced by:  rpxrd  11020  rpcnd  11021  rpregt0d  11025  rprege0d  11026  rprene0d  11027  rprecred  11030  ltmulgt11d  11050  ltmulgt12d  11051  gt0divd  11052  ge0divd  11053  lediv12ad  11074  xlemul1  11245  xov1plusxeqvd  11423  ltexp2a  11907  expcan  11908  ltexp2  11909  leexp2a  11911  expnlbnd2  11987  expmulnbnd  11988  sqrlem6  12729  cau3lem  12834  rlimcld2  13048  addcn2  13063  mulcn2  13065  reccn2  13066  o1rlimmul  13088  rlimno1  13123  caucvgrlem  13142  isumrpcl  13298  isumltss  13303  expcnv  13318  mertenslem1  13336  effsumlt  13387  recoshcl  13434  eirrlem  13478  rpnnen2lem11  13499  bitsmod  13624  prmreclem3  13971  prmreclem5  13973  4sqlem7  13997  ssblex  19978  metss2lem  20061  methaus  20070  met1stc  20071  met2ndci  20072  metusttoOLD  20107  metustto  20108  metustexhalfOLD  20113  metustexhalf  20114  nlmvscnlem2  20241  nlmvscnlem1  20242  nrginvrcnlem  20246  nmoi2  20284  nghmcn  20299  reperflem  20370  iccntr  20373  icccmplem2  20375  reconnlem2  20379  opnreen  20383  metdcnlem  20388  metnrmlem3  20412  addcnlem  20415  cnheibor  20502  cnllycmp  20503  lebnumlem3  20510  lebnumii  20513  nmoleub2lem  20644  nmoleub2lem3  20645  nmoleub2lem2  20646  nmoleub3  20649  nmhmcn  20650  ipcnlem2  20731  ipcnlem1  20732  lmnn  20749  iscfil3  20759  cfilfcls  20760  iscmet3lem1  20777  iscmet3lem2  20778  bcthlem4  20813  bcthlem5  20814  minveclem3b  20890  minveclem3  20891  ivthlem2  20911  ovolgelb  20938  ovollb2lem  20946  ovolunlem1a  20954  ovolunlem1  20955  ovoliunlem1  20960  ovoliunlem2  20961  ovolscalem1  20971  ioombl1lem2  21015  ioombl1lem4  21017  uniioombllem1  21036  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  opnmbllem  21056  volcn  21061  vitalilem4  21066  itg2mulclem  21199  itg2monolem3  21205  itg2cnlem2  21215  itg2cn  21216  itggt0  21294  dveflem  21426  dvferm1lem  21431  dvferm2lem  21433  lhop1lem  21460  lhop1  21461  lhop  21463  dvcnvrelem1  21464  dvcnvrelem2  21465  dvcnvre  21466  dvfsumrlim  21478  ftc1a  21484  ftc1lem4  21486  plyeq0lem  21653  aalioulem2  21774  aalioulem4  21776  aalioulem5  21777  aalioulem6  21778  aaliou  21779  aaliou2b  21782  aaliou3lem1  21783  aaliou3lem2  21784  aaliou3lem8  21786  aaliou3lem5  21788  aaliou3lem7  21790  aaliou3lem9  21791  ulmcn  21839  ulmdvlem1  21840  mtest  21844  itgulm  21848  psercn  21866  pserdvlem1  21867  pserdvlem2  21868  pserdv  21869  abelthlem7  21878  pilem2  21892  divlogrlim  22055  logcnlem3  22064  logcnlem4  22065  logccv  22083  divcxp  22107  cxplt  22114  cxple2  22117  cxpcn3lem  22160  cxpaddlelem  22164  cxpaddle  22165  loglesqr  22171  leibpi  22312  rlimcnp3  22336  cxplim  22340  rlimcxp  22342  cxp2limlem  22344  cxp2lim  22345  cxploglim  22346  cxploglim2  22347  divsqrsumlem  22348  jensenlem2  22356  logdifbnd  22362  emcllem4  22367  harmonicbnd4  22379  fsumharmonic  22380  ftalem1  22385  ftalem2  22386  ftalem3  22387  ftalem5  22389  basellem1  22393  basellem3  22395  basellem4  22396  basellem8  22400  chtwordi  22469  chpchtsum  22533  logfacrlim  22538  logexprlim  22539  bclbnd  22594  efexple  22595  bposlem1  22598  bposlem2  22599  bposlem6  22603  bposlem7  22604  chebbnd1lem3  22695  chebbnd1  22696  chtppilimlem1  22697  chtppilimlem2  22698  chpo1ubb  22705  rplogsumlem1  22708  rplogsumlem2  22709  dchrisum0lem1a  22710  rpvmasumlem  22711  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusumlema  22717  dchrmusum2  22718  dchrvmasumlem1  22719  dchrvmasum2lem  22720  dchrvmasumlema  22724  dchrvmasumiflem1  22725  dchrisum0fno1  22735  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrisum0  22744  mulogsumlem  22755  logdivsum  22757  mulog2sumlem2  22759  vmalogdivsum2  22762  2vmadivsumlem  22764  log2sumbnd  22768  selberglem2  22770  selberg  22772  selberg2lem  22774  chpdifbndlem1  22777  chpdifbndlem2  22778  selberg3lem1  22781  selberg4lem1  22784  pntrsumbnd2  22791  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem5  22805  pntrlog2bndlem6a  22806  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem1  22813  pntibndlem2  22815  pntibndlem3  22816  pntibnd  22817  pntlemc  22819  pntlema  22820  pntlemb  22821  pntlemg  22822  pntlemh  22823  pntlemn  22824  pntlemq  22825  pntlemr  22826  pntlemj  22827  pntlemi  22828  pntlemf  22829  pntlemk  22830  pntlemo  22831  pntleme  22832  pntlem3  22833  pntlemp  22834  pntleml  22835  ostth2lem1  22842  ostth2lem3  22859  ostth2  22861  ostth3  22862  smcnlem  24043  blocnilem  24155  blocni  24156  ubthlem2  24223  minvecolem3  24228  minvecolem4  24232  minvecolem5  24233  nmcexi  25381  lnconi  25388  rpxdivcld  26060  sqsscirc1  26290  cnre2csqlem  26292  tpr2rico  26294  xrmulc1cn  26312  xrge0iifiso  26317  xrge0iifhom  26319  esumcst  26466  esumdivc  26484  dya2icoseg  26644  probmeasb  26765  sgnmulrp2  26878  signshf  26941  zetacvg  26953  lgamgulmlem2  26968  lgamgulmlem5  26971  lgamucov  26976  regamcl  26999  relgamcl  27000  heicant  28379  opnmbllem0  28380  mblfinlem3  28383  itg2addnclem3  28398  itg2addnc  28399  itggt0cn  28417  ftc1cnnclem  28418  ftc1anclem6  28425  ftc1anclem7  28426  geomcau  28608  sstotbnd2  28626  isbnd3  28636  equivbnd  28642  prdsbnd2  28647  cntotbnd  28648  heibor1lem  28661  heiborlem6  28668  bfplem1  28674  bfplem2  28675  bfp  28676  rrndstprj2  28683  rrnequiv  28687  irrapxlem4  29119  irrapxlem5  29120  irrapx1  29122  pell1qrgaplem  29167  pell14qrgapw  29170  pellqrexplicit  29171  pellqrex  29173  pellfundge  29176  pellfundgt1  29177  rmspecfund  29203  rmxycomplete  29211  rpexpmord  29242  rmxypos  29243  fmul01lt1lem1  29718  fmul01lt1lem2  29719  stoweidlem1  29749  stoweidlem3  29751  stoweidlem5  29753  stoweidlem7  29755  stoweidlem11  29759  stoweidlem13  29761  stoweidlem14  29762  stoweidlem24  29772  stoweidlem25  29773  stoweidlem26  29774  stoweidlem34  29782  stoweidlem41  29789  stoweidlem42  29790  stoweidlem49  29797  stoweidlem51  29799  stoweidlem52  29800  stoweidlem59  29807  stoweidlem60  29808  stoweidlem62  29810  stoweid  29811  wallispilem5  29817  stirlinglem1  29822  stirlinglem4  29825  stirlinglem5  29826  stirlinglem6  29827
  Copyright terms: Public domain W3C validator