Theorem rpred 13060

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 3963	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11137  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-ss 3950  df-rp 13018

This theorem is referenced by:  rpxrd  13061  rpcnd  13062  rpregt0d  13066  rprege0d  13067  rprene0d  13068  rprecred  13071  ltmulgt11d  13095  ltmulgt12d  13096  gt0divd  13097  ge0divd  13098  lediv12ad  13119  prodge0rd  13125  xlemul1  13315  xov1plusxeqvd  13521  ltexp2a  14189  rpexpmord  14191  expcan  14192  ltexp2  14193  leexp2a  14195  expnlbnd2  14256  expmulnbnd  14257  exp11nnd  14283  01sqrexlem6  15269  cau3lem  15376  rlimcld2  15597  addcn2  15613  mulcn2  15615  reccn2  15616  o1rlimmul  15638  rlimno1  15673  caucvgrlem  15692  isumrpcl  15862  isumltss  15867  expcnv  15883  mertenslem1  15903  effsumlt  16130  recoshcl  16177  eirrlem  16223  rpnnen2lem11  16243  bitsmod  16456  prmreclem3  16939  prmreclem5  16941  4sqlem7  16965  ssblex  24402  metss2lem  24487  methaus  24496  met1stc  24497  met2ndci  24498  metustto  24529  metustexhalf  24532  nlmvscnlem2  24661  nlmvscnlem1  24662  nrginvrcnlem  24667  nmoi2  24706  nghmcn  24721  reperflem  24795  iccntr  24798  icccmplem2  24800  reconnlem2  24804  opnreen  24808  metdcnlem  24813  metnrmlem3  24838  addcnlem  24841  cnheibor  24942  cnllycmp  24943  lebnumlem3  24950  lebnumii  24953  nmoleub2lem  25102  nmoleub2lem3  25103  nmoleub2lem2  25104  nmoleub3  25107  nmhmcn  25108  ipcnlem2  25233  ipcnlem1  25234  lmnn  25252  iscfil3  25262  cfilfcls  25263  iscmet3lem1  25280  iscmet3lem2  25281  bcthlem4  25316  bcthlem5  25317  minveclem3b  25417  minveclem3  25418  ivthlem2  25442  ovolgelb  25470  ovollb2lem  25478  ovolunlem1a  25486  ovolunlem1  25487  ovoliunlem1  25492  ovoliunlem2  25493  ovolscalem1  25503  ioombl1lem2  25549  ioombl1lem4  25551  uniioombllem1  25571  uniioombllem3  25575  uniioombllem4  25576  uniioombllem5  25577  opnmbllem  25591  volcn  25596  vitalilem4  25601  itg2mulclem  25736  itg2monolem3  25742  itg2cnlem2  25752  itg2cn  25753  itggt0  25834  dveflem  25972  dvferm1lem  25977  dvferm2lem  25979  lhop1lem  26007  lhop1  26008  lhop  26010  dvcnvrelem1  26011  dvcnvrelem2  26012  dvcnvre  26013  dvfsumrlim  26027  ftc1a  26033  ftc1lem4  26035  plyeq0lem  26204  aalioulem2  26330  aalioulem4  26332  aalioulem5  26333  aalioulem6  26334  aaliou  26335  aaliou2b  26338  aaliou3lem1  26339  aaliou3lem2  26340  aaliou3lem8  26342  aaliou3lem5  26344  aaliou3lem7  26346  aaliou3lem9  26347  ulmcn  26397  ulmdvlem1  26398  mtest  26402  itgulm  26406  psercn  26425  pserdvlem1  26426  pserdvlem2  26427  pserdv  26428  abelthlem7  26437  pilem2  26451  divlogrlim  26632  logcnlem3  26641  logcnlem4  26642  logccv  26660  divcxp  26684  cxplt  26691  cxple2  26694  recxpf1lem  26726  cxpcn3lem  26745  cxpaddlelem  26749  cxpaddle  26750  loglesqrt  26759  leibpi  26940  rlimcnp3  26965  cxplim  26970  rlimcxp  26972  cxp2limlem  26974  cxp2lim  26975  cxploglim  26976  cxploglim2  26977  divsqrtsumlem  26978  jensenlem2  26986  logdifbnd  26992  emcllem4  26997  harmonicbnd4  27009  fsumharmonic  27010  zetacvg  27013  lgamgulmlem2  27028  lgamgulmlem5  27031  lgamucov  27036  regamcl  27059  relgamcl  27060  ftalem1  27071  ftalem2  27072  ftalem3  27073  ftalem5  27075  basellem1  27079  basellem3  27081  basellem4  27082  basellem8  27086  chtwordi  27154  chpchtsum  27218  logfacrlim  27223  logexprlim  27224  bclbnd  27279  efexple  27280  bposlem1  27283  bposlem2  27284  bposlem6  27288  bposlem7  27289  chebbnd1lem3  27470  chebbnd1  27471  chtppilimlem1  27472  chtppilimlem2  27473  chpo1ubb  27480  rplogsumlem1  27483  rplogsumlem2  27484  dchrisum0lem1a  27485  rpvmasumlem  27486  dchrisumlem2  27489  dchrisumlem3  27490  dchrmusumlema  27492  dchrmusum2  27493  dchrvmasumlem1  27494  dchrvmasum2lem  27495  dchrvmasumlema  27499  dchrvmasumiflem1  27500  dchrisum0fno1  27510  dchrisum0lem1b  27514  dchrisum0lem1  27515  dchrisum0lem2  27517  dchrisum0lem3  27518  dchrisum0  27519  mulogsumlem  27530  logdivsum  27532  mulog2sumlem2  27534  vmalogdivsum2  27537  2vmadivsumlem  27539  log2sumbnd  27543  selberglem2  27545  selberg  27547  selberg2lem  27549  chpdifbndlem1  27552  chpdifbndlem2  27553  selberg3lem1  27556  selberg4lem1  27559  pntrsumbnd2  27566  pntrlog2bndlem2  27577  pntrlog2bndlem3  27578  pntrlog2bndlem5  27580  pntrlog2bndlem6a  27581  pntrlog2bndlem6  27582  pntrlog2bnd  27583  pntpbnd1a  27584  pntpbnd1  27585  pntpbnd2  27586  pntibndlem1  27588  pntibndlem2  27590  pntibndlem3  27591  pntibnd  27592  pntlemc  27594  pntlema  27595  pntlemb  27596  pntlemg  27597  pntlemh  27598  pntlemn  27599  pntlemq  27600  pntlemr  27601  pntlemj  27602  pntlemi  27603  pntlemf  27604  pntlemk  27605  pntlemo  27606  pntleme  27607  pntlem3  27608  pntlemp  27609  pntleml  27610  ostth2lem1  27617  ostth2lem3  27634  ostth2  27636  ostth3  27637  crctcshwlkn0lem5  29781  nrt2irr  30439  smcnlem  30663  blocnilem  30770  blocni  30771  ubthlem2  30837  minvecolem3  30842  minvecolem4  30846  minvecolem5  30847  nmcexi  31992  lnconi  31999  fsumub  32777  rpxdivcld  32863  sqsscirc1  33848  cnre2csqlem  33850  tpr2rico  33852  xrmulc1cn  33870  xrge0iifiso  33875  xrge0iifhom  33877  esumcst  34005  esumdivc  34025  dya2icoseg  34220  omssubaddlem  34242  omssubadd  34243  probmeasb  34373  sgnmulrp2  34487  signsply0  34507  logdivsqrle  34606  hgt750leme  34614  dnicn  36434  unblimceq0lem  36448  unbdqndv2lem1  36451  unbdqndv2lem2  36452  knoppndvlem18  36471  knoppndvlem21  36474  poimirlem29  37597  heicant  37603  opnmbllem0  37604  mblfinlem3  37607  itg2addnclem3  37621  itg2addnc  37622  itggt0cn  37638  ftc1cnnclem  37639  ftc1anclem6  37646  ftc1anclem7  37647  geomcau  37707  sstotbnd2  37722  isbnd3  37732  equivbnd  37738  prdsbnd2  37743  cntotbnd  37744  heibor1lem  37757  heiborlem6  37764  bfplem1  37770  bfplem2  37771  bfp  37772  rrndstprj2  37779  rrnequiv  37783  lcmineqlem21  41991  aks4d1p1p4  42013  aks4d1p1p7  42016  aks4d1p5  42022  aks4d1p6  42023  aks6d1c2  42072  fltnlta  42618  irrapxlem4  42781  irrapxlem5  42782  irrapx1  42784  pell1qrgaplem  42829  pell14qrgapw  42832  pellqrexplicit  42833  pellqrex  42835  pellfundge  42838  pellfundgt1  42839  rmspecfund  42865  rmxycomplete  42874  rmxypos  42904  binomcxplemnotnn0  44320  suprltrp  45284  supxrge  45294  infrpge  45307  infleinflem1  45326  xralrple4  45329  recnnltrp  45333  rpgtrecnn  45336  cvgcaule  45447  fmul01lt1lem1  45544  fmul01lt1lem2  45545  ltmod  45598  lptre2pt  45600  addlimc  45608  0ellimcdiv  45609  limclner  45611  climleltrp  45636  climisp  45706  climxrrelem  45709  climxrre  45710  limsupgtlem  45737  liminfltlem  45764  cnrefiisplem  45789  climxlim2lem  45805  dvdivbd  45883  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  itgiccshift  45940  itgperiod  45941  stoweidlem1  45961  stoweidlem3  45963  stoweidlem5  45965  stoweidlem7  45967  stoweidlem11  45971  stoweidlem13  45973  stoweidlem14  45974  stoweidlem24  45984  stoweidlem25  45985  stoweidlem26  45986  stoweidlem34  45994  stoweidlem41  46001  stoweidlem42  46002  stoweidlem49  46009  stoweidlem51  46011  stoweidlem52  46012  stoweidlem59  46019  stoweidlem60  46020  stoweidlem62  46022  stoweid  46023  wallispilem5  46029  stirlinglem1  46034  stirlinglem4  46037  stirlinglem5  46038  stirlinglem6  46039  dirkercncflem1  46063  fourierdlem30  46097  fourierdlem39  46106  fourierdlem47  46113  fourierdlem73  46139  fourierdlem81  46147  fourierdlem87  46153  fourierdlem103  46169  fourierdlem104  46170  fourierdlem107  46173  rrndistlt  46250  qndenserrnbllem  46254  sge0ltfirp  46360  sge0rpcpnf  46381  sge0xaddlem1  46393  omeiunltfirp  46479  carageniuncllem2  46482  ovnsubaddlem1  46530  hoidmvlelem1  46555  hoidmvlelem2  46556  hoidmvlelem3  46557  hoidmvlelem4  46558  hoiqssbllem1  46582  hoiqssbllem2  46583  hoiqssbllem3  46584  hspmbllem2  46587  hspmbllem3  46588  ovolval5lem1  46612  ovolval5lem2  46613  iinhoiicc  46634  vonioolem1  46640  pimrecltpos  46668  smflimlem3  46733  smfmullem1  46751  smfmullem2  46752  smfmullem3  46753  modexp2m1d  47545  dignn0flhalflem1  48482  itsclc0yqsol  48631  amgmwlem  49317  amgmw2d  49319  young2d  49320