Theorem rpred 13064

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℝcr 11148  ℝ⁺crp 13022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-ss 3963  df-rp 13023

This theorem is referenced by:  rpxrd  13065  rpcnd  13066  rpregt0d  13070  rprege0d  13071  rprene0d  13072  rprecred  13075  ltmulgt11d  13099  ltmulgt12d  13100  gt0divd  13101  ge0divd  13102  lediv12ad  13123  prodge0rd  13129  xlemul1  13317  xov1plusxeqvd  13523  ltexp2a  14179  rpexpmord  14181  expcan  14182  ltexp2  14183  leexp2a  14185  expnlbnd2  14246  expmulnbnd  14247  exp11nnd  14273  01sqrexlem6  15247  cau3lem  15354  rlimcld2  15575  addcn2  15591  mulcn2  15593  reccn2  15594  o1rlimmul  15616  rlimno1  15653  caucvgrlem  15672  isumrpcl  15842  isumltss  15847  expcnv  15863  mertenslem1  15883  effsumlt  16108  recoshcl  16155  eirrlem  16201  rpnnen2lem11  16221  bitsmod  16431  prmreclem3  16915  prmreclem5  16917  4sqlem7  16941  ssblex  24422  metss2lem  24508  methaus  24517  met1stc  24518  met2ndci  24519  metustto  24550  metustexhalf  24553  nlmvscnlem2  24690  nlmvscnlem1  24691  nrginvrcnlem  24696  nmoi2  24735  nghmcn  24750  reperflem  24822  iccntr  24825  icccmplem2  24827  reconnlem2  24831  opnreen  24835  metdcnlem  24840  metnrmlem3  24865  addcnlem  24868  cnheibor  24969  cnllycmp  24970  lebnumlem3  24977  lebnumii  24980  nmoleub2lem  25129  nmoleub2lem3  25130  nmoleub2lem2  25131  nmoleub3  25134  nmhmcn  25135  ipcnlem2  25260  ipcnlem1  25261  lmnn  25279  iscfil3  25289  cfilfcls  25290  iscmet3lem1  25307  iscmet3lem2  25308  bcthlem4  25343  bcthlem5  25344  minveclem3b  25444  minveclem3  25445  ivthlem2  25469  ovolgelb  25497  ovollb2lem  25505  ovolunlem1a  25513  ovolunlem1  25514  ovoliunlem1  25519  ovoliunlem2  25520  ovolscalem1  25530  ioombl1lem2  25576  ioombl1lem4  25578  uniioombllem1  25598  uniioombllem3  25602  uniioombllem4  25603  uniioombllem5  25604  opnmbllem  25618  volcn  25623  vitalilem4  25628  itg2mulclem  25764  itg2monolem3  25770  itg2cnlem2  25780  itg2cn  25781  itggt0  25861  dveflem  25999  dvferm1lem  26004  dvferm2lem  26006  lhop1lem  26034  lhop1  26035  lhop  26037  dvcnvrelem1  26038  dvcnvrelem2  26039  dvcnvre  26040  dvfsumrlim  26054  ftc1a  26060  ftc1lem4  26062  plyeq0lem  26234  aalioulem2  26358  aalioulem4  26360  aalioulem5  26361  aalioulem6  26362  aaliou  26363  aaliou2b  26366  aaliou3lem1  26367  aaliou3lem2  26368  aaliou3lem8  26370  aaliou3lem5  26372  aaliou3lem7  26374  aaliou3lem9  26375  ulmcn  26425  ulmdvlem1  26426  mtest  26430  itgulm  26434  psercn  26453  pserdvlem1  26454  pserdvlem2  26455  pserdv  26456  abelthlem7  26465  pilem2  26479  divlogrlim  26659  logcnlem3  26668  logcnlem4  26669  logccv  26687  divcxp  26711  cxplt  26718  cxple2  26721  recxpf1lem  26753  cxpcn3lem  26772  cxpaddlelem  26776  cxpaddle  26777  loglesqrt  26786  leibpi  26967  rlimcnp3  26992  cxplim  26997  rlimcxp  26999  cxp2limlem  27001  cxp2lim  27002  cxploglim  27003  cxploglim2  27004  divsqrtsumlem  27005  jensenlem2  27013  logdifbnd  27019  emcllem4  27024  harmonicbnd4  27036  fsumharmonic  27037  zetacvg  27040  lgamgulmlem2  27055  lgamgulmlem5  27058  lgamucov  27063  regamcl  27086  relgamcl  27087  ftalem1  27098  ftalem2  27099  ftalem3  27100  ftalem5  27102  basellem1  27106  basellem3  27108  basellem4  27109  basellem8  27113  chtwordi  27181  chpchtsum  27245  logfacrlim  27250  logexprlim  27251  bclbnd  27306  efexple  27307  bposlem1  27310  bposlem2  27311  bposlem6  27315  bposlem7  27316  chebbnd1lem3  27497  chebbnd1  27498  chtppilimlem1  27499  chtppilimlem2  27500  chpo1ubb  27507  rplogsumlem1  27510  rplogsumlem2  27511  dchrisum0lem1a  27512  rpvmasumlem  27513  dchrisumlem2  27516  dchrisumlem3  27517  dchrmusumlema  27519  dchrmusum2  27520  dchrvmasumlem1  27521  dchrvmasum2lem  27522  dchrvmasumlema  27526  dchrvmasumiflem1  27527  dchrisum0fno1  27537  dchrisum0lem1b  27541  dchrisum0lem1  27542  dchrisum0lem2  27544  dchrisum0lem3  27545  dchrisum0  27546  mulogsumlem  27557  logdivsum  27559  mulog2sumlem2  27561  vmalogdivsum2  27564  2vmadivsumlem  27566  log2sumbnd  27570  selberglem2  27572  selberg  27574  selberg2lem  27576  chpdifbndlem1  27579  chpdifbndlem2  27580  selberg3lem1  27583  selberg4lem1  27586  pntrsumbnd2  27593  pntrlog2bndlem2  27604  pntrlog2bndlem3  27605  pntrlog2bndlem5  27607  pntrlog2bndlem6a  27608  pntrlog2bndlem6  27609  pntrlog2bnd  27610  pntpbnd1a  27611  pntpbnd1  27612  pntpbnd2  27613  pntibndlem1  27615  pntibndlem2  27617  pntibndlem3  27618  pntibnd  27619  pntlemc  27621  pntlema  27622  pntlemb  27623  pntlemg  27624  pntlemh  27625  pntlemn  27626  pntlemq  27627  pntlemr  27628  pntlemj  27629  pntlemi  27630  pntlemf  27631  pntlemk  27632  pntlemo  27633  pntleme  27634  pntlem3  27635  pntlemp  27636  pntleml  27637  ostth2lem1  27644  ostth2lem3  27661  ostth2  27663  ostth3  27664  crctcshwlkn0lem5  29745  nrt2irr  30403  smcnlem  30627  blocnilem  30734  blocni  30735  ubthlem2  30801  minvecolem3  30806  minvecolem4  30810  minvecolem5  30811  nmcexi  31956  lnconi  31963  fsumub  32732  rpxdivcld  32798  sqsscirc1  33736  cnre2csqlem  33738  tpr2rico  33740  xrmulc1cn  33758  xrge0iifiso  33763  xrge0iifhom  33765  esumcst  33909  esumdivc  33929  dya2icoseg  34124  omssubaddlem  34146  omssubadd  34147  probmeasb  34277  sgnmulrp2  34390  signsply0  34410  logdivsqrle  34509  hgt750leme  34517  dnicn  36208  unblimceq0lem  36222  unbdqndv2lem1  36225  unbdqndv2lem2  36226  knoppndvlem18  36245  knoppndvlem21  36248  poimirlem29  37363  heicant  37369  opnmbllem0  37370  mblfinlem3  37373  itg2addnclem3  37387  itg2addnc  37388  itggt0cn  37404  ftc1cnnclem  37405  ftc1anclem6  37412  ftc1anclem7  37413  geomcau  37473  sstotbnd2  37488  isbnd3  37498  equivbnd  37504  prdsbnd2  37509  cntotbnd  37510  heibor1lem  37523  heiborlem6  37530  bfplem1  37536  bfplem2  37537  bfp  37538  rrndstprj2  37545  rrnequiv  37549  lcmineqlem21  41761  aks4d1p1p4  41783  aks4d1p1p7  41786  aks4d1p5  41792  aks4d1p6  41793  aks6d1c2  41842  fltnlta  42353  irrapxlem4  42519  irrapxlem5  42520  irrapx1  42522  pell1qrgaplem  42567  pell14qrgapw  42570  pellqrexplicit  42571  pellqrex  42573  pellfundge  42576  pellfundgt1  42577  rmspecfund  42603  rmxycomplete  42612  rmxypos  42642  binomcxplemnotnn0  44067  suprltrp  44979  supxrge  44989  infrpge  45002  infleinflem1  45021  xralrple4  45024  recnnltrp  45028  rpgtrecnn  45031  cvgcaule  45143  fmul01lt1lem1  45241  fmul01lt1lem2  45242  ltmod  45295  lptre2pt  45297  addlimc  45305  0ellimcdiv  45306  limclner  45308  climleltrp  45333  climisp  45403  climxrrelem  45406  climxrre  45407  limsupgtlem  45434  liminfltlem  45461  cnrefiisplem  45486  climxlim2lem  45502  dvdivbd  45580  ioodvbdlimc1lem2  45589  ioodvbdlimc2lem  45591  itgiccshift  45637  itgperiod  45638  stoweidlem1  45658  stoweidlem3  45660  stoweidlem5  45662  stoweidlem7  45664  stoweidlem11  45668  stoweidlem13  45670  stoweidlem14  45671  stoweidlem24  45681  stoweidlem25  45682  stoweidlem26  45683  stoweidlem34  45691  stoweidlem41  45698  stoweidlem42  45699  stoweidlem49  45706  stoweidlem51  45708  stoweidlem52  45709  stoweidlem59  45716  stoweidlem60  45717  stoweidlem62  45719  stoweid  45720  wallispilem5  45726  stirlinglem1  45731  stirlinglem4  45734  stirlinglem5  45735  stirlinglem6  45736  dirkercncflem1  45760  fourierdlem30  45794  fourierdlem39  45803  fourierdlem47  45810  fourierdlem73  45836  fourierdlem81  45844  fourierdlem87  45850  fourierdlem103  45866  fourierdlem104  45867  fourierdlem107  45870  rrndistlt  45947  qndenserrnbllem  45951  sge0ltfirp  46057  sge0rpcpnf  46078  sge0xaddlem1  46090  omeiunltfirp  46176  carageniuncllem2  46179  ovnsubaddlem1  46227  hoidmvlelem1  46252  hoidmvlelem2  46253  hoidmvlelem3  46254  hoidmvlelem4  46255  hoiqssbllem1  46279  hoiqssbllem2  46280  hoiqssbllem3  46281  hspmbllem2  46284  hspmbllem3  46285  ovolval5lem1  46309  ovolval5lem2  46310  iinhoiicc  46331  vonioolem1  46337  pimrecltpos  46365  smflimlem3  46430  smfmullem1  46448  smfmullem2  46449  smfmullem3  46450  modexp2m1d  47220  dignn0flhalflem1  48039  itsclc0yqsol  48188  amgmwlem  48586  amgmw2d  48588  young2d  48589