Theorem rpred 13013

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11106  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3955  df-ss 3965  df-rp 12972

This theorem is referenced by:  rpxrd  13014  rpcnd  13015  rpregt0d  13019  rprege0d  13020  rprene0d  13021  rprecred  13024  ltmulgt11d  13048  ltmulgt12d  13049  gt0divd  13050  ge0divd  13051  lediv12ad  13072  prodge0rd  13078  xlemul1  13266  xov1plusxeqvd  13472  ltexp2a  14128  rpexpmord  14130  expcan  14131  ltexp2  14132  leexp2a  14134  expnlbnd2  14194  expmulnbnd  14195  01sqrexlem6  15191  cau3lem  15298  rlimcld2  15519  addcn2  15535  mulcn2  15537  reccn2  15538  o1rlimmul  15560  rlimno1  15597  caucvgrlem  15616  isumrpcl  15786  isumltss  15791  expcnv  15807  mertenslem1  15827  effsumlt  16051  recoshcl  16098  eirrlem  16144  rpnnen2lem11  16164  bitsmod  16374  prmreclem3  16848  prmreclem5  16850  4sqlem7  16874  ssblex  23926  metss2lem  24012  methaus  24021  met1stc  24022  met2ndci  24023  metustto  24054  metustexhalf  24057  nlmvscnlem2  24194  nlmvscnlem1  24195  nrginvrcnlem  24200  nmoi2  24239  nghmcn  24254  reperflem  24326  iccntr  24329  icccmplem2  24331  reconnlem2  24335  opnreen  24339  metdcnlem  24344  metnrmlem3  24369  addcnlem  24372  cnheibor  24463  cnllycmp  24464  lebnumlem3  24471  lebnumii  24474  nmoleub2lem  24622  nmoleub2lem3  24623  nmoleub2lem2  24624  nmoleub3  24627  nmhmcn  24628  ipcnlem2  24753  ipcnlem1  24754  lmnn  24772  iscfil3  24782  cfilfcls  24783  iscmet3lem1  24800  iscmet3lem2  24801  bcthlem4  24836  bcthlem5  24837  minveclem3b  24937  minveclem3  24938  ivthlem2  24961  ovolgelb  24989  ovollb2lem  24997  ovolunlem1a  25005  ovolunlem1  25006  ovoliunlem1  25011  ovoliunlem2  25012  ovolscalem1  25022  ioombl1lem2  25068  ioombl1lem4  25070  uniioombllem1  25090  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  opnmbllem  25110  volcn  25115  vitalilem4  25120  itg2mulclem  25256  itg2monolem3  25262  itg2cnlem2  25272  itg2cn  25273  itggt0  25353  dveflem  25488  dvferm1lem  25493  dvferm2lem  25495  lhop1lem  25522  lhop1  25523  lhop  25525  dvcnvrelem1  25526  dvcnvrelem2  25527  dvcnvre  25528  dvfsumrlim  25540  ftc1a  25546  ftc1lem4  25548  plyeq0lem  25716  aalioulem2  25838  aalioulem4  25840  aalioulem5  25841  aalioulem6  25842  aaliou  25843  aaliou2b  25846  aaliou3lem1  25847  aaliou3lem2  25848  aaliou3lem8  25850  aaliou3lem5  25852  aaliou3lem7  25854  aaliou3lem9  25855  ulmcn  25903  ulmdvlem1  25904  mtest  25908  itgulm  25912  psercn  25930  pserdvlem1  25931  pserdvlem2  25932  pserdv  25933  abelthlem7  25942  pilem2  25956  divlogrlim  26135  logcnlem3  26144  logcnlem4  26145  logccv  26163  divcxp  26187  cxplt  26194  cxple2  26197  cxpcn3lem  26245  cxpaddlelem  26249  cxpaddle  26250  loglesqrt  26256  leibpi  26437  rlimcnp3  26462  cxplim  26466  rlimcxp  26468  cxp2limlem  26470  cxp2lim  26471  cxploglim  26472  cxploglim2  26473  divsqrtsumlem  26474  jensenlem2  26482  logdifbnd  26488  emcllem4  26493  harmonicbnd4  26505  fsumharmonic  26506  zetacvg  26509  lgamgulmlem2  26524  lgamgulmlem5  26527  lgamucov  26532  regamcl  26555  relgamcl  26556  ftalem1  26567  ftalem2  26568  ftalem3  26569  ftalem5  26571  basellem1  26575  basellem3  26577  basellem4  26578  basellem8  26582  chtwordi  26650  chpchtsum  26712  logfacrlim  26717  logexprlim  26718  bclbnd  26773  efexple  26774  bposlem1  26777  bposlem2  26778  bposlem6  26782  bposlem7  26783  chebbnd1lem3  26964  chebbnd1  26965  chtppilimlem1  26966  chtppilimlem2  26967  chpo1ubb  26974  rplogsumlem1  26977  rplogsumlem2  26978  dchrisum0lem1a  26979  rpvmasumlem  26980  dchrisumlem2  26983  dchrisumlem3  26984  dchrmusumlema  26986  dchrmusum2  26987  dchrvmasumlem1  26988  dchrvmasum2lem  26989  dchrvmasumlema  26993  dchrvmasumiflem1  26994  dchrisum0fno1  27004  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2  27011  dchrisum0lem3  27012  dchrisum0  27013  mulogsumlem  27024  logdivsum  27026  mulog2sumlem2  27028  vmalogdivsum2  27031  2vmadivsumlem  27033  log2sumbnd  27037  selberglem2  27039  selberg  27041  selberg2lem  27043  chpdifbndlem1  27046  chpdifbndlem2  27047  selberg3lem1  27050  selberg4lem1  27053  pntrsumbnd2  27060  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem5  27074  pntrlog2bndlem6a  27075  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntibndlem1  27082  pntibndlem2  27084  pntibndlem3  27085  pntibnd  27086  pntlemc  27088  pntlema  27089  pntlemb  27090  pntlemg  27091  pntlemh  27092  pntlemn  27093  pntlemq  27094  pntlemr  27095  pntlemj  27096  pntlemi  27097  pntlemf  27098  pntlemk  27099  pntlemo  27100  pntleme  27101  pntlem3  27102  pntlemp  27103  pntleml  27104  ostth2lem1  27111  ostth2lem3  27128  ostth2  27130  ostth3  27131  crctcshwlkn0lem5  29058  smcnlem  29938  blocnilem  30045  blocni  30046  ubthlem2  30112  minvecolem3  30117  minvecolem4  30121  minvecolem5  30122  nmcexi  31267  lnconi  31274  fsumub  32022  rpxdivcld  32088  sqsscirc1  32877  cnre2csqlem  32879  tpr2rico  32881  xrmulc1cn  32899  xrge0iifiso  32904  xrge0iifhom  32906  esumcst  33050  esumdivc  33070  dya2icoseg  33265  omssubaddlem  33287  omssubadd  33288  probmeasb  33418  sgnmulrp2  33531  signsply0  33551  logdivsqrle  33651  hgt750leme  33659  dnicn  35357  unblimceq0lem  35371  unbdqndv2lem1  35374  unbdqndv2lem2  35375  knoppndvlem18  35394  knoppndvlem21  35397  poimirlem29  36506  heicant  36512  opnmbllem0  36513  mblfinlem3  36516  itg2addnclem3  36530  itg2addnc  36531  itggt0cn  36547  ftc1cnnclem  36548  ftc1anclem6  36555  ftc1anclem7  36556  geomcau  36616  sstotbnd2  36631  isbnd3  36641  equivbnd  36647  prdsbnd2  36652  cntotbnd  36653  heibor1lem  36666  heiborlem6  36673  bfplem1  36679  bfplem2  36680  bfp  36681  rrndstprj2  36688  rrnequiv  36692  lcmineqlem21  40903  aks4d1p1p4  40925  aks4d1p1p7  40928  aks4d1p5  40934  aks4d1p6  40935  exp11nnd  41211  fltnlta  41402  irrapxlem4  41549  irrapxlem5  41550  irrapx1  41552  pell1qrgaplem  41597  pell14qrgapw  41600  pellqrexplicit  41601  pellqrex  41603  pellfundge  41606  pellfundgt1  41607  rmspecfund  41633  rmxycomplete  41642  rmxypos  41672  binomcxplemnotnn0  43101  suprltrp  44025  supxrge  44035  infrpge  44048  infleinflem1  44067  xralrple4  44070  recnnltrp  44074  rpgtrecnn  44077  cvgcaule  44189  fmul01lt1lem1  44287  fmul01lt1lem2  44288  ltmod  44341  lptre2pt  44343  addlimc  44351  0ellimcdiv  44352  limclner  44354  climleltrp  44379  climisp  44449  climxrrelem  44452  climxrre  44453  limsupgtlem  44480  liminfltlem  44507  cnrefiisplem  44532  climxlim2lem  44548  dvdivbd  44626  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  itgiccshift  44683  itgperiod  44684  stoweidlem1  44704  stoweidlem3  44706  stoweidlem5  44708  stoweidlem7  44710  stoweidlem11  44714  stoweidlem13  44716  stoweidlem14  44717  stoweidlem24  44727  stoweidlem25  44728  stoweidlem26  44729  stoweidlem34  44737  stoweidlem41  44744  stoweidlem42  44745  stoweidlem49  44752  stoweidlem51  44754  stoweidlem52  44755  stoweidlem59  44762  stoweidlem60  44763  stoweidlem62  44765  stoweid  44766  wallispilem5  44772  stirlinglem1  44777  stirlinglem4  44780  stirlinglem5  44781  stirlinglem6  44782  dirkercncflem1  44806  fourierdlem30  44840  fourierdlem39  44849  fourierdlem47  44856  fourierdlem73  44882  fourierdlem81  44890  fourierdlem87  44896  fourierdlem103  44912  fourierdlem104  44913  fourierdlem107  44916  rrndistlt  44993  qndenserrnbllem  44997  sge0ltfirp  45103  sge0rpcpnf  45124  sge0xaddlem1  45136  omeiunltfirp  45222  carageniuncllem2  45225  ovnsubaddlem1  45273  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  hoiqssbllem1  45325  hoiqssbllem2  45326  hoiqssbllem3  45327  hspmbllem2  45330  hspmbllem3  45331  ovolval5lem1  45355  ovolval5lem2  45356  iinhoiicc  45377  vonioolem1  45383  pimrecltpos  45411  smflimlem3  45476  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  modexp2m1d  46267  dignn0flhalflem1  47255  itsclc0yqsol  47404  amgmwlem  47803  amgmw2d  47805  young2d  47806