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

Theorem rpred 12419
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 12384 . 2 + ⊆ ℝ
2 rpred.1 . 2 (𝜑𝐴 ∈ ℝ+)
31, 2sseldi 3962 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cr 10524  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940  df-ss 3949  df-rp 12378
This theorem is referenced by:  rpxrd  12420  rpcnd  12421  rpregt0d  12425  rprege0d  12426  rprene0d  12427  rprecred  12430  ltmulgt11d  12454  ltmulgt12d  12455  gt0divd  12456  ge0divd  12457  lediv12ad  12478  prodge0rd  12484  xlemul1  12671  xov1plusxeqvd  12872  ltexp2a  13518  rpexpmord  13520  expcan  13521  ltexp2  13522  leexp2a  13524  expnlbnd2  13583  expmulnbnd  13584  sqrlem6  14595  cau3lem  14702  rlimcld2  14923  addcn2  14938  mulcn2  14940  reccn2  14941  o1rlimmul  14963  rlimno1  14998  caucvgrlem  15017  isumrpcl  15186  isumltss  15191  expcnv  15207  mertenslem1  15228  effsumlt  15452  recoshcl  15499  eirrlem  15545  rpnnen2lem11  15565  bitsmod  15773  prmreclem3  16242  prmreclem5  16244  4sqlem7  16268  ssblex  22965  metss2lem  23048  methaus  23057  met1stc  23058  met2ndci  23059  metustto  23090  metustexhalf  23093  nlmvscnlem2  23221  nlmvscnlem1  23222  nrginvrcnlem  23227  nmoi2  23266  nghmcn  23281  reperflem  23353  iccntr  23356  icccmplem2  23358  reconnlem2  23362  opnreen  23366  metdcnlem  23371  metnrmlem3  23396  addcnlem  23399  cnheibor  23486  cnllycmp  23487  lebnumlem3  23494  lebnumii  23497  nmoleub2lem  23645  nmoleub2lem3  23646  nmoleub2lem2  23647  nmoleub3  23650  nmhmcn  23651  ipcnlem2  23774  ipcnlem1  23775  lmnn  23793  iscfil3  23803  cfilfcls  23804  iscmet3lem1  23821  iscmet3lem2  23822  bcthlem4  23857  bcthlem5  23858  minveclem3b  23958  minveclem3  23959  ivthlem2  23980  ovolgelb  24008  ovollb2lem  24016  ovolunlem1a  24024  ovolunlem1  24025  ovoliunlem1  24030  ovoliunlem2  24031  ovolscalem1  24041  ioombl1lem2  24087  ioombl1lem4  24089  uniioombllem1  24109  uniioombllem3  24113  uniioombllem4  24114  uniioombllem5  24115  opnmbllem  24129  volcn  24134  vitalilem4  24139  itg2mulclem  24274  itg2monolem3  24280  itg2cnlem2  24290  itg2cn  24291  itggt0  24369  dveflem  24503  dvferm1lem  24508  dvferm2lem  24510  lhop1lem  24537  lhop1  24538  lhop  24540  dvcnvrelem1  24541  dvcnvrelem2  24542  dvcnvre  24543  dvfsumrlim  24555  ftc1a  24561  ftc1lem4  24563  plyeq0lem  24727  aalioulem2  24849  aalioulem4  24851  aalioulem5  24852  aalioulem6  24853  aaliou  24854  aaliou2b  24857  aaliou3lem1  24858  aaliou3lem2  24859  aaliou3lem8  24861  aaliou3lem5  24863  aaliou3lem7  24865  aaliou3lem9  24866  ulmcn  24914  ulmdvlem1  24915  mtest  24919  itgulm  24923  psercn  24941  pserdvlem1  24942  pserdvlem2  24943  pserdv  24944  abelthlem7  24953  pilem2  24967  divlogrlim  25145  logcnlem3  25154  logcnlem4  25155  logccv  25173  divcxp  25197  cxplt  25204  cxple2  25207  cxpcn3lem  25255  cxpaddlelem  25259  cxpaddle  25260  loglesqrt  25266  leibpi  25447  rlimcnp3  25472  cxplim  25476  rlimcxp  25478  cxp2limlem  25480  cxp2lim  25481  cxploglim  25482  cxploglim2  25483  divsqrtsumlem  25484  jensenlem2  25492  logdifbnd  25498  emcllem4  25503  harmonicbnd4  25515  fsumharmonic  25516  zetacvg  25519  lgamgulmlem2  25534  lgamgulmlem5  25537  lgamucov  25542  regamcl  25565  relgamcl  25566  ftalem1  25577  ftalem2  25578  ftalem3  25579  ftalem5  25581  basellem1  25585  basellem3  25587  basellem4  25588  basellem8  25592  chtwordi  25660  chpchtsum  25722  logfacrlim  25727  logexprlim  25728  bclbnd  25783  efexple  25784  bposlem1  25787  bposlem2  25788  bposlem6  25792  bposlem7  25793  chebbnd1lem3  25974  chebbnd1  25975  chtppilimlem1  25976  chtppilimlem2  25977  chpo1ubb  25984  rplogsumlem1  25987  rplogsumlem2  25988  dchrisum0lem1a  25989  rpvmasumlem  25990  dchrisumlem2  25993  dchrisumlem3  25994  dchrmusumlema  25996  dchrmusum2  25997  dchrvmasumlem1  25998  dchrvmasum2lem  25999  dchrvmasumlema  26003  dchrvmasumiflem1  26004  dchrisum0fno1  26014  dchrisum0lem1b  26018  dchrisum0lem1  26019  dchrisum0lem2  26021  dchrisum0lem3  26022  dchrisum0  26023  mulogsumlem  26034  logdivsum  26036  mulog2sumlem2  26038  vmalogdivsum2  26041  2vmadivsumlem  26043  log2sumbnd  26047  selberglem2  26049  selberg  26051  selberg2lem  26053  chpdifbndlem1  26056  chpdifbndlem2  26057  selberg3lem1  26060  selberg4lem1  26063  pntrsumbnd2  26070  pntrlog2bndlem2  26081  pntrlog2bndlem3  26082  pntrlog2bndlem5  26084  pntrlog2bndlem6a  26085  pntrlog2bndlem6  26086  pntrlog2bnd  26087  pntpbnd1a  26088  pntpbnd1  26089  pntpbnd2  26090  pntibndlem1  26092  pntibndlem2  26094  pntibndlem3  26095  pntibnd  26096  pntlemc  26098  pntlema  26099  pntlemb  26100  pntlemg  26101  pntlemh  26102  pntlemn  26103  pntlemq  26104  pntlemr  26105  pntlemj  26106  pntlemi  26107  pntlemf  26108  pntlemk  26109  pntlemo  26110  pntleme  26111  pntlem3  26112  pntlemp  26113  pntleml  26114  ostth2lem1  26121  ostth2lem3  26138  ostth2  26140  ostth3  26141  crctcshwlkn0lem5  27519  smcnlem  28401  blocnilem  28508  blocni  28509  ubthlem2  28575  minvecolem3  28580  minvecolem4  28584  minvecolem5  28585  nmcexi  29730  lnconi  29737  fsumub  30471  rpxdivcld  30537  sqsscirc1  31050  cnre2csqlem  31052  tpr2rico  31054  xrmulc1cn  31072  xrge0iifiso  31077  xrge0iifhom  31079  esumcst  31221  esumdivc  31241  dya2icoseg  31434  omssubaddlem  31456  omssubadd  31457  probmeasb  31587  sgnmulrp2  31700  signsply0  31720  logdivsqrle  31820  hgt750leme  31828  dnicn  33728  unblimceq0lem  33742  unbdqndv2lem1  33745  unbdqndv2lem2  33746  knoppndvlem18  33765  knoppndvlem21  33768  poimirlem29  34802  heicant  34808  opnmbllem0  34809  mblfinlem3  34812  itg2addnclem3  34826  itg2addnc  34827  itggt0cn  34845  ftc1cnnclem  34846  ftc1anclem6  34853  ftc1anclem7  34854  geomcau  34915  sstotbnd2  34933  isbnd3  34943  equivbnd  34949  prdsbnd2  34954  cntotbnd  34955  heibor1lem  34968  heiborlem6  34975  bfplem1  34981  bfplem2  34982  bfp  34983  rrndstprj2  34990  rrnequiv  34994  fltnlta  39153  irrapxlem4  39300  irrapxlem5  39301  irrapx1  39303  pell1qrgaplem  39348  pell14qrgapw  39351  pellqrexplicit  39352  pellqrex  39354  pellfundge  39357  pellfundgt1  39358  rmspecfund  39384  rmxycomplete  39392  rmxypos  39422  binomcxplemnotnn0  40565  suprltrp  41472  supxrge  41482  infrpge  41495  infleinflem1  41514  xralrple4  41517  recnnltrp  41521  rpgtrecnn  41525  fmul01lt1lem1  41741  fmul01lt1lem2  41742  ltmod  41795  lptre2pt  41797  addlimc  41805  0ellimcdiv  41806  limclner  41808  climleltrp  41833  climisp  41903  climxrrelem  41906  climxrre  41907  limsupgtlem  41934  liminfltlem  41961  cnrefiisplem  41986  climxlim2lem  42002  dvdivbd  42084  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  itgiccshift  42141  itgperiod  42142  stoweidlem1  42163  stoweidlem3  42165  stoweidlem5  42167  stoweidlem7  42169  stoweidlem11  42173  stoweidlem13  42175  stoweidlem14  42176  stoweidlem24  42186  stoweidlem25  42187  stoweidlem26  42188  stoweidlem34  42196  stoweidlem41  42203  stoweidlem42  42204  stoweidlem49  42211  stoweidlem51  42213  stoweidlem52  42214  stoweidlem59  42221  stoweidlem60  42222  stoweidlem62  42224  stoweid  42225  wallispilem5  42231  stirlinglem1  42236  stirlinglem4  42239  stirlinglem5  42240  stirlinglem6  42241  dirkercncflem1  42265  fourierdlem30  42299  fourierdlem39  42308  fourierdlem47  42315  fourierdlem73  42341  fourierdlem81  42349  fourierdlem87  42355  fourierdlem103  42371  fourierdlem104  42372  fourierdlem107  42375  rrndistlt  42452  qndenserrnbllem  42456  sge0ltfirp  42559  sge0rpcpnf  42580  sge0xaddlem1  42592  omeiunltfirp  42678  carageniuncllem2  42681  ovnsubaddlem1  42729  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  hoiqssbllem1  42781  hoiqssbllem2  42782  hoiqssbllem3  42783  hspmbllem2  42786  hspmbllem3  42787  ovolval5lem1  42811  ovolval5lem2  42812  iinhoiicc  42833  vonioolem1  42839  pimrecltpos  42864  smflimlem3  42926  smfmullem1  42943  smfmullem2  42944  smfmullem3  42945  modexp2m1d  43654  dignn0flhalflem1  44603  itsclc0yqsol  44679  amgmwlem  44831  amgmw2d  44833  young2d  44834
  Copyright terms: Public domain W3C validator