Theorem rpred 12701

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 12666	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3915	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-rp 12660

This theorem is referenced by:  rpxrd  12702  rpcnd  12703  rpregt0d  12707  rprege0d  12708  rprene0d  12709  rprecred  12712  ltmulgt11d  12736  ltmulgt12d  12737  gt0divd  12738  ge0divd  12739  lediv12ad  12760  prodge0rd  12766  xlemul1  12953  xov1plusxeqvd  13159  ltexp2a  13812  rpexpmord  13814  expcan  13815  ltexp2  13816  leexp2a  13818  expnlbnd2  13877  expmulnbnd  13878  sqrlem6  14887  cau3lem  14994  rlimcld2  15215  addcn2  15231  mulcn2  15233  reccn2  15234  o1rlimmul  15256  rlimno1  15293  caucvgrlem  15312  isumrpcl  15483  isumltss  15488  expcnv  15504  mertenslem1  15524  effsumlt  15748  recoshcl  15795  eirrlem  15841  rpnnen2lem11  15861  bitsmod  16071  prmreclem3  16547  prmreclem5  16549  4sqlem7  16573  ssblex  23489  metss2lem  23573  methaus  23582  met1stc  23583  met2ndci  23584  metustto  23615  metustexhalf  23618  nlmvscnlem2  23755  nlmvscnlem1  23756  nrginvrcnlem  23761  nmoi2  23800  nghmcn  23815  reperflem  23887  iccntr  23890  icccmplem2  23892  reconnlem2  23896  opnreen  23900  metdcnlem  23905  metnrmlem3  23930  addcnlem  23933  cnheibor  24024  cnllycmp  24025  lebnumlem3  24032  lebnumii  24035  nmoleub2lem  24183  nmoleub2lem3  24184  nmoleub2lem2  24185  nmoleub3  24188  nmhmcn  24189  ipcnlem2  24313  ipcnlem1  24314  lmnn  24332  iscfil3  24342  cfilfcls  24343  iscmet3lem1  24360  iscmet3lem2  24361  bcthlem4  24396  bcthlem5  24397  minveclem3b  24497  minveclem3  24498  ivthlem2  24521  ovolgelb  24549  ovollb2lem  24557  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovolscalem1  24582  ioombl1lem2  24628  ioombl1lem4  24630  uniioombllem1  24650  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  opnmbllem  24670  volcn  24675  vitalilem4  24680  itg2mulclem  24816  itg2monolem3  24822  itg2cnlem2  24832  itg2cn  24833  itggt0  24913  dveflem  25048  dvferm1lem  25053  dvferm2lem  25055  lhop1lem  25082  lhop1  25083  lhop  25085  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcnvre  25088  dvfsumrlim  25100  ftc1a  25106  ftc1lem4  25108  plyeq0lem  25276  aalioulem2  25398  aalioulem4  25400  aalioulem5  25401  aalioulem6  25402  aaliou  25403  aaliou2b  25406  aaliou3lem1  25407  aaliou3lem2  25408  aaliou3lem8  25410  aaliou3lem5  25412  aaliou3lem7  25414  aaliou3lem9  25415  ulmcn  25463  ulmdvlem1  25464  mtest  25468  itgulm  25472  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  pserdv  25493  abelthlem7  25502  pilem2  25516  divlogrlim  25695  logcnlem3  25704  logcnlem4  25705  logccv  25723  divcxp  25747  cxplt  25754  cxple2  25757  cxpcn3lem  25805  cxpaddlelem  25809  cxpaddle  25810  loglesqrt  25816  leibpi  25997  rlimcnp3  26022  cxplim  26026  rlimcxp  26028  cxp2limlem  26030  cxp2lim  26031  cxploglim  26032  cxploglim2  26033  divsqrtsumlem  26034  jensenlem2  26042  logdifbnd  26048  emcllem4  26053  harmonicbnd4  26065  fsumharmonic  26066  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem5  26087  lgamucov  26092  regamcl  26115  relgamcl  26116  ftalem1  26127  ftalem2  26128  ftalem3  26129  ftalem5  26131  basellem1  26135  basellem3  26137  basellem4  26138  basellem8  26142  chtwordi  26210  chpchtsum  26272  logfacrlim  26277  logexprlim  26278  bclbnd  26333  efexple  26334  bposlem1  26337  bposlem2  26338  bposlem6  26342  bposlem7  26343  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chpo1ubb  26534  rplogsumlem1  26537  rplogsumlem2  26538  dchrisum0lem1a  26539  rpvmasumlem  26540  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0fno1  26564  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  mulogsumlem  26584  logdivsum  26586  mulog2sumlem2  26588  vmalogdivsum2  26591  2vmadivsumlem  26593  log2sumbnd  26597  selberglem2  26599  selberg  26601  selberg2lem  26603  chpdifbndlem1  26606  chpdifbndlem2  26607  selberg3lem1  26610  selberg4lem1  26613  pntrsumbnd2  26620  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntrlog2bndlem6a  26635  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem1  26642  pntibndlem2  26644  pntibndlem3  26645  pntibnd  26646  pntlemc  26648  pntlema  26649  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemn  26653  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemi  26657  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntleme  26661  pntlem3  26662  pntlemp  26663  pntleml  26664  ostth2lem1  26671  ostth2lem3  26688  ostth2  26690  ostth3  26691  crctcshwlkn0lem5  28080  smcnlem  28960  blocnilem  29067  blocni  29068  ubthlem2  29134  minvecolem3  29139  minvecolem4  29143  minvecolem5  29144  nmcexi  30289  lnconi  30296  fsumub  31044  rpxdivcld  31110  sqsscirc1  31760  cnre2csqlem  31762  tpr2rico  31764  xrmulc1cn  31782  xrge0iifiso  31787  xrge0iifhom  31789  esumcst  31931  esumdivc  31951  dya2icoseg  32144  omssubaddlem  32166  omssubadd  32167  probmeasb  32297  sgnmulrp2  32410  signsply0  32430  logdivsqrle  32530  hgt750leme  32538  dnicn  34599  unblimceq0lem  34613  unbdqndv2lem1  34616  unbdqndv2lem2  34617  knoppndvlem18  34636  knoppndvlem21  34639  poimirlem29  35733  heicant  35739  opnmbllem0  35740  mblfinlem3  35743  itg2addnclem3  35757  itg2addnc  35758  itggt0cn  35774  ftc1cnnclem  35775  ftc1anclem6  35782  ftc1anclem7  35783  geomcau  35844  sstotbnd2  35859  isbnd3  35869  equivbnd  35875  prdsbnd2  35880  cntotbnd  35881  heibor1lem  35894  heiborlem6  35901  bfplem1  35907  bfplem2  35908  bfp  35909  rrndstprj2  35916  rrnequiv  35920  lcmineqlem21  39985  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p5  40016  aks4d1p6  40017  exp11nnd  40245  fltnlta  40416  irrapxlem4  40563  irrapxlem5  40564  irrapx1  40566  pell1qrgaplem  40611  pell14qrgapw  40614  pellqrexplicit  40615  pellqrex  40617  pellfundge  40620  pellfundgt1  40621  rmspecfund  40647  rmxycomplete  40655  rmxypos  40685  binomcxplemnotnn0  41863  suprltrp  42757  supxrge  42767  infrpge  42780  infleinflem1  42799  xralrple4  42802  recnnltrp  42806  rpgtrecnn  42809  fmul01lt1lem1  43015  fmul01lt1lem2  43016  ltmod  43069  lptre2pt  43071  addlimc  43079  0ellimcdiv  43080  limclner  43082  climleltrp  43107  climisp  43177  climxrrelem  43180  climxrre  43181  limsupgtlem  43208  liminfltlem  43235  cnrefiisplem  43260  climxlim2lem  43276  dvdivbd  43354  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  itgiccshift  43411  itgperiod  43412  stoweidlem1  43432  stoweidlem3  43434  stoweidlem5  43436  stoweidlem7  43438  stoweidlem11  43442  stoweidlem13  43444  stoweidlem14  43445  stoweidlem24  43455  stoweidlem25  43456  stoweidlem26  43457  stoweidlem34  43465  stoweidlem41  43472  stoweidlem42  43473  stoweidlem49  43480  stoweidlem51  43482  stoweidlem52  43483  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  stoweid  43494  wallispilem5  43500  stirlinglem1  43505  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  dirkercncflem1  43534  fourierdlem30  43568  fourierdlem39  43577  fourierdlem47  43584  fourierdlem73  43610  fourierdlem81  43618  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  rrndistlt  43721  qndenserrnbllem  43725  sge0ltfirp  43828  sge0rpcpnf  43849  sge0xaddlem1  43861  omeiunltfirp  43947  carageniuncllem2  43950  ovnsubaddlem1  43998  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoiqssbllem1  44050  hoiqssbllem2  44051  hoiqssbllem3  44052  hspmbllem2  44055  hspmbllem3  44056  ovolval5lem1  44080  ovolval5lem2  44081  iinhoiicc  44102  vonioolem1  44108  pimrecltpos  44133  smflimlem3  44195  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  modexp2m1d  44952  dignn0flhalflem1  45849  itsclc0yqsol  45998  amgmwlem  46392  amgmw2d  46394  young2d  46395