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

Theorem rpred 12958
Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rpred (𝜑𝐴 ∈ ℝ)

Proof of Theorem rpred
StepHypRef Expression
1 rpssre 12923 . 2 + ⊆ ℝ
2 rpred.1 . 2 (𝜑𝐴 ∈ ℝ+)
31, 2sselid 3943 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  +crp 12916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918  df-ss 3928  df-rp 12917
This theorem is referenced by:  rpxrd  12959  rpcnd  12960  rpregt0d  12964  rprege0d  12965  rprene0d  12966  rprecred  12969  ltmulgt11d  12993  ltmulgt12d  12994  gt0divd  12995  ge0divd  12996  lediv12ad  13017  prodge0rd  13023  xlemul1  13210  xov1plusxeqvd  13416  ltexp2a  14072  rpexpmord  14074  expcan  14075  ltexp2  14076  leexp2a  14078  expnlbnd2  14138  expmulnbnd  14139  01sqrexlem6  15133  cau3lem  15240  rlimcld2  15461  addcn2  15477  mulcn2  15479  reccn2  15480  o1rlimmul  15502  rlimno1  15539  caucvgrlem  15558  isumrpcl  15729  isumltss  15734  expcnv  15750  mertenslem1  15770  effsumlt  15994  recoshcl  16041  eirrlem  16087  rpnnen2lem11  16107  bitsmod  16317  prmreclem3  16791  prmreclem5  16793  4sqlem7  16817  ssblex  23784  metss2lem  23870  methaus  23879  met1stc  23880  met2ndci  23881  metustto  23912  metustexhalf  23915  nlmvscnlem2  24052  nlmvscnlem1  24053  nrginvrcnlem  24058  nmoi2  24097  nghmcn  24112  reperflem  24184  iccntr  24187  icccmplem2  24189  reconnlem2  24193  opnreen  24197  metdcnlem  24202  metnrmlem3  24227  addcnlem  24230  cnheibor  24321  cnllycmp  24322  lebnumlem3  24329  lebnumii  24332  nmoleub2lem  24480  nmoleub2lem3  24481  nmoleub2lem2  24482  nmoleub3  24485  nmhmcn  24486  ipcnlem2  24611  ipcnlem1  24612  lmnn  24630  iscfil3  24640  cfilfcls  24641  iscmet3lem1  24658  iscmet3lem2  24659  bcthlem4  24694  bcthlem5  24695  minveclem3b  24795  minveclem3  24796  ivthlem2  24819  ovolgelb  24847  ovollb2lem  24855  ovolunlem1a  24863  ovolunlem1  24864  ovoliunlem1  24869  ovoliunlem2  24870  ovolscalem1  24880  ioombl1lem2  24926  ioombl1lem4  24928  uniioombllem1  24948  uniioombllem3  24952  uniioombllem4  24953  uniioombllem5  24954  opnmbllem  24968  volcn  24973  vitalilem4  24978  itg2mulclem  25114  itg2monolem3  25120  itg2cnlem2  25130  itg2cn  25131  itggt0  25211  dveflem  25346  dvferm1lem  25351  dvferm2lem  25353  lhop1lem  25380  lhop1  25381  lhop  25383  dvcnvrelem1  25384  dvcnvrelem2  25385  dvcnvre  25386  dvfsumrlim  25398  ftc1a  25404  ftc1lem4  25406  plyeq0lem  25574  aalioulem2  25696  aalioulem4  25698  aalioulem5  25699  aalioulem6  25700  aaliou  25701  aaliou2b  25704  aaliou3lem1  25705  aaliou3lem2  25706  aaliou3lem8  25708  aaliou3lem5  25710  aaliou3lem7  25712  aaliou3lem9  25713  ulmcn  25761  ulmdvlem1  25762  mtest  25766  itgulm  25770  psercn  25788  pserdvlem1  25789  pserdvlem2  25790  pserdv  25791  abelthlem7  25800  pilem2  25814  divlogrlim  25993  logcnlem3  26002  logcnlem4  26003  logccv  26021  divcxp  26045  cxplt  26052  cxple2  26055  cxpcn3lem  26103  cxpaddlelem  26107  cxpaddle  26108  loglesqrt  26114  leibpi  26295  rlimcnp3  26320  cxplim  26324  rlimcxp  26326  cxp2limlem  26328  cxp2lim  26329  cxploglim  26330  cxploglim2  26331  divsqrtsumlem  26332  jensenlem2  26340  logdifbnd  26346  emcllem4  26351  harmonicbnd4  26363  fsumharmonic  26364  zetacvg  26367  lgamgulmlem2  26382  lgamgulmlem5  26385  lgamucov  26390  regamcl  26413  relgamcl  26414  ftalem1  26425  ftalem2  26426  ftalem3  26427  ftalem5  26429  basellem1  26433  basellem3  26435  basellem4  26436  basellem8  26440  chtwordi  26508  chpchtsum  26570  logfacrlim  26575  logexprlim  26576  bclbnd  26631  efexple  26632  bposlem1  26635  bposlem2  26636  bposlem6  26640  bposlem7  26641  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem1  26824  chtppilimlem2  26825  chpo1ubb  26832  rplogsumlem1  26835  rplogsumlem2  26836  dchrisum0lem1a  26837  rpvmasumlem  26838  dchrisumlem2  26841  dchrisumlem3  26842  dchrmusumlema  26844  dchrmusum2  26845  dchrvmasumlem1  26846  dchrvmasum2lem  26847  dchrvmasumlema  26851  dchrvmasumiflem1  26852  dchrisum0fno1  26862  dchrisum0lem1b  26866  dchrisum0lem1  26867  dchrisum0lem2  26869  dchrisum0lem3  26870  dchrisum0  26871  mulogsumlem  26882  logdivsum  26884  mulog2sumlem2  26886  vmalogdivsum2  26889  2vmadivsumlem  26891  log2sumbnd  26895  selberglem2  26897  selberg  26899  selberg2lem  26901  chpdifbndlem1  26904  chpdifbndlem2  26905  selberg3lem1  26908  selberg4lem1  26911  pntrsumbnd2  26918  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem5  26932  pntrlog2bndlem6a  26933  pntrlog2bndlem6  26934  pntrlog2bnd  26935  pntpbnd1a  26936  pntpbnd1  26937  pntpbnd2  26938  pntibndlem1  26940  pntibndlem2  26942  pntibndlem3  26943  pntibnd  26944  pntlemc  26946  pntlema  26947  pntlemb  26948  pntlemg  26949  pntlemh  26950  pntlemn  26951  pntlemq  26952  pntlemr  26953  pntlemj  26954  pntlemi  26955  pntlemf  26956  pntlemk  26957  pntlemo  26958  pntleme  26959  pntlem3  26960  pntlemp  26961  pntleml  26962  ostth2lem1  26969  ostth2lem3  26986  ostth2  26988  ostth3  26989  crctcshwlkn0lem5  28762  smcnlem  29642  blocnilem  29749  blocni  29750  ubthlem2  29816  minvecolem3  29821  minvecolem4  29825  minvecolem5  29826  nmcexi  30971  lnconi  30978  fsumub  31727  rpxdivcld  31793  sqsscirc1  32492  cnre2csqlem  32494  tpr2rico  32496  xrmulc1cn  32514  xrge0iifiso  32519  xrge0iifhom  32521  esumcst  32665  esumdivc  32685  dya2icoseg  32880  omssubaddlem  32902  omssubadd  32903  probmeasb  33033  sgnmulrp2  33146  signsply0  33166  logdivsqrle  33266  hgt750leme  33274  dnicn  34958  unblimceq0lem  34972  unbdqndv2lem1  34975  unbdqndv2lem2  34976  knoppndvlem18  34995  knoppndvlem21  34998  poimirlem29  36110  heicant  36116  opnmbllem0  36117  mblfinlem3  36120  itg2addnclem3  36134  itg2addnc  36135  itggt0cn  36151  ftc1cnnclem  36152  ftc1anclem6  36159  ftc1anclem7  36160  geomcau  36221  sstotbnd2  36236  isbnd3  36246  equivbnd  36252  prdsbnd2  36257  cntotbnd  36258  heibor1lem  36271  heiborlem6  36278  bfplem1  36284  bfplem2  36285  bfp  36286  rrndstprj2  36293  rrnequiv  36297  lcmineqlem21  40509  aks4d1p1p4  40531  aks4d1p1p7  40534  aks4d1p5  40540  aks4d1p6  40541  exp11nnd  40813  fltnlta  41004  irrapxlem4  41151  irrapxlem5  41152  irrapx1  41154  pell1qrgaplem  41199  pell14qrgapw  41202  pellqrexplicit  41203  pellqrex  41205  pellfundge  41208  pellfundgt1  41209  rmspecfund  41235  rmxycomplete  41244  rmxypos  41274  binomcxplemnotnn0  42643  suprltrp  43569  supxrge  43579  infrpge  43592  infleinflem1  43611  xralrple4  43614  recnnltrp  43618  rpgtrecnn  43621  cvgcaule  43734  fmul01lt1lem1  43832  fmul01lt1lem2  43833  ltmod  43886  lptre2pt  43888  addlimc  43896  0ellimcdiv  43897  limclner  43899  climleltrp  43924  climisp  43994  climxrrelem  43997  climxrre  43998  limsupgtlem  44025  liminfltlem  44052  cnrefiisplem  44077  climxlim2lem  44093  dvdivbd  44171  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  itgiccshift  44228  itgperiod  44229  stoweidlem1  44249  stoweidlem3  44251  stoweidlem5  44253  stoweidlem7  44255  stoweidlem11  44259  stoweidlem13  44261  stoweidlem14  44262  stoweidlem24  44272  stoweidlem25  44273  stoweidlem26  44274  stoweidlem34  44282  stoweidlem41  44289  stoweidlem42  44290  stoweidlem49  44297  stoweidlem51  44299  stoweidlem52  44300  stoweidlem59  44307  stoweidlem60  44308  stoweidlem62  44310  stoweid  44311  wallispilem5  44317  stirlinglem1  44322  stirlinglem4  44325  stirlinglem5  44326  stirlinglem6  44327  dirkercncflem1  44351  fourierdlem30  44385  fourierdlem39  44394  fourierdlem47  44401  fourierdlem73  44427  fourierdlem81  44435  fourierdlem87  44441  fourierdlem103  44457  fourierdlem104  44458  fourierdlem107  44461  rrndistlt  44538  qndenserrnbllem  44542  sge0ltfirp  44648  sge0rpcpnf  44669  sge0xaddlem1  44681  omeiunltfirp  44767  carageniuncllem2  44770  ovnsubaddlem1  44818  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  hoiqssbllem1  44870  hoiqssbllem2  44871  hoiqssbllem3  44872  hspmbllem2  44875  hspmbllem3  44876  ovolval5lem1  44900  ovolval5lem2  44901  iinhoiicc  44922  vonioolem1  44928  pimrecltpos  44956  smflimlem3  45021  smfmullem1  45039  smfmullem2  45040  smfmullem3  45041  modexp2m1d  45811  dignn0flhalflem1  46708  itsclc0yqsol  46857  amgmwlem  47256  amgmw2d  47258  young2d  47259
  Copyright terms: Public domain W3C validator