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

Theorem rpred 11341
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 11312 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3430 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   RRcr 9538   RR+crp 11302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-in 3411  df-ss 3418  df-rp 11303
This theorem is referenced by:  rpxrd  11342  rpcnd  11343  rpregt0d  11347  rprege0d  11348  rprene0d  11349  rprecred  11352  ltmulgt11d  11373  ltmulgt12d  11374  gt0divd  11375  ge0divd  11376  lediv12ad  11397  xlemul1  11576  xov1plusxeqvd  11778  ltexp2a  12324  expcan  12325  ltexp2  12326  leexp2a  12328  expnlbnd2  12403  expmulnbnd  12404  sqrlem6  13311  cau3lem  13417  rlimcld2  13642  addcn2  13657  mulcn2  13659  reccn2  13660  o1rlimmul  13682  rlimno1  13717  caucvgrlem  13736  caucvgrlemOLD  13737  isumrpcl  13901  isumltss  13906  expcnv  13922  mertenslem1  13940  effsumlt  14165  recoshcl  14212  eirrlem  14256  rpnnen2lem11  14277  bitsmod  14410  prmreclem3  14862  prmreclem5  14864  4sqlem7  14888  ssblex  21443  metss2lem  21526  methaus  21535  met1stc  21536  met2ndci  21537  metustto  21568  metustexhalf  21571  nlmvscnlem2  21688  nlmvscnlem1  21689  nrginvrcnlem  21693  nmoi2  21735  nmoi2OLD  21751  nghmcn  21766  reperflem  21836  iccntr  21839  icccmplem2  21841  reconnlem2  21845  opnreen  21849  metdcnlem  21854  metnrmlem3  21878  metnrmlem3OLD  21893  addcnlem  21896  cnheibor  21983  cnllycmp  21984  lebnumlem3  21991  lebnumlem3OLD  21994  lebnumii  21997  nmoleub2lem  22128  nmoleub2lem3  22129  nmoleub2lem2  22130  nmoleub3  22133  nmhmcn  22134  ipcnlem2  22215  ipcnlem1  22216  lmnn  22233  iscfil3  22243  cfilfcls  22244  iscmet3lem1  22261  iscmet3lem2  22262  bcthlem4  22295  bcthlem5  22296  minveclem3b  22370  minveclem3  22371  minveclem3bOLD  22382  minveclem3OLD  22383  ivthlem2  22403  ovolgelb  22433  ovollb2lem  22441  ovolunlem1a  22449  ovolunlem1  22450  ovoliunlem1  22455  ovoliunlem2  22456  ovolscalem1  22466  ioombl1lem2  22512  ioombl1lem4  22514  uniioombllem1  22538  uniioombllem3  22543  uniioombllem4  22544  uniioombllem5  22545  opnmbllem  22559  volcn  22564  vitalilem4  22569  itg2mulclem  22704  itg2monolem3  22710  itg2cnlem2  22720  itg2cn  22721  itggt0  22799  dveflem  22931  dvferm1lem  22936  dvferm2lem  22938  lhop1lem  22965  lhop1  22966  lhop  22968  dvcnvrelem1  22969  dvcnvrelem2  22970  dvcnvre  22971  dvfsumrlim  22983  ftc1a  22989  ftc1lem4  22991  plyeq0lem  23164  aalioulem2  23289  aalioulem4  23291  aalioulem5  23292  aalioulem6  23293  aaliou  23294  aaliou2b  23297  aaliou3lem1  23298  aaliou3lem2  23299  aaliou3lem8  23301  aaliou3lem5  23303  aaliou3lem7  23305  aaliou3lem9  23306  ulmcn  23354  ulmdvlem1  23355  mtest  23359  itgulm  23363  psercn  23381  pserdvlem1  23382  pserdvlem2  23383  pserdv  23384  abelthlem7  23393  pilem2  23407  pilem2OLD  23408  divlogrlim  23580  logcnlem3  23589  logcnlem4  23590  logccv  23608  divcxp  23632  cxplt  23639  cxple2  23642  cxpcn3lem  23687  cxpaddlelem  23691  cxpaddle  23692  loglesqrt  23698  leibpi  23868  rlimcnp3  23893  cxplim  23897  rlimcxp  23899  cxp2limlem  23901  cxp2lim  23902  cxploglim  23903  cxploglim2  23904  divsqrtsumlem  23905  jensenlem2  23913  logdifbnd  23919  emcllem4  23924  harmonicbnd4  23936  fsumharmonic  23937  zetacvg  23940  lgamgulmlem2  23955  lgamgulmlem5  23958  lgamucov  23963  regamcl  23986  relgamcl  23987  ftalem1  23997  ftalem2  23998  ftalem3  23999  ftalem5  24001  ftalem5OLD  24003  basellem1  24007  basellem3  24009  basellem4  24010  basellem8  24014  chtwordi  24083  chpchtsum  24147  logfacrlim  24152  logexprlim  24153  bclbnd  24208  efexple  24209  bposlem1  24212  bposlem2  24213  bposlem6  24217  bposlem7  24218  chebbnd1lem3  24309  chebbnd1  24310  chtppilimlem1  24311  chtppilimlem2  24312  chpo1ubb  24319  rplogsumlem1  24322  rplogsumlem2  24323  dchrisum0lem1a  24324  rpvmasumlem  24325  dchrisumlem2  24328  dchrisumlem3  24329  dchrmusumlema  24331  dchrmusum2  24332  dchrvmasumlem1  24333  dchrvmasum2lem  24334  dchrvmasumlema  24338  dchrvmasumiflem1  24339  dchrisum0fno1  24349  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2  24356  dchrisum0lem3  24357  dchrisum0  24358  mulogsumlem  24369  logdivsum  24371  mulog2sumlem2  24373  vmalogdivsum2  24376  2vmadivsumlem  24378  log2sumbnd  24382  selberglem2  24384  selberg  24386  selberg2lem  24388  chpdifbndlem1  24391  chpdifbndlem2  24392  selberg3lem1  24395  selberg4lem1  24398  pntrsumbnd2  24405  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem5  24419  pntrlog2bndlem6a  24420  pntrlog2bndlem6  24421  pntrlog2bnd  24422  pntpbnd1a  24423  pntpbnd1  24424  pntpbnd2  24425  pntibndlem1  24427  pntibndlem2  24429  pntibndlem3  24430  pntibnd  24431  pntlemc  24433  pntlema  24434  pntlemb  24435  pntlemg  24436  pntlemh  24437  pntlemn  24438  pntlemq  24439  pntlemr  24440  pntlemj  24441  pntlemi  24442  pntlemf  24443  pntlemk  24444  pntlemo  24445  pntleme  24446  pntlem3  24447  pntlemp  24448  pntleml  24449  ostth2lem1  24456  ostth2lem3  24473  ostth2  24475  ostth3  24476  smcnlem  26333  blocnilem  26445  blocni  26446  ubthlem2  26513  minvecolem3  26518  minvecolem4  26522  minvecolem5  26523  minvecolem3OLD  26528  minvecolem4OLD  26532  minvecolem5OLD  26533  nmcexi  27679  lnconi  27686  rpxdivcld  28403  sqsscirc1  28714  cnre2csqlem  28716  tpr2rico  28718  xrmulc1cn  28736  xrge0iifiso  28741  xrge0iifhom  28743  esumcst  28884  esumdivc  28904  dya2icoseg  29099  omssubaddlem  29127  omssubadd  29128  omssubaddlemOLD  29131  omssubaddOLD  29132  probmeasb  29263  sgnmulrp2  29414  signsply0  29440  signshf  29477  poimirlem29  31969  heicant  31975  opnmbllem0  31976  mblfinlem3  31979  itg2addnclem3  31995  itg2addnc  31996  itggt0cn  32014  ftc1cnnclem  32015  ftc1anclem6  32022  ftc1anclem7  32023  geomcau  32088  sstotbnd2  32106  isbnd3  32116  equivbnd  32122  prdsbnd2  32127  cntotbnd  32128  heibor1lem  32141  heiborlem6  32148  bfplem1  32154  bfplem2  32155  bfp  32156  rrndstprj2  32163  rrnequiv  32167  irrapxlem4  35669  irrapxlem5  35670  irrapx1  35672  pell1qrgaplem  35719  pell14qrgapw  35722  pellqrexplicit  35723  pellqrex  35726  pellfundge  35730  pellfundgt1  35731  rmspecfund  35757  rmxycomplete  35765  rpexpmord  35796  rmxypos  35797  binomcxplemnotnn0  36705  suprltrp  37551  supxrge  37561  infrpge  37574  fmul01lt1lem1  37662  fmul01lt1lem2  37663  ltmod  37718  lptre2pt  37720  addlimc  37729  0ellimcdiv  37730  limclner  37732  dvdivbd  37795  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  itgiccshift  37857  itgperiod  37858  stoweidlem1  37861  stoweidlem3  37863  stoweidlem5  37865  stoweidlem7  37867  stoweidlem11  37871  stoweidlem13  37873  stoweidlem14  37874  stoweidlem24  37884  stoweidlem25  37885  stoweidlem26  37886  stoweidlem34  37895  stoweidlem41  37902  stoweidlem42  37903  stoweidlem49  37910  stoweidlem51  37912  stoweidlem52  37913  stoweidlem59  37920  stoweidlem60  37921  stoweidlem62  37923  stoweidlem62OLD  37924  stoweid  37925  wallispilem5  37931  stirlinglem1  37936  stirlinglem4  37939  stirlinglem5  37940  stirlinglem6  37941  dirkercncflem1  37965  fourierdlem30  37999  fourierdlem39  38009  fourierdlem47  38017  fourierdlem73  38043  fourierdlem81  38051  fourierdlem87  38057  fourierdlem103  38073  fourierdlem104  38074  fourierdlem107  38077  rrndistlt  38159  qndenserrnbllem  38163  sge0ltfirp  38242  sge0rpcpnf  38263  sge0xaddlem1  38275  omeiunltfirp  38340  carageniuncllem2  38343  ovnsubaddlem1  38392  hoidmvlelem1  38417  hoidmvlelem2  38418  hoidmvlelem3  38419  hoidmvlelem4  38420  hoiqssbllem1  38444  hoiqssbllem2  38445  hoiqssbllem3  38446  hspmbllem2  38449  hspmbllem3  38450  modexp2m1d  38912  dignn0flhalflem1  40479
  Copyright terms: Public domain W3C validator