Theorem rpred 13078

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  ℝ⁺crp 13034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925  df-rp 13035

This theorem is used by:  rpxrd  13079  rpcnd  13080  rpregt0d  13084  rprege0d  13085  rprene0d  13086  rprecred  13089  ltmulgt11d  13113  ltmulgt12d  13114  gt0divd  13115  ge0divd  13116  lediv12ad  13137  prodge0rd  13143  xlemul1  13334  xov1plusxeqvd  13543  ltexp2a  14222  rpexpmord  14224  expcan  14225  ltexp2  14226  leexp2a  14228  expnlbnd2  14290  expmulnbnd  14291  exp11nnd  14317  sgnmulrp2  15171  01sqrexlem6  15324  cau3lem  15432  rlimcld2  15655  addcn2  15671  mulcn2  15673  reccn2  15674  o1rlimmul  15696  rlimno1  15731  caucvgrlem  15750  isumrpcl  15923  isumltss  15928  expcnv  15944  mertenslem1  15964  effsumlt  16192  recoshcl  16239  eirrlem  16285  rpnnen2lem11  16305  bitsmod  16519  prmreclem3  17003  prmreclem5  17005  4sqlem7  17029  ssblex  24622  metss2lem  24705  methaus  24714  met1stc  24715  met2ndci  24716  metustto  24747  metustexhalf  24750  nlmvscnlem2  24879  nlmvscnlem1  24880  nrginvrcnlem  24885  nmoi2  24924  nghmcn  24939  reperflem  25013  iccntr  25016  icccmplem2  25018  reconnlem2  25022  opnreen  25026  metdcnlem  25031  metnrmlem3  25056  addcnlem  25059  cnheibor  25151  cnllycmp  25152  lebnumlem3  25159  lebnumii  25162  nmoleub2lem  25310  nmoleub2lem3  25311  nmoleub2lem2  25312  nmoleub3  25315  nmhmcn  25316  ipcnlem2  25440  ipcnlem1  25441  lmnn  25459  iscfil3  25469  cfilfcls  25470  iscmet3lem1  25487  iscmet3lem2  25488  bcthlem4  25523  bcthlem5  25524  minveclem3b  25624  minveclem3  25625  ivthlem2  25648  ovolgelb  25676  ovollb2lem  25684  ovolunlem1a  25692  ovolunlem1  25693  ovoliunlem1  25698  ovoliunlem2  25699  ovolscalem1  25709  ioombl1lem2  25755  ioombl1lem4  25757  uniioombllem1  25777  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  opnmbllem  25797  volcn  25802  vitalilem4  25807  itg2mulclem  25942  itg2monolem3  25948  itg2cnlem2  25958  itg2cn  25959  itggt0  26040  dveflem  26175  dvferm1lem  26180  dvferm2lem  26182  lhop1lem  26209  lhop1  26210  lhop  26212  dvcnvrelem1  26213  dvcnvrelem2  26214  dvcnvre  26215  dvfsumrlim  26227  ftc1a  26233  ftc1lem4  26235  plyeq0lem  26404  aalioulem2  26533  aalioulem4  26535  aalioulem5  26536  aalioulem6  26537  aaliou  26538  aaliou2b  26541  aaliou3lem1  26542  aaliou3lem2  26543  aaliou3lem8  26545  aaliou3lem5  26547  aaliou3lem7  26549  aaliou3lem9  26550  ulmcn  26599  ulmdvlem1  26600  mtest  26604  itgulm  26608  psercn  26626  pserdvlem1  26627  pserdvlem2  26628  pserdv  26629  abelthlem7  26638  pilem2  26652  divlogrlim  26837  logcnlem3  26846  logcnlem4  26847  logccv  26865  divcxp  26889  cxplt  26896  cxple2  26899  recxpf1lem  26931  cxpcn3lem  26949  cxpaddlelem  26953  cxpaddle  26954  loglesqrt  26963  leibpi  27144  rlimcnp3  27169  cxplim  27173  rlimcxp  27175  cxp2limlem  27177  cxp2lim  27178  cxploglim  27179  cxploglim2  27180  divsqrtsumlem  27181  jensenlem2  27189  logdifbnd  27195  emcllem4  27200  harmonicbnd4  27212  fsumharmonic  27213  zetacvg  27216  lgamgulmlem2  27231  lgamgulmlem5  27234  lgamucov  27239  regamcl  27262  relgamcl  27263  ftalem1  27274  ftalem2  27275  ftalem3  27276  ftalem5  27278  basellem1  27282  basellem3  27284  basellem4  27285  basellem8  27289  chtwordi  27357  chpchtsum  27420  logfacrlim  27425  logexprlim  27426  bclbnd  27481  efexple  27482  bposlem1  27485  bposlem2  27486  bposlem6  27490  bposlem7  27491  chebbnd1lem3  27672  chebbnd1  27673  chtppilimlem1  27674  chtppilimlem2  27675  chpo1ubb  27682  rplogsumlem1  27685  rplogsumlem2  27686  dchrisum0lem1a  27687  rpvmasumlem  27688  dchrisumlem2  27691  dchrisumlem3  27692  dchrmusumlema  27694  dchrmusum2  27695  dchrvmasumlem1  27696  dchrvmasum2lem  27697  dchrvmasumlema  27701  dchrvmasumiflem1  27702  dchrisum0fno1  27712  dchrisum0lem1b  27716  dchrisum0lem1  27717  dchrisum0lem2  27719  dchrisum0lem3  27720  dchrisum0  27721  mulogsumlem  27732  logdivsum  27734  mulog2sumlem2  27736  vmalogdivsum2  27739  2vmadivsumlem  27741  log2sumbnd  27745  selberglem2  27747  selberg  27749  selberg2lem  27751  chpdifbndlem1  27754  chpdifbndlem2  27755  selberg3lem1  27758  selberg4lem1  27761  pntrsumbnd2  27768  pntrlog2bndlem2  27779  pntrlog2bndlem3  27780  pntrlog2bndlem5  27782  pntrlog2bndlem6a  27783  pntrlog2bndlem6  27784  pntrlog2bnd  27785  pntpbnd1a  27786  pntpbnd1  27787  pntpbnd2  27788  pntibndlem1  27790  pntibndlem2  27792  pntibndlem3  27793  pntibnd  27794  pntlemc  27796  pntlema  27797  pntlemb  27798  pntlemg  27799  pntlemh  27800  pntlemn  27801  pntlemq  27802  pntlemr  27803  pntlemj  27804  pntlemi  27805  pntlemf  27806  pntlemk  27807  pntlemo  27808  pntleme  27809  pntlem3  27810  pntlemp  27811  pntleml  27812  ostth2lem1  27819  ostth2lem3  27836  ostth2  27838  ostth3  27839  crctcshwlkn0lem5  30200  nrt2irr  30861  smcnlem  31086  blocnilem  31193  blocni  31194  ubthlem2  31260  minvecolem3  31265  minvecolem4  31269  minvecolem5  31270  nmcexi  32415  lnconi  32422  fsumub  33209  rpxdivcld  33290  constrinvcl  34194  constrsqrtcl  34200  sqsscirc1  34329  cnre2csqlem  34331  tpr2rico  34333  xrmulc1cn  34351  xrge0iifiso  34356  xrge0iifhom  34358  esumcst  34484  esumdivc  34504  dya2icoseg  34699  omssubaddlem  34721  omssubadd  34722  probmeasb  34852  signsply0  34970  logdivsqrle  35069  hgt750leme  35077  dnicn  37122  unblimceq0lem  37136  unbdqndv2lem1  37139  unbdqndv2lem2  37140  knoppndvlem18  37159  knoppndvlem21  37162  poimirlem29  38341  heicant  38347  opnmbllem0  38348  mblfinlem3  38351  itg2addnclem3  38365  itg2addnc  38366  itggt0cn  38382  ftc1cnnclem  38383  ftc1anclem6  38390  ftc1anclem7  38391  geomcau  38451  sstotbnd2  38466  isbnd3  38476  equivbnd  38482  prdsbnd2  38487  cntotbnd  38488  heibor1lem  38501  heiborlem6  38508  bfplem1  38514  bfplem2  38515  bfp  38516  rrndstprj2  38523  rrnequiv  38527  lcmineqlem21  42857  aks4d1p1p4  42879  aks4d1p1p7  42882  aks4d1p5  42888  aks4d1p6  42889  aks6d1c2  42938  fltnlta  43436  irrapxlem4  43593  irrapxlem5  43594  irrapx1  43596  pell1qrgaplem  43641  pell14qrgapw  43644  pellqrexplicit  43645  pellqrex  43647  pellfundge  43650  pellfundgt1  43651  rmspecfund  43677  rmxycomplete  43685  rmxypos  43715  binomcxplemnotnn0  45107  suprltrp  46085  supxrge  46095  infrpge  46108  infleinflem1  46126  xralrple4  46129  recnnltrp  46133  rpgtrecnn  46136  cvgcaule  46246  fmul01lt1lem1  46341  fmul01lt1lem2  46342  ltmod  46393  lptre2pt  46395  addlimc  46403  0ellimcdiv  46404  limclner  46406  climleltrp  46431  climisp  46501  climxrrelem  46504  climxrre  46505  limsupgtlem  46532  liminfltlem  46559  cnrefiisplem  46584  climxlim2lem  46600  dvdivbd  46678  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  itgiccshift  46735  itgperiod  46736  stoweidlem1  46756  stoweidlem3  46758  stoweidlem5  46760  stoweidlem7  46762  stoweidlem11  46766  stoweidlem13  46768  stoweidlem14  46769  stoweidlem24  46779  stoweidlem25  46780  stoweidlem26  46781  stoweidlem34  46789  stoweidlem41  46796  stoweidlem42  46797  stoweidlem49  46804  stoweidlem51  46806  stoweidlem52  46807  stoweidlem59  46814  stoweidlem60  46815  stoweidlem62  46817  stoweid  46818  wallispilem5  46824  stirlinglem1  46829  stirlinglem4  46832  stirlinglem5  46833  stirlinglem6  46834  dirkercncflem1  46858  fourierdlem30  46892  fourierdlem39  46901  fourierdlem47  46908  fourierdlem73  46934  fourierdlem81  46942  fourierdlem87  46948  fourierdlem103  46964  fourierdlem104  46965  fourierdlem107  46968  rrndistlt  47045  qndenserrnbllem  47049  sge0ltfirp  47155  sge0rpcpnf  47176  sge0xaddlem1  47188  omeiunltfirp  47274  carageniuncllem2  47277  ovnsubaddlem1  47325  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  hoiqssbllem1  47377  hoiqssbllem2  47378  hoiqssbllem3  47379  hspmbllem2  47382  hspmbllem3  47383  ovolval5lem1  47407  ovolval5lem2  47408  iinhoiicc  47429  vonioolem1  47435  pimrecltpos  47463  smflimlem3  47528  smfmullem1  47546  smfmullem2  47547  smfmullem3  47548  modexp2m1d  48405  dignn0flhalflem1  49436  itsclc0yqsol  49585  amgmwlem  50691  amgmw2d  50693  young2d  50694