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

Theorem rpred 11343
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 11314 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3463 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1869   RRcr 9540   RR+crp 11304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rab 2785  df-in 3444  df-ss 3451  df-rp 11305
This theorem is referenced by:  rpxrd  11344  rpcnd  11345  rpregt0d  11349  rprege0d  11350  rprene0d  11351  rprecred  11354  ltmulgt11d  11375  ltmulgt12d  11376  gt0divd  11377  ge0divd  11378  lediv12ad  11399  xlemul1  11578  xov1plusxeqvd  11780  ltexp2a  12325  expcan  12326  ltexp2  12327  leexp2a  12329  expnlbnd2  12404  expmulnbnd  12405  sqrlem6  13305  cau3lem  13411  rlimcld2  13635  addcn2  13650  mulcn2  13652  reccn2  13653  o1rlimmul  13675  rlimno1  13710  caucvgrlem  13729  caucvgrlemOLD  13730  isumrpcl  13894  isumltss  13899  expcnv  13915  mertenslem1  13933  effsumlt  14158  recoshcl  14205  eirrlem  14249  rpnnen2lem11  14270  bitsmod  14403  prmreclem3  14855  prmreclem5  14857  4sqlem7  14881  ssblex  21435  metss2lem  21518  methaus  21527  met1stc  21528  met2ndci  21529  metustto  21560  metustexhalf  21563  nlmvscnlem2  21680  nlmvscnlem1  21681  nrginvrcnlem  21685  nmoi2  21727  nmoi2OLD  21743  nghmcn  21758  reperflem  21828  iccntr  21831  icccmplem2  21833  reconnlem2  21837  opnreen  21841  metdcnlem  21846  metnrmlem3  21870  metnrmlem3OLD  21885  addcnlem  21888  cnheibor  21975  cnllycmp  21976  lebnumlem3  21983  lebnumlem3OLD  21986  lebnumii  21989  nmoleub2lem  22120  nmoleub2lem3  22121  nmoleub2lem2  22122  nmoleub3  22125  nmhmcn  22126  ipcnlem2  22207  ipcnlem1  22208  lmnn  22225  iscfil3  22235  cfilfcls  22236  iscmet3lem1  22253  iscmet3lem2  22254  bcthlem4  22287  bcthlem5  22288  minveclem3b  22362  minveclem3  22363  minveclem3bOLD  22374  minveclem3OLD  22375  ivthlem2  22395  ovolgelb  22425  ovollb2lem  22433  ovolunlem1a  22441  ovolunlem1  22442  ovoliunlem1  22447  ovoliunlem2  22448  ovolscalem1  22458  ioombl1lem2  22504  ioombl1lem4  22506  uniioombllem1  22530  uniioombllem3  22535  uniioombllem4  22536  uniioombllem5  22537  opnmbllem  22551  volcn  22556  vitalilem4  22561  itg2mulclem  22696  itg2monolem3  22702  itg2cnlem2  22712  itg2cn  22713  itggt0  22791  dveflem  22923  dvferm1lem  22928  dvferm2lem  22930  lhop1lem  22957  lhop1  22958  lhop  22960  dvcnvrelem1  22961  dvcnvrelem2  22962  dvcnvre  22963  dvfsumrlim  22975  ftc1a  22981  ftc1lem4  22983  plyeq0lem  23156  aalioulem2  23281  aalioulem4  23283  aalioulem5  23284  aalioulem6  23285  aaliou  23286  aaliou2b  23289  aaliou3lem1  23290  aaliou3lem2  23291  aaliou3lem8  23293  aaliou3lem5  23295  aaliou3lem7  23297  aaliou3lem9  23298  ulmcn  23346  ulmdvlem1  23347  mtest  23351  itgulm  23355  psercn  23373  pserdvlem1  23374  pserdvlem2  23375  pserdv  23376  abelthlem7  23385  pilem2  23399  pilem2OLD  23400  divlogrlim  23572  logcnlem3  23581  logcnlem4  23582  logccv  23600  divcxp  23624  cxplt  23631  cxple2  23634  cxpcn3lem  23679  cxpaddlelem  23683  cxpaddle  23684  loglesqrt  23690  leibpi  23860  rlimcnp3  23885  cxplim  23889  rlimcxp  23891  cxp2limlem  23893  cxp2lim  23894  cxploglim  23895  cxploglim2  23896  divsqrtsumlem  23897  jensenlem2  23905  logdifbnd  23911  emcllem4  23916  harmonicbnd4  23928  fsumharmonic  23929  zetacvg  23932  lgamgulmlem2  23947  lgamgulmlem5  23950  lgamucov  23955  regamcl  23978  relgamcl  23979  ftalem1  23989  ftalem2  23990  ftalem3  23991  ftalem5  23993  ftalem5OLD  23995  basellem1  23999  basellem3  24001  basellem4  24002  basellem8  24006  chtwordi  24075  chpchtsum  24139  logfacrlim  24144  logexprlim  24145  bclbnd  24200  efexple  24201  bposlem1  24204  bposlem2  24205  bposlem6  24209  bposlem7  24210  chebbnd1lem3  24301  chebbnd1  24302  chtppilimlem1  24303  chtppilimlem2  24304  chpo1ubb  24311  rplogsumlem1  24314  rplogsumlem2  24315  dchrisum0lem1a  24316  rpvmasumlem  24317  dchrisumlem2  24320  dchrisumlem3  24321  dchrmusumlema  24323  dchrmusum2  24324  dchrvmasumlem1  24325  dchrvmasum2lem  24326  dchrvmasumlema  24330  dchrvmasumiflem1  24331  dchrisum0fno1  24341  dchrisum0lem1b  24345  dchrisum0lem1  24346  dchrisum0lem2  24348  dchrisum0lem3  24349  dchrisum0  24350  mulogsumlem  24361  logdivsum  24363  mulog2sumlem2  24365  vmalogdivsum2  24368  2vmadivsumlem  24370  log2sumbnd  24374  selberglem2  24376  selberg  24378  selberg2lem  24380  chpdifbndlem1  24383  chpdifbndlem2  24384  selberg3lem1  24387  selberg4lem1  24390  pntrsumbnd2  24397  pntrlog2bndlem2  24408  pntrlog2bndlem3  24409  pntrlog2bndlem5  24411  pntrlog2bndlem6a  24412  pntrlog2bndlem6  24413  pntrlog2bnd  24414  pntpbnd1a  24415  pntpbnd1  24416  pntpbnd2  24417  pntibndlem1  24419  pntibndlem2  24421  pntibndlem3  24422  pntibnd  24423  pntlemc  24425  pntlema  24426  pntlemb  24427  pntlemg  24428  pntlemh  24429  pntlemn  24430  pntlemq  24431  pntlemr  24432  pntlemj  24433  pntlemi  24434  pntlemf  24435  pntlemk  24436  pntlemo  24437  pntleme  24438  pntlem3  24439  pntlemp  24440  pntleml  24441  ostth2lem1  24448  ostth2lem3  24465  ostth2  24467  ostth3  24468  smcnlem  26325  blocnilem  26437  blocni  26438  ubthlem2  26505  minvecolem3  26510  minvecolem4  26514  minvecolem5  26515  minvecolem3OLD  26520  minvecolem4OLD  26524  minvecolem5OLD  26525  nmcexi  27671  lnconi  27678  rpxdivcld  28404  sqsscirc1  28716  cnre2csqlem  28718  tpr2rico  28720  xrmulc1cn  28738  xrge0iifiso  28743  xrge0iifhom  28745  esumcst  28886  esumdivc  28906  dya2icoseg  29101  omssubaddlem  29129  omssubadd  29130  omssubaddlemOLD  29133  omssubaddOLD  29134  probmeasb  29265  sgnmulrp2  29416  signsply0  29442  signshf  29479  poimirlem29  31889  heicant  31895  opnmbllem0  31896  mblfinlem3  31899  itg2addnclem3  31915  itg2addnc  31916  itggt0cn  31934  ftc1cnnclem  31935  ftc1anclem6  31942  ftc1anclem7  31943  geomcau  32008  sstotbnd2  32026  isbnd3  32036  equivbnd  32042  prdsbnd2  32047  cntotbnd  32048  heibor1lem  32061  heiborlem6  32068  bfplem1  32074  bfplem2  32075  bfp  32076  rrndstprj2  32083  rrnequiv  32087  irrapxlem4  35595  irrapxlem5  35596  irrapx1  35598  pell1qrgaplem  35645  pell14qrgapw  35648  pellqrexplicit  35649  pellqrex  35652  pellfundge  35656  pellfundgt1  35657  rmspecfund  35683  rmxycomplete  35691  rpexpmord  35722  rmxypos  35723  binomcxplemnotnn0  36569  suprltrp  37399  supxrge  37409  infrpge  37422  fmul01lt1lem1  37488  fmul01lt1lem2  37489  ltmod  37544  lptre2pt  37546  addlimc  37555  0ellimcdiv  37556  limclner  37558  dvdivbd  37621  ioodvbdlimc1lem2  37630  ioodvbdlimc1lem2OLD  37632  ioodvbdlimc2lem  37634  ioodvbdlimc2lemOLD  37635  itgiccshift  37683  itgperiod  37684  stoweidlem1  37687  stoweidlem3  37689  stoweidlem5  37691  stoweidlem7  37693  stoweidlem11  37697  stoweidlem13  37699  stoweidlem14  37700  stoweidlem24  37710  stoweidlem25  37711  stoweidlem26  37712  stoweidlem34  37721  stoweidlem41  37728  stoweidlem42  37729  stoweidlem49  37736  stoweidlem51  37738  stoweidlem52  37739  stoweidlem59  37746  stoweidlem60  37747  stoweidlem62  37749  stoweidlem62OLD  37750  stoweid  37751  wallispilem5  37757  stirlinglem1  37762  stirlinglem4  37765  stirlinglem5  37766  stirlinglem6  37767  dirkercncflem1  37791  fourierdlem30  37825  fourierdlem39  37835  fourierdlem47  37843  fourierdlem73  37869  fourierdlem81  37877  fourierdlem87  37883  fourierdlem103  37899  fourierdlem104  37900  fourierdlem107  37903  sge0ltfirp  38036  sge0rpcpnf  38057  sge0xaddlem1  38069  omeiunltfirp  38125  carageniuncllem2  38128  ovnsubaddlem1  38173  modexp2m1d  38630  dignn0flhalflem1  39732
  Copyright terms: Public domain W3C validator