Theorem rpred 13023

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11115  ℝ⁺crp 12981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-in 3955  df-ss 3965  df-rp 12982

This theorem is referenced by:  rpxrd  13024  rpcnd  13025  rpregt0d  13029  rprege0d  13030  rprene0d  13031  rprecred  13034  ltmulgt11d  13058  ltmulgt12d  13059  gt0divd  13060  ge0divd  13061  lediv12ad  13082  prodge0rd  13088  xlemul1  13276  xov1plusxeqvd  13482  ltexp2a  14138  rpexpmord  14140  expcan  14141  ltexp2  14142  leexp2a  14144  expnlbnd2  14204  expmulnbnd  14205  01sqrexlem6  15201  cau3lem  15308  rlimcld2  15529  addcn2  15545  mulcn2  15547  reccn2  15548  o1rlimmul  15570  rlimno1  15607  caucvgrlem  15626  isumrpcl  15796  isumltss  15801  expcnv  15817  mertenslem1  15837  effsumlt  16061  recoshcl  16108  eirrlem  16154  rpnnen2lem11  16174  bitsmod  16384  prmreclem3  16858  prmreclem5  16860  4sqlem7  16884  ssblex  24254  metss2lem  24340  methaus  24349  met1stc  24350  met2ndci  24351  metustto  24382  metustexhalf  24385  nlmvscnlem2  24522  nlmvscnlem1  24523  nrginvrcnlem  24528  nmoi2  24567  nghmcn  24582  reperflem  24654  iccntr  24657  icccmplem2  24659  reconnlem2  24663  opnreen  24667  metdcnlem  24672  metnrmlem3  24697  addcnlem  24700  cnheibor  24801  cnllycmp  24802  lebnumlem3  24809  lebnumii  24812  nmoleub2lem  24961  nmoleub2lem3  24962  nmoleub2lem2  24963  nmoleub3  24966  nmhmcn  24967  ipcnlem2  25092  ipcnlem1  25093  lmnn  25111  iscfil3  25121  cfilfcls  25122  iscmet3lem1  25139  iscmet3lem2  25140  bcthlem4  25175  bcthlem5  25176  minveclem3b  25276  minveclem3  25277  ivthlem2  25301  ovolgelb  25329  ovollb2lem  25337  ovolunlem1a  25345  ovolunlem1  25346  ovoliunlem1  25351  ovoliunlem2  25352  ovolscalem1  25362  ioombl1lem2  25408  ioombl1lem4  25410  uniioombllem1  25430  uniioombllem3  25434  uniioombllem4  25435  uniioombllem5  25436  opnmbllem  25450  volcn  25455  vitalilem4  25460  itg2mulclem  25596  itg2monolem3  25602  itg2cnlem2  25612  itg2cn  25613  itggt0  25693  dveflem  25831  dvferm1lem  25836  dvferm2lem  25838  lhop1lem  25866  lhop1  25867  lhop  25869  dvcnvrelem1  25870  dvcnvrelem2  25871  dvcnvre  25872  dvfsumrlim  25886  ftc1a  25892  ftc1lem4  25894  plyeq0lem  26062  aalioulem2  26185  aalioulem4  26187  aalioulem5  26188  aalioulem6  26189  aaliou  26190  aaliou2b  26193  aaliou3lem1  26194  aaliou3lem2  26195  aaliou3lem8  26197  aaliou3lem5  26199  aaliou3lem7  26201  aaliou3lem9  26202  ulmcn  26250  ulmdvlem1  26251  mtest  26255  itgulm  26259  psercn  26278  pserdvlem1  26279  pserdvlem2  26280  pserdv  26281  abelthlem7  26290  pilem2  26304  divlogrlim  26483  logcnlem3  26492  logcnlem4  26493  logccv  26511  divcxp  26535  cxplt  26542  cxple2  26545  recxpf1lem  26577  cxpcn3lem  26596  cxpaddlelem  26600  cxpaddle  26601  loglesqrt  26607  leibpi  26788  rlimcnp3  26813  cxplim  26817  rlimcxp  26819  cxp2limlem  26821  cxp2lim  26822  cxploglim  26823  cxploglim2  26824  divsqrtsumlem  26825  jensenlem2  26833  logdifbnd  26839  emcllem4  26844  harmonicbnd4  26856  fsumharmonic  26857  zetacvg  26860  lgamgulmlem2  26875  lgamgulmlem5  26878  lgamucov  26883  regamcl  26906  relgamcl  26907  ftalem1  26918  ftalem2  26919  ftalem3  26920  ftalem5  26922  basellem1  26926  basellem3  26928  basellem4  26929  basellem8  26933  chtwordi  27001  chpchtsum  27065  logfacrlim  27070  logexprlim  27071  bclbnd  27126  efexple  27127  bposlem1  27130  bposlem2  27131  bposlem6  27135  bposlem7  27136  chebbnd1lem3  27317  chebbnd1  27318  chtppilimlem1  27319  chtppilimlem2  27320  chpo1ubb  27327  rplogsumlem1  27330  rplogsumlem2  27331  dchrisum0lem1a  27332  rpvmasumlem  27333  dchrisumlem2  27336  dchrisumlem3  27337  dchrmusumlema  27339  dchrmusum2  27340  dchrvmasumlem1  27341  dchrvmasum2lem  27342  dchrvmasumlema  27346  dchrvmasumiflem1  27347  dchrisum0fno1  27357  dchrisum0lem1b  27361  dchrisum0lem1  27362  dchrisum0lem2  27364  dchrisum0lem3  27365  dchrisum0  27366  mulogsumlem  27377  logdivsum  27379  mulog2sumlem2  27381  vmalogdivsum2  27384  2vmadivsumlem  27386  log2sumbnd  27390  selberglem2  27392  selberg  27394  selberg2lem  27396  chpdifbndlem1  27399  chpdifbndlem2  27400  selberg3lem1  27403  selberg4lem1  27406  pntrsumbnd2  27413  pntrlog2bndlem2  27424  pntrlog2bndlem3  27425  pntrlog2bndlem5  27427  pntrlog2bndlem6a  27428  pntrlog2bndlem6  27429  pntrlog2bnd  27430  pntpbnd1a  27431  pntpbnd1  27432  pntpbnd2  27433  pntibndlem1  27435  pntibndlem2  27437  pntibndlem3  27438  pntibnd  27439  pntlemc  27441  pntlema  27442  pntlemb  27443  pntlemg  27444  pntlemh  27445  pntlemn  27446  pntlemq  27447  pntlemr  27448  pntlemj  27449  pntlemi  27450  pntlemf  27451  pntlemk  27452  pntlemo  27453  pntleme  27454  pntlem3  27455  pntlemp  27456  pntleml  27457  ostth2lem1  27464  ostth2lem3  27481  ostth2  27483  ostth3  27484  crctcshwlkn0lem5  29501  nrt2irr  30159  smcnlem  30383  blocnilem  30490  blocni  30491  ubthlem2  30557  minvecolem3  30562  minvecolem4  30566  minvecolem5  30567  nmcexi  31712  lnconi  31719  fsumub  32467  rpxdivcld  32533  sqsscirc1  33352  cnre2csqlem  33354  tpr2rico  33356  xrmulc1cn  33374  xrge0iifiso  33379  xrge0iifhom  33381  esumcst  33525  esumdivc  33545  dya2icoseg  33740  omssubaddlem  33762  omssubadd  33763  probmeasb  33893  sgnmulrp2  34006  signsply0  34026  logdivsqrle  34126  hgt750leme  34134  dnicn  35832  unblimceq0lem  35846  unbdqndv2lem1  35849  unbdqndv2lem2  35850  knoppndvlem18  35869  knoppndvlem21  35872  poimirlem29  36981  heicant  36987  opnmbllem0  36988  mblfinlem3  36991  itg2addnclem3  37005  itg2addnc  37006  itggt0cn  37022  ftc1cnnclem  37023  ftc1anclem6  37030  ftc1anclem7  37031  geomcau  37091  sstotbnd2  37106  isbnd3  37116  equivbnd  37122  prdsbnd2  37127  cntotbnd  37128  heibor1lem  37141  heiborlem6  37148  bfplem1  37154  bfplem2  37155  bfp  37156  rrndstprj2  37163  rrnequiv  37167  lcmineqlem21  41381  aks4d1p1p4  41403  aks4d1p1p7  41406  aks4d1p5  41412  aks4d1p6  41413  exp11nnd  41678  fltnlta  41868  irrapxlem4  42026  irrapxlem5  42027  irrapx1  42029  pell1qrgaplem  42074  pell14qrgapw  42077  pellqrexplicit  42078  pellqrex  42080  pellfundge  42083  pellfundgt1  42084  rmspecfund  42110  rmxycomplete  42119  rmxypos  42149  binomcxplemnotnn0  43578  suprltrp  44497  supxrge  44507  infrpge  44520  infleinflem1  44539  xralrple4  44542  recnnltrp  44546  rpgtrecnn  44549  cvgcaule  44661  fmul01lt1lem1  44759  fmul01lt1lem2  44760  ltmod  44813  lptre2pt  44815  addlimc  44823  0ellimcdiv  44824  limclner  44826  climleltrp  44851  climisp  44921  climxrrelem  44924  climxrre  44925  limsupgtlem  44952  liminfltlem  44979  cnrefiisplem  45004  climxlim2lem  45020  dvdivbd  45098  ioodvbdlimc1lem2  45107  ioodvbdlimc2lem  45109  itgiccshift  45155  itgperiod  45156  stoweidlem1  45176  stoweidlem3  45178  stoweidlem5  45180  stoweidlem7  45182  stoweidlem11  45186  stoweidlem13  45188  stoweidlem14  45189  stoweidlem24  45199  stoweidlem25  45200  stoweidlem26  45201  stoweidlem34  45209  stoweidlem41  45216  stoweidlem42  45217  stoweidlem49  45224  stoweidlem51  45226  stoweidlem52  45227  stoweidlem59  45234  stoweidlem60  45235  stoweidlem62  45237  stoweid  45238  wallispilem5  45244  stirlinglem1  45249  stirlinglem4  45252  stirlinglem5  45253  stirlinglem6  45254  dirkercncflem1  45278  fourierdlem30  45312  fourierdlem39  45321  fourierdlem47  45328  fourierdlem73  45354  fourierdlem81  45362  fourierdlem87  45368  fourierdlem103  45384  fourierdlem104  45385  fourierdlem107  45388  rrndistlt  45465  qndenserrnbllem  45469  sge0ltfirp  45575  sge0rpcpnf  45596  sge0xaddlem1  45608  omeiunltfirp  45694  carageniuncllem2  45697  ovnsubaddlem1  45745  hoidmvlelem1  45770  hoidmvlelem2  45771  hoidmvlelem3  45772  hoidmvlelem4  45773  hoiqssbllem1  45797  hoiqssbllem2  45798  hoiqssbllem3  45799  hspmbllem2  45802  hspmbllem3  45803  ovolval5lem1  45827  ovolval5lem2  45828  iinhoiicc  45849  vonioolem1  45855  pimrecltpos  45883  smflimlem3  45948  smfmullem1  45966  smfmullem2  45967  smfmullem3  45968  modexp2m1d  46739  dignn0flhalflem1  47463  itsclc0yqsol  47612  amgmwlem  48011  amgmw2d  48013  young2d  48014