Theorem rpred 12986

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-rp 12943

This theorem is referenced by:  rpxrd  12987  rpcnd  12988  rpregt0d  12992  rprege0d  12993  rprene0d  12994  rprecred  12997  ltmulgt11d  13021  ltmulgt12d  13022  gt0divd  13023  ge0divd  13024  lediv12ad  13045  prodge0rd  13051  xlemul1  13242  xov1plusxeqvd  13451  ltexp2a  14128  rpexpmord  14130  expcan  14131  ltexp2  14132  leexp2a  14134  expnlbnd2  14196  expmulnbnd  14197  exp11nnd  14223  01sqrexlem6  15209  cau3lem  15317  rlimcld2  15540  addcn2  15556  mulcn2  15558  reccn2  15559  o1rlimmul  15581  rlimno1  15616  caucvgrlem  15635  isumrpcl  15808  isumltss  15813  expcnv  15829  mertenslem1  15849  effsumlt  16078  recoshcl  16125  eirrlem  16171  rpnnen2lem11  16191  bitsmod  16405  prmreclem3  16889  prmreclem5  16891  4sqlem7  16915  ssblex  24393  metss2lem  24476  methaus  24485  met1stc  24486  met2ndci  24487  metustto  24518  metustexhalf  24521  nlmvscnlem2  24650  nlmvscnlem1  24651  nrginvrcnlem  24656  nmoi2  24695  nghmcn  24710  reperflem  24784  iccntr  24787  icccmplem2  24789  reconnlem2  24793  opnreen  24797  metdcnlem  24802  metnrmlem3  24827  addcnlem  24830  cnheibor  24922  cnllycmp  24923  lebnumlem3  24930  lebnumii  24933  nmoleub2lem  25081  nmoleub2lem3  25082  nmoleub2lem2  25083  nmoleub3  25086  nmhmcn  25087  ipcnlem2  25211  ipcnlem1  25212  lmnn  25230  iscfil3  25240  cfilfcls  25241  iscmet3lem1  25258  iscmet3lem2  25259  bcthlem4  25294  bcthlem5  25295  minveclem3b  25395  minveclem3  25396  ivthlem2  25419  ovolgelb  25447  ovollb2lem  25455  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliunlem2  25470  ovolscalem1  25480  ioombl1lem2  25526  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  opnmbllem  25568  volcn  25573  vitalilem4  25578  itg2mulclem  25713  itg2monolem3  25719  itg2cnlem2  25729  itg2cn  25730  itggt0  25811  dveflem  25946  dvferm1lem  25951  dvferm2lem  25953  lhop1lem  25980  lhop1  25981  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvfsumrlim  25998  ftc1a  26004  ftc1lem4  26006  plyeq0lem  26175  aalioulem2  26299  aalioulem4  26301  aalioulem5  26302  aalioulem6  26303  aaliou  26304  aaliou2b  26307  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem8  26311  aaliou3lem5  26313  aaliou3lem7  26315  aaliou3lem9  26316  ulmcn  26364  ulmdvlem1  26365  mtest  26369  itgulm  26373  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  abelthlem7  26403  pilem2  26417  divlogrlim  26599  logcnlem3  26608  logcnlem4  26609  logccv  26627  divcxp  26651  cxplt  26658  cxple2  26661  recxpf1lem  26693  cxpcn3lem  26711  cxpaddlelem  26715  cxpaddle  26716  loglesqrt  26725  leibpi  26906  rlimcnp3  26931  cxplim  26935  rlimcxp  26937  cxp2limlem  26939  cxp2lim  26940  cxploglim  26941  cxploglim2  26942  divsqrtsumlem  26943  jensenlem2  26951  logdifbnd  26957  emcllem4  26962  harmonicbnd4  26974  fsumharmonic  26975  zetacvg  26978  lgamgulmlem2  26993  lgamgulmlem5  26996  lgamucov  27001  regamcl  27024  relgamcl  27025  ftalem1  27036  ftalem2  27037  ftalem3  27038  ftalem5  27040  basellem1  27044  basellem3  27046  basellem4  27047  basellem8  27051  chtwordi  27119  chpchtsum  27182  logfacrlim  27187  logexprlim  27188  bclbnd  27243  efexple  27244  bposlem1  27247  bposlem2  27248  bposlem6  27252  bposlem7  27253  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chpo1ubb  27444  rplogsumlem1  27447  rplogsumlem2  27448  dchrisum0lem1a  27449  rpvmasumlem  27450  dchrisumlem2  27453  dchrisumlem3  27454  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasumlema  27463  dchrvmasumiflem1  27464  dchrisum0fno1  27474  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2  27481  dchrisum0lem3  27482  dchrisum0  27483  mulogsumlem  27494  logdivsum  27496  mulog2sumlem2  27498  vmalogdivsum2  27501  2vmadivsumlem  27503  log2sumbnd  27507  selberglem2  27509  selberg  27511  selberg2lem  27513  chpdifbndlem1  27516  chpdifbndlem2  27517  selberg3lem1  27520  selberg4lem1  27523  pntrsumbnd2  27530  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem5  27544  pntrlog2bndlem6a  27545  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem1  27552  pntibndlem2  27554  pntibndlem3  27555  pntibnd  27556  pntlemc  27558  pntlema  27559  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemn  27563  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemi  27567  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntleme  27571  pntlem3  27572  pntlemp  27573  pntleml  27574  ostth2lem1  27581  ostth2lem3  27598  ostth2  27600  ostth3  27601  crctcshwlkn0lem5  29882  nrt2irr  30543  smcnlem  30768  blocnilem  30875  blocni  30876  ubthlem2  30942  minvecolem3  30947  minvecolem4  30951  minvecolem5  30952  nmcexi  32097  lnconi  32104  fsumub  32901  sgnmulrp2  32909  rpxdivcld  32993  constrinvcl  33917  constrsqrtcl  33923  sqsscirc1  34052  cnre2csqlem  34054  tpr2rico  34056  xrmulc1cn  34074  xrge0iifiso  34079  xrge0iifhom  34081  esumcst  34207  esumdivc  34227  dya2icoseg  34421  omssubaddlem  34443  omssubadd  34444  probmeasb  34574  signsply0  34695  logdivsqrle  34794  hgt750leme  34802  dnicn  36752  unblimceq0lem  36766  unbdqndv2lem1  36769  unbdqndv2lem2  36770  knoppndvlem18  36789  knoppndvlem21  36792  poimirlem29  37970  heicant  37976  opnmbllem0  37977  mblfinlem3  37980  itg2addnclem3  37994  itg2addnc  37995  itggt0cn  38011  ftc1cnnclem  38012  ftc1anclem6  38019  ftc1anclem7  38020  geomcau  38080  sstotbnd2  38095  isbnd3  38105  equivbnd  38111  prdsbnd2  38116  cntotbnd  38117  heibor1lem  38130  heiborlem6  38137  bfplem1  38143  bfplem2  38144  bfp  38145  rrndstprj2  38152  rrnequiv  38156  lcmineqlem21  42488  aks4d1p1p4  42510  aks4d1p1p7  42513  aks4d1p5  42519  aks4d1p6  42520  aks6d1c2  42569  fltnlta  43096  irrapxlem4  43253  irrapxlem5  43254  irrapx1  43256  pell1qrgaplem  43301  pell14qrgapw  43304  pellqrexplicit  43305  pellqrex  43307  pellfundge  43310  pellfundgt1  43311  rmspecfund  43337  rmxycomplete  43345  rmxypos  43375  binomcxplemnotnn0  44783  suprltrp  45758  supxrge  45768  infrpge  45781  infleinflem1  45799  xralrple4  45802  recnnltrp  45806  rpgtrecnn  45809  cvgcaule  45919  fmul01lt1lem1  46014  fmul01lt1lem2  46015  ltmod  46066  lptre2pt  46068  addlimc  46076  0ellimcdiv  46077  limclner  46079  climleltrp  46104  climisp  46174  climxrrelem  46177  climxrre  46178  limsupgtlem  46205  liminfltlem  46232  cnrefiisplem  46257  climxlim2lem  46273  dvdivbd  46351  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  itgiccshift  46408  itgperiod  46409  stoweidlem1  46429  stoweidlem3  46431  stoweidlem5  46433  stoweidlem7  46435  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem24  46452  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem41  46469  stoweidlem42  46470  stoweidlem49  46477  stoweidlem51  46479  stoweidlem52  46480  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  stoweid  46491  wallispilem5  46497  stirlinglem1  46502  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  dirkercncflem1  46531  fourierdlem30  46565  fourierdlem39  46574  fourierdlem47  46581  fourierdlem73  46607  fourierdlem81  46615  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  rrndistlt  46718  qndenserrnbllem  46722  sge0ltfirp  46828  sge0rpcpnf  46849  sge0xaddlem1  46861  omeiunltfirp  46947  carageniuncllem2  46950  ovnsubaddlem1  46998  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoiqssbllem1  47050  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem2  47055  hspmbllem3  47056  ovolval5lem1  47080  ovolval5lem2  47081  iinhoiicc  47102  vonioolem1  47108  pimrecltpos  47136  smflimlem3  47201  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  modexp2m1d  48075  dignn0flhalflem1  49091  itsclc0yqsol  49240  amgmwlem  50277  amgmw2d  50279  young2d  50280