Theorem rpred 12961

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-rp 12918

This theorem is referenced by:  rpxrd  12962  rpcnd  12963  rpregt0d  12967  rprege0d  12968  rprene0d  12969  rprecred  12972  ltmulgt11d  12996  ltmulgt12d  12997  gt0divd  12998  ge0divd  12999  lediv12ad  13020  prodge0rd  13026  xlemul1  13217  xov1plusxeqvd  13426  ltexp2a  14101  rpexpmord  14103  expcan  14104  ltexp2  14105  leexp2a  14107  expnlbnd2  14169  expmulnbnd  14170  exp11nnd  14196  01sqrexlem6  15182  cau3lem  15290  rlimcld2  15513  addcn2  15529  mulcn2  15531  reccn2  15532  o1rlimmul  15554  rlimno1  15589  caucvgrlem  15608  isumrpcl  15778  isumltss  15783  expcnv  15799  mertenslem1  15819  effsumlt  16048  recoshcl  16095  eirrlem  16141  rpnnen2lem11  16161  bitsmod  16375  prmreclem3  16858  prmreclem5  16860  4sqlem7  16884  ssblex  24384  metss2lem  24467  methaus  24476  met1stc  24477  met2ndci  24478  metustto  24509  metustexhalf  24512  nlmvscnlem2  24641  nlmvscnlem1  24642  nrginvrcnlem  24647  nmoi2  24686  nghmcn  24701  reperflem  24775  iccntr  24778  icccmplem2  24780  reconnlem2  24784  opnreen  24788  metdcnlem  24793  metnrmlem3  24818  addcnlem  24821  cnheibor  24922  cnllycmp  24923  lebnumlem3  24930  lebnumii  24933  nmoleub2lem  25082  nmoleub2lem3  25083  nmoleub2lem2  25084  nmoleub3  25087  nmhmcn  25088  ipcnlem2  25212  ipcnlem1  25213  lmnn  25231  iscfil3  25241  cfilfcls  25242  iscmet3lem1  25259  iscmet3lem2  25260  bcthlem4  25295  bcthlem5  25296  minveclem3b  25396  minveclem3  25397  ivthlem2  25421  ovolgelb  25449  ovollb2lem  25457  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliunlem2  25472  ovolscalem1  25482  ioombl1lem2  25528  ioombl1lem4  25530  uniioombllem1  25550  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  opnmbllem  25570  volcn  25575  vitalilem4  25580  itg2mulclem  25715  itg2monolem3  25721  itg2cnlem2  25731  itg2cn  25732  itggt0  25813  dveflem  25951  dvferm1lem  25956  dvferm2lem  25958  lhop1lem  25986  lhop1  25987  lhop  25989  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcnvre  25992  dvfsumrlim  26006  ftc1a  26012  ftc1lem4  26014  plyeq0lem  26183  aalioulem2  26309  aalioulem4  26311  aalioulem5  26312  aalioulem6  26313  aaliou  26314  aaliou2b  26317  aaliou3lem1  26318  aaliou3lem2  26319  aaliou3lem8  26321  aaliou3lem5  26323  aaliou3lem7  26325  aaliou3lem9  26326  ulmcn  26376  ulmdvlem1  26377  mtest  26381  itgulm  26385  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  abelthlem7  26416  pilem2  26430  divlogrlim  26612  logcnlem3  26621  logcnlem4  26622  logccv  26640  divcxp  26664  cxplt  26671  cxple2  26674  recxpf1lem  26706  cxpcn3lem  26725  cxpaddlelem  26729  cxpaddle  26730  loglesqrt  26739  leibpi  26920  rlimcnp3  26945  cxplim  26950  rlimcxp  26952  cxp2limlem  26954  cxp2lim  26955  cxploglim  26956  cxploglim2  26957  divsqrtsumlem  26958  jensenlem2  26966  logdifbnd  26972  emcllem4  26977  harmonicbnd4  26989  fsumharmonic  26990  zetacvg  26993  lgamgulmlem2  27008  lgamgulmlem5  27011  lgamucov  27016  regamcl  27039  relgamcl  27040  ftalem1  27051  ftalem2  27052  ftalem3  27053  ftalem5  27055  basellem1  27059  basellem3  27061  basellem4  27062  basellem8  27066  chtwordi  27134  chpchtsum  27198  logfacrlim  27203  logexprlim  27204  bclbnd  27259  efexple  27260  bposlem1  27263  bposlem2  27264  bposlem6  27268  bposlem7  27269  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chpo1ubb  27460  rplogsumlem1  27463  rplogsumlem2  27464  dchrisum0lem1a  27465  rpvmasumlem  27466  dchrisumlem2  27469  dchrisumlem3  27470  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasumlema  27479  dchrvmasumiflem1  27480  dchrisum0fno1  27490  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2  27497  dchrisum0lem3  27498  dchrisum0  27499  mulogsumlem  27510  logdivsum  27512  mulog2sumlem2  27514  vmalogdivsum2  27517  2vmadivsumlem  27519  log2sumbnd  27523  selberglem2  27525  selberg  27527  selberg2lem  27529  chpdifbndlem1  27532  chpdifbndlem2  27533  selberg3lem1  27536  selberg4lem1  27539  pntrsumbnd2  27546  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntrlog2bndlem6a  27561  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem1  27568  pntibndlem2  27570  pntibndlem3  27571  pntibnd  27572  pntlemc  27574  pntlema  27575  pntlemb  27576  pntlemg  27577  pntlemh  27578  pntlemn  27579  pntlemq  27580  pntlemr  27581  pntlemj  27582  pntlemi  27583  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntleme  27587  pntlem3  27588  pntlemp  27589  pntleml  27590  ostth2lem1  27597  ostth2lem3  27614  ostth2  27616  ostth3  27617  crctcshwlkn0lem5  29899  nrt2irr  30560  smcnlem  30784  blocnilem  30891  blocni  30892  ubthlem2  30958  minvecolem3  30963  minvecolem4  30967  minvecolem5  30968  nmcexi  32113  lnconi  32120  fsumub  32919  sgnmulrp2  32927  rpxdivcld  33025  constrinvcl  33950  constrsqrtcl  33956  sqsscirc1  34085  cnre2csqlem  34087  tpr2rico  34089  xrmulc1cn  34107  xrge0iifiso  34112  xrge0iifhom  34114  esumcst  34240  esumdivc  34260  dya2icoseg  34454  omssubaddlem  34476  omssubadd  34477  probmeasb  34607  signsply0  34728  logdivsqrle  34827  hgt750leme  34835  dnicn  36711  unblimceq0lem  36725  unbdqndv2lem1  36728  unbdqndv2lem2  36729  knoppndvlem18  36748  knoppndvlem21  36751  poimirlem29  37894  heicant  37900  opnmbllem0  37901  mblfinlem3  37904  itg2addnclem3  37918  itg2addnc  37919  itggt0cn  37935  ftc1cnnclem  37936  ftc1anclem6  37943  ftc1anclem7  37944  geomcau  38004  sstotbnd2  38019  isbnd3  38029  equivbnd  38035  prdsbnd2  38040  cntotbnd  38041  heibor1lem  38054  heiborlem6  38061  bfplem1  38067  bfplem2  38068  bfp  38069  rrndstprj2  38076  rrnequiv  38080  lcmineqlem21  42413  aks4d1p1p4  42435  aks4d1p1p7  42438  aks4d1p5  42444  aks4d1p6  42445  aks6d1c2  42494  fltnlta  43015  irrapxlem4  43176  irrapxlem5  43177  irrapx1  43179  pell1qrgaplem  43224  pell14qrgapw  43227  pellqrexplicit  43228  pellqrex  43230  pellfundge  43233  pellfundgt1  43234  rmspecfund  43260  rmxycomplete  43268  rmxypos  43298  binomcxplemnotnn0  44706  suprltrp  45681  supxrge  45691  infrpge  45704  infleinflem1  45722  xralrple4  45725  recnnltrp  45729  rpgtrecnn  45732  cvgcaule  45843  fmul01lt1lem1  45938  fmul01lt1lem2  45939  ltmod  45990  lptre2pt  45992  addlimc  46000  0ellimcdiv  46001  limclner  46003  climleltrp  46028  climisp  46098  climxrrelem  46101  climxrre  46102  limsupgtlem  46129  liminfltlem  46156  cnrefiisplem  46181  climxlim2lem  46197  dvdivbd  46275  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  itgiccshift  46332  itgperiod  46333  stoweidlem1  46353  stoweidlem3  46355  stoweidlem5  46357  stoweidlem7  46359  stoweidlem11  46363  stoweidlem13  46365  stoweidlem14  46366  stoweidlem24  46376  stoweidlem25  46377  stoweidlem26  46378  stoweidlem34  46386  stoweidlem41  46393  stoweidlem42  46394  stoweidlem49  46401  stoweidlem51  46403  stoweidlem52  46404  stoweidlem59  46411  stoweidlem60  46412  stoweidlem62  46414  stoweid  46415  wallispilem5  46421  stirlinglem1  46426  stirlinglem4  46429  stirlinglem5  46430  stirlinglem6  46431  dirkercncflem1  46455  fourierdlem30  46489  fourierdlem39  46498  fourierdlem47  46505  fourierdlem73  46531  fourierdlem81  46539  fourierdlem87  46545  fourierdlem103  46561  fourierdlem104  46562  fourierdlem107  46565  rrndistlt  46642  qndenserrnbllem  46646  sge0ltfirp  46752  sge0rpcpnf  46773  sge0xaddlem1  46785  omeiunltfirp  46871  carageniuncllem2  46874  ovnsubaddlem1  46922  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hoiqssbllem1  46974  hoiqssbllem2  46975  hoiqssbllem3  46976  hspmbllem2  46979  hspmbllem3  46980  ovolval5lem1  47004  ovolval5lem2  47005  iinhoiicc  47026  vonioolem1  47032  pimrecltpos  47060  smflimlem3  47125  smfmullem1  47143  smfmullem2  47144  smfmullem3  47145  modexp2m1d  47966  dignn0flhalflem1  48969  itsclc0yqsol  49118  amgmwlem  50155  amgmw2d  50157  young2d  50158