Theorem rpred 13061

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

Step	Hyp	Ref	Expression
1		rpssre 13025	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3936	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923  df-rp 13018

This theorem is referenced by:  rpxrd  13062  rpcnd  13063  rpregt0d  13067  rprege0d  13068  rprene0d  13069  rprecred  13072  ltmulgt11d  13096  ltmulgt12d  13097  gt0divd  13098  ge0divd  13099  lediv12ad  13120  prodge0rd  13126  xlemul1  13317  xov1plusxeqvd  13526  ltexp2a  14204  rpexpmord  14206  expcan  14207  ltexp2  14208  leexp2a  14210  expnlbnd2  14272  expmulnbnd  14273  exp11nnd  14299  sgnmulrp2  15147  01sqrexlem6  15300  cau3lem  15408  rlimcld2  15631  addcn2  15647  mulcn2  15649  reccn2  15650  o1rlimmul  15672  rlimno1  15707  caucvgrlem  15726  isumrpcl  15899  isumltss  15904  expcnv  15920  mertenslem1  15940  effsumlt  16168  recoshcl  16215  eirrlem  16261  rpnnen2lem11  16281  bitsmod  16495  prmreclem3  16979  prmreclem5  16981  4sqlem7  17005  ssblex  24566  metss2lem  24649  methaus  24658  met1stc  24659  met2ndci  24660  metustto  24691  metustexhalf  24694  nlmvscnlem2  24823  nlmvscnlem1  24824  nrginvrcnlem  24829  nmoi2  24868  nghmcn  24883  reperflem  24957  iccntr  24960  icccmplem2  24962  reconnlem2  24966  opnreen  24970  metdcnlem  24975  metnrmlem3  25000  addcnlem  25003  cnheibor  25095  cnllycmp  25096  lebnumlem3  25103  lebnumii  25106  nmoleub2lem  25254  nmoleub2lem3  25255  nmoleub2lem2  25256  nmoleub3  25259  nmhmcn  25260  ipcnlem2  25384  ipcnlem1  25385  lmnn  25403  iscfil3  25413  cfilfcls  25414  iscmet3lem1  25431  iscmet3lem2  25432  bcthlem4  25467  bcthlem5  25468  minveclem3b  25568  minveclem3  25569  ivthlem2  25592  ovolgelb  25620  ovollb2lem  25628  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovoliunlem2  25643  ovolscalem1  25653  ioombl1lem2  25699  ioombl1lem4  25701  uniioombllem1  25721  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  opnmbllem  25741  volcn  25746  vitalilem4  25751  itg2mulclem  25886  itg2monolem3  25892  itg2cnlem2  25902  itg2cn  25903  itggt0  25984  dveflem  26119  dvferm1lem  26124  dvferm2lem  26126  lhop1lem  26153  lhop1  26154  lhop  26156  dvcnvrelem1  26157  dvcnvrelem2  26158  dvcnvre  26159  dvfsumrlim  26171  ftc1a  26177  ftc1lem4  26179  plyeq0lem  26348  aalioulem2  26475  aalioulem4  26477  aalioulem5  26478  aalioulem6  26479  aaliou  26480  aaliou2b  26483  aaliou3lem1  26484  aaliou3lem2  26485  aaliou3lem8  26487  aaliou3lem5  26489  aaliou3lem7  26491  aaliou3lem9  26492  ulmcn  26540  ulmdvlem1  26541  mtest  26545  itgulm  26549  psercn  26567  pserdvlem1  26568  pserdvlem2  26569  pserdv  26570  abelthlem7  26579  pilem2  26593  divlogrlim  26778  logcnlem3  26787  logcnlem4  26788  logccv  26806  divcxp  26830  cxplt  26837  cxple2  26840  recxpf1lem  26872  cxpcn3lem  26890  cxpaddlelem  26894  cxpaddle  26895  loglesqrt  26904  leibpi  27085  rlimcnp3  27110  cxplim  27114  rlimcxp  27116  cxp2limlem  27118  cxp2lim  27119  cxploglim  27120  cxploglim2  27121  divsqrtsumlem  27122  jensenlem2  27130  logdifbnd  27136  emcllem4  27141  harmonicbnd4  27153  fsumharmonic  27154  zetacvg  27157  lgamgulmlem2  27172  lgamgulmlem5  27175  lgamucov  27180  regamcl  27203  relgamcl  27204  ftalem1  27215  ftalem2  27216  ftalem3  27217  ftalem5  27219  basellem1  27223  basellem3  27225  basellem4  27226  basellem8  27230  chtwordi  27298  chpchtsum  27361  logfacrlim  27366  logexprlim  27367  bclbnd  27422  efexple  27423  bposlem1  27426  bposlem2  27427  bposlem6  27431  bposlem7  27432  chebbnd1lem3  27613  chebbnd1  27614  chtppilimlem1  27615  chtppilimlem2  27616  chpo1ubb  27623  rplogsumlem1  27626  rplogsumlem2  27627  dchrisum0lem1a  27628  rpvmasumlem  27629  dchrisumlem2  27632  dchrisumlem3  27633  dchrmusumlema  27635  dchrmusum2  27636  dchrvmasumlem1  27637  dchrvmasum2lem  27638  dchrvmasumlema  27642  dchrvmasumiflem1  27643  dchrisum0fno1  27653  dchrisum0lem1b  27657  dchrisum0lem1  27658  dchrisum0lem2  27660  dchrisum0lem3  27661  dchrisum0  27662  mulogsumlem  27673  logdivsum  27675  mulog2sumlem2  27677  vmalogdivsum2  27680  2vmadivsumlem  27682  log2sumbnd  27686  selberglem2  27688  selberg  27690  selberg2lem  27692  chpdifbndlem1  27695  chpdifbndlem2  27696  selberg3lem1  27699  selberg4lem1  27702  pntrsumbnd2  27709  pntrlog2bndlem2  27720  pntrlog2bndlem3  27721  pntrlog2bndlem5  27723  pntrlog2bndlem6a  27724  pntrlog2bndlem6  27725  pntrlog2bnd  27726  pntpbnd1a  27727  pntpbnd1  27728  pntpbnd2  27729  pntibndlem1  27731  pntibndlem2  27733  pntibndlem3  27734  pntibnd  27735  pntlemc  27737  pntlema  27738  pntlemb  27739  pntlemg  27740  pntlemh  27741  pntlemn  27742  pntlemq  27743  pntlemr  27744  pntlemj  27745  pntlemi  27746  pntlemf  27747  pntlemk  27748  pntlemo  27749  pntleme  27750  pntlem3  27751  pntlemp  27752  pntleml  27753  ostth2lem1  27760  ostth2lem3  27777  ostth2  27779  ostth3  27780  crctcshwlkn0lem5  30141  nrt2irr  30802  smcnlem  31027  blocnilem  31134  blocni  31135  ubthlem2  31201  minvecolem3  31206  minvecolem4  31210  minvecolem5  31211  nmcexi  32356  lnconi  32363  fsumub  33150  rpxdivcld  33231  constrinvcl  34141  constrsqrtcl  34147  sqsscirc1  34276  cnre2csqlem  34278  tpr2rico  34280  xrmulc1cn  34298  xrge0iifiso  34303  xrge0iifhom  34305  esumcst  34431  esumdivc  34451  dya2icoseg  34645  omssubaddlem  34667  omssubadd  34668  probmeasb  34798  signsply0  34916  logdivsqrle  35015  hgt750leme  35023  dnicn  37059  unblimceq0lem  37073  unbdqndv2lem1  37076  unbdqndv2lem2  37077  knoppndvlem18  37096  knoppndvlem21  37099  poimirlem29  38278  heicant  38284  opnmbllem0  38285  mblfinlem3  38288  itg2addnclem3  38302  itg2addnc  38303  itggt0cn  38319  ftc1cnnclem  38320  ftc1anclem6  38327  ftc1anclem7  38328  geomcau  38388  sstotbnd2  38403  isbnd3  38413  equivbnd  38419  prdsbnd2  38424  cntotbnd  38425  heibor1lem  38438  heiborlem6  38445  bfplem1  38451  bfplem2  38452  bfp  38453  rrndstprj2  38460  rrnequiv  38464  lcmineqlem21  42794  aks4d1p1p4  42816  aks4d1p1p7  42819  aks4d1p5  42825  aks4d1p6  42826  aks6d1c2  42875  fltnlta  43375  irrapxlem4  43532  irrapxlem5  43533  irrapx1  43535  pell1qrgaplem  43580  pell14qrgapw  43583  pellqrexplicit  43584  pellqrex  43586  pellfundge  43589  pellfundgt1  43590  rmspecfund  43616  rmxycomplete  43624  rmxypos  43654  binomcxplemnotnn0  45046  suprltrp  46024  supxrge  46034  infrpge  46047  infleinflem1  46065  xralrple4  46068  recnnltrp  46072  rpgtrecnn  46075  cvgcaule  46185  fmul01lt1lem1  46280  fmul01lt1lem2  46281  ltmod  46332  lptre2pt  46334  addlimc  46342  0ellimcdiv  46343  limclner  46345  climleltrp  46370  climisp  46440  climxrrelem  46443  climxrre  46444  limsupgtlem  46471  liminfltlem  46498  cnrefiisplem  46523  climxlim2lem  46539  dvdivbd  46617  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  itgiccshift  46674  itgperiod  46675  stoweidlem1  46695  stoweidlem3  46697  stoweidlem5  46699  stoweidlem7  46701  stoweidlem11  46705  stoweidlem13  46707  stoweidlem14  46708  stoweidlem24  46718  stoweidlem25  46719  stoweidlem26  46720  stoweidlem34  46728  stoweidlem41  46735  stoweidlem42  46736  stoweidlem49  46743  stoweidlem51  46745  stoweidlem52  46746  stoweidlem59  46753  stoweidlem60  46754  stoweidlem62  46756  stoweid  46757  wallispilem5  46763  stirlinglem1  46768  stirlinglem4  46771  stirlinglem5  46772  stirlinglem6  46773  dirkercncflem1  46797  fourierdlem30  46831  fourierdlem39  46840  fourierdlem47  46847  fourierdlem73  46873  fourierdlem81  46881  fourierdlem87  46887  fourierdlem103  46903  fourierdlem104  46904  fourierdlem107  46907  rrndistlt  46984  qndenserrnbllem  46988  sge0ltfirp  47094  sge0rpcpnf  47115  sge0xaddlem1  47127  omeiunltfirp  47213  carageniuncllem2  47216  ovnsubaddlem1  47264  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  hoidmvlelem4  47292  hoiqssbllem1  47316  hoiqssbllem2  47317  hoiqssbllem3  47318  hspmbllem2  47321  hspmbllem3  47322  ovolval5lem1  47346  ovolval5lem2  47347  iinhoiicc  47368  vonioolem1  47374  pimrecltpos  47402  smflimlem3  47467  smfmullem1  47485  smfmullem2  47486  smfmullem3  47487  modexp2m1d  48341  dignn0flhalflem1  49372  itsclc0yqsol  49521  amgmwlem  50579  amgmw2d  50581  young2d  50582