Theorem rpred 13034

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  ℝ⁺crp 12990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3921  df-rp 12991

This theorem is referenced by:  rpxrd  13035  rpcnd  13036  rpregt0d  13040  rprege0d  13041  rprene0d  13042  rprecred  13045  ltmulgt11d  13069  ltmulgt12d  13070  gt0divd  13071  ge0divd  13072  lediv12ad  13093  prodge0rd  13099  xlemul1  13290  xov1plusxeqvd  13499  ltexp2a  14176  rpexpmord  14178  expcan  14179  ltexp2  14180  leexp2a  14182  expnlbnd2  14244  expmulnbnd  14245  exp11nnd  14271  01sqrexlem6  15257  cau3lem  15365  rlimcld2  15588  addcn2  15604  mulcn2  15606  reccn2  15607  o1rlimmul  15629  rlimno1  15664  caucvgrlem  15683  isumrpcl  15856  isumltss  15861  expcnv  15877  mertenslem1  15897  effsumlt  16126  recoshcl  16173  eirrlem  16219  rpnnen2lem11  16239  bitsmod  16453  prmreclem3  16937  prmreclem5  16939  4sqlem7  16963  ssblex  24468  metss2lem  24551  methaus  24560  met1stc  24561  met2ndci  24562  metustto  24593  metustexhalf  24596  nlmvscnlem2  24725  nlmvscnlem1  24726  nrginvrcnlem  24731  nmoi2  24770  nghmcn  24785  reperflem  24859  iccntr  24862  icccmplem2  24864  reconnlem2  24868  opnreen  24872  metdcnlem  24877  metnrmlem3  24902  addcnlem  24905  cnheibor  24997  cnllycmp  24998  lebnumlem3  25005  lebnumii  25008  nmoleub2lem  25156  nmoleub2lem3  25157  nmoleub2lem2  25158  nmoleub3  25161  nmhmcn  25162  ipcnlem2  25286  ipcnlem1  25287  lmnn  25305  iscfil3  25315  cfilfcls  25316  iscmet3lem1  25333  iscmet3lem2  25334  bcthlem4  25369  bcthlem5  25370  minveclem3b  25470  minveclem3  25471  ivthlem2  25494  ovolgelb  25522  ovollb2lem  25530  ovolunlem1a  25538  ovolunlem1  25539  ovoliunlem1  25544  ovoliunlem2  25545  ovolscalem1  25555  ioombl1lem2  25601  ioombl1lem4  25603  uniioombllem1  25623  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  opnmbllem  25643  volcn  25648  vitalilem4  25653  itg2mulclem  25788  itg2monolem3  25794  itg2cnlem2  25804  itg2cn  25805  itggt0  25886  dveflem  26021  dvferm1lem  26026  dvferm2lem  26028  lhop1lem  26055  lhop1  26056  lhop  26058  dvcnvrelem1  26059  dvcnvrelem2  26060  dvcnvre  26061  dvfsumrlim  26073  ftc1a  26079  ftc1lem4  26081  plyeq0lem  26250  aalioulem2  26374  aalioulem4  26376  aalioulem5  26377  aalioulem6  26378  aaliou  26379  aaliou2b  26382  aaliou3lem1  26383  aaliou3lem2  26384  aaliou3lem8  26386  aaliou3lem5  26388  aaliou3lem7  26390  aaliou3lem9  26391  ulmcn  26439  ulmdvlem1  26440  mtest  26444  itgulm  26448  psercn  26466  pserdvlem1  26467  pserdvlem2  26468  pserdv  26469  abelthlem7  26478  pilem2  26492  divlogrlim  26677  logcnlem3  26686  logcnlem4  26687  logccv  26705  divcxp  26729  cxplt  26736  cxple2  26739  recxpf1lem  26771  cxpcn3lem  26789  cxpaddlelem  26793  cxpaddle  26794  loglesqrt  26803  leibpi  26984  rlimcnp3  27009  cxplim  27013  rlimcxp  27015  cxp2limlem  27017  cxp2lim  27018  cxploglim  27019  cxploglim2  27020  divsqrtsumlem  27021  jensenlem2  27029  logdifbnd  27035  emcllem4  27040  harmonicbnd4  27052  fsumharmonic  27053  zetacvg  27056  lgamgulmlem2  27071  lgamgulmlem5  27074  lgamucov  27079  regamcl  27102  relgamcl  27103  ftalem1  27114  ftalem2  27115  ftalem3  27116  ftalem5  27118  basellem1  27122  basellem3  27124  basellem4  27125  basellem8  27129  chtwordi  27197  chpchtsum  27260  logfacrlim  27265  logexprlim  27266  bclbnd  27321  efexple  27322  bposlem1  27325  bposlem2  27326  bposlem6  27330  bposlem7  27331  chebbnd1lem3  27512  chebbnd1  27513  chtppilimlem1  27514  chtppilimlem2  27515  chpo1ubb  27522  rplogsumlem1  27525  rplogsumlem2  27526  dchrisum0lem1a  27527  rpvmasumlem  27528  dchrisumlem2  27531  dchrisumlem3  27532  dchrmusumlema  27534  dchrmusum2  27535  dchrvmasumlem1  27536  dchrvmasum2lem  27537  dchrvmasumlema  27541  dchrvmasumiflem1  27542  dchrisum0fno1  27552  dchrisum0lem1b  27556  dchrisum0lem1  27557  dchrisum0lem2  27559  dchrisum0lem3  27560  dchrisum0  27561  mulogsumlem  27572  logdivsum  27574  mulog2sumlem2  27576  vmalogdivsum2  27579  2vmadivsumlem  27581  log2sumbnd  27585  selberglem2  27587  selberg  27589  selberg2lem  27591  chpdifbndlem1  27594  chpdifbndlem2  27595  selberg3lem1  27598  selberg4lem1  27601  pntrsumbnd2  27608  pntrlog2bndlem2  27619  pntrlog2bndlem3  27620  pntrlog2bndlem5  27622  pntrlog2bndlem6a  27623  pntrlog2bndlem6  27624  pntrlog2bnd  27625  pntpbnd1a  27626  pntpbnd1  27627  pntpbnd2  27628  pntibndlem1  27630  pntibndlem2  27632  pntibndlem3  27633  pntibnd  27634  pntlemc  27636  pntlema  27637  pntlemb  27638  pntlemg  27639  pntlemh  27640  pntlemn  27641  pntlemq  27642  pntlemr  27643  pntlemj  27644  pntlemi  27645  pntlemf  27646  pntlemk  27647  pntlemo  27648  pntleme  27649  pntlem3  27650  pntlemp  27651  pntleml  27652  ostth2lem1  27659  ostth2lem3  27676  ostth2  27678  ostth3  27679  crctcshwlkn0lem5  29960  nrt2irr  30621  smcnlem  30846  blocnilem  30953  blocni  30954  ubthlem2  31020  minvecolem3  31025  minvecolem4  31029  minvecolem5  31030  nmcexi  32175  lnconi  32182  fsumub  32980  sgnmulrp2  32988  rpxdivcld  33072  constrinvcl  34031  constrsqrtcl  34037  sqsscirc1  34166  cnre2csqlem  34168  tpr2rico  34170  xrmulc1cn  34188  xrge0iifiso  34193  xrge0iifhom  34195  esumcst  34321  esumdivc  34341  dya2icoseg  34535  omssubaddlem  34557  omssubadd  34558  probmeasb  34688  signsply0  34809  logdivsqrle  34908  hgt750leme  34916  dnicn  36894  unblimceq0lem  36908  unbdqndv2lem1  36911  unbdqndv2lem2  36912  knoppndvlem18  36931  knoppndvlem21  36934  poimirlem29  38112  heicant  38118  opnmbllem0  38119  mblfinlem3  38122  itg2addnclem3  38136  itg2addnc  38137  itggt0cn  38153  ftc1cnnclem  38154  ftc1anclem6  38161  ftc1anclem7  38162  geomcau  38222  sstotbnd2  38237  isbnd3  38247  equivbnd  38253  prdsbnd2  38258  cntotbnd  38259  heibor1lem  38272  heiborlem6  38279  bfplem1  38285  bfplem2  38286  bfp  38287  rrndstprj2  38294  rrnequiv  38298  lcmineqlem21  42630  aks4d1p1p4  42652  aks4d1p1p7  42655  aks4d1p5  42661  aks4d1p6  42662  aks6d1c2  42711  fltnlta  43209  irrapxlem4  43366  irrapxlem5  43367  irrapx1  43369  pell1qrgaplem  43414  pell14qrgapw  43417  pellqrexplicit  43418  pellqrex  43420  pellfundge  43423  pellfundgt1  43424  rmspecfund  43450  rmxycomplete  43458  rmxypos  43488  binomcxplemnotnn0  44896  suprltrp  45868  supxrge  45878  infrpge  45891  infleinflem1  45909  xralrple4  45912  recnnltrp  45916  rpgtrecnn  45919  cvgcaule  46029  fmul01lt1lem1  46124  fmul01lt1lem2  46125  ltmod  46176  lptre2pt  46178  addlimc  46186  0ellimcdiv  46187  limclner  46189  climleltrp  46214  climisp  46284  climxrrelem  46287  climxrre  46288  limsupgtlem  46315  liminfltlem  46342  cnrefiisplem  46367  climxlim2lem  46383  dvdivbd  46461  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  itgiccshift  46518  itgperiod  46519  stoweidlem1  46539  stoweidlem3  46541  stoweidlem5  46543  stoweidlem7  46545  stoweidlem11  46549  stoweidlem13  46551  stoweidlem14  46552  stoweidlem24  46562  stoweidlem25  46563  stoweidlem26  46564  stoweidlem34  46572  stoweidlem41  46579  stoweidlem42  46580  stoweidlem49  46587  stoweidlem51  46589  stoweidlem52  46590  stoweidlem59  46597  stoweidlem60  46598  stoweidlem62  46600  stoweid  46601  wallispilem5  46607  stirlinglem1  46612  stirlinglem4  46615  stirlinglem5  46616  stirlinglem6  46617  dirkercncflem1  46641  fourierdlem30  46675  fourierdlem39  46684  fourierdlem47  46691  fourierdlem73  46717  fourierdlem81  46725  fourierdlem87  46731  fourierdlem103  46747  fourierdlem104  46748  fourierdlem107  46751  rrndistlt  46828  qndenserrnbllem  46832  sge0ltfirp  46938  sge0rpcpnf  46959  sge0xaddlem1  46971  omeiunltfirp  47057  carageniuncllem2  47060  ovnsubaddlem1  47108  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  hoiqssbllem1  47160  hoiqssbllem2  47161  hoiqssbllem3  47162  hspmbllem2  47165  hspmbllem3  47166  ovolval5lem1  47190  ovolval5lem2  47191  iinhoiicc  47212  vonioolem1  47218  pimrecltpos  47246  smflimlem3  47311  smfmullem1  47329  smfmullem2  47330  smfmullem3  47331  modexp2m1d  48185  dignn0flhalflem1  49201  itsclc0yqsol  49350  amgmwlem  50387  amgmw2d  50389  young2d  50390