Theorem rpred 13090

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  ℝ⁺crp 13046

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-rp 13047

This theorem is used by:  rpxrd  13091  rpcnd  13092  rpregt0d  13096  rprege0d  13097  rprene0d  13098  rprecred  13101  ltmulgt11d  13125  ltmulgt12d  13126  gt0divd  13127  ge0divd  13128  lediv12ad  13149  prodge0rd  13155  xlemul1  13346  xov1plusxeqvd  13555  ltexp2a  14234  rpexpmord  14236  expcan  14237  ltexp2  14238  leexp2a  14240  expnlbnd2  14302  expmulnbnd  14303  exp11nnd  14329  sgnmulrp2  15185  01sqrexlem6  15338  cau3lem  15446  rlimcld2  15669  addcn2  15685  mulcn2  15687  reccn2  15688  o1rlimmul  15710  rlimno1  15745  caucvgrlem  15764  isumrpcl  15936  isumltss  15941  expcnv  15957  mertenslem1  15977  effsumlt  16205  recoshcl  16252  eirrlem  16298  rpnnen2lem11  16318  bitsmod  16532  prmreclem3  17016  prmreclem5  17018  4sqlem7  17042  ssblex  24660  metss2lem  24743  methaus  24752  met1stc  24753  met2ndci  24754  metustto  24785  metustexhalf  24788  nlmvscnlem2  24917  nlmvscnlem1  24918  nrginvrcnlem  24923  nmoi2  24962  nghmcn  24977  reperflem  25051  iccntr  25054  icccmplem2  25056  reconnlem2  25060  opnreen  25064  metdcnlem  25069  metnrmlem3  25094  addcnlem  25097  cnheibor  25189  cnllycmp  25190  lebnumlem3  25197  lebnumii  25200  nmoleub2lem  25348  nmoleub2lem3  25349  nmoleub2lem2  25350  nmoleub3  25353  nmhmcn  25354  ipcnlem2  25478  ipcnlem1  25479  lmnn  25497  iscfil3  25507  cfilfcls  25508  iscmet3lem1  25525  iscmet3lem2  25526  bcthlem4  25561  bcthlem5  25562  minveclem3b  25662  minveclem3  25663  ivthlem2  25686  ovolgelb  25714  ovollb2lem  25722  ovolunlem1a  25730  ovolunlem1  25731  ovoliunlem1  25736  ovoliunlem2  25737  ovolscalem1  25747  ioombl1lem2  25793  ioombl1lem4  25795  uniioombllem1  25815  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  opnmbllem  25835  volcn  25840  vitalilem4  25845  itg2mulclem  25980  itg2monolem3  25986  itg2cnlem2  25996  itg2cn  25997  itggt0  26078  dveflem  26213  dvferm1lem  26218  dvferm2lem  26220  lhop1lem  26247  lhop1  26248  lhop  26250  dvcnvrelem1  26251  dvcnvrelem2  26252  dvcnvre  26253  dvfsumrlim  26265  ftc1a  26271  ftc1lem4  26273  plyeq0lem  26443  aalioulem2  26576  aalioulem4  26578  aalioulem5  26579  aalioulem6  26580  aaliou  26581  aaliou2b  26584  aaliou3lem1  26585  aaliou3lem2  26586  aaliou3lem8  26588  aaliou3lem5  26590  aaliou3lem7  26592  aaliou3lem9  26593  ulmcn  26642  ulmdvlem1  26643  mtest  26647  itgulm  26651  psercn  26669  pserdvlem1  26670  pserdvlem2  26671  pserdv  26672  abelthlem7  26681  pilem2  26695  divlogrlim  26880  logcnlem3  26889  logcnlem4  26890  logccv  26908  divcxp  26932  cxplt  26939  cxple2  26942  recxpf1lem  26974  cxpcn3lem  26992  cxpaddlelem  26996  cxpaddle  26997  loglesqrt  27006  leibpi  27187  rlimcnp3  27212  cxplim  27216  rlimcxp  27218  cxp2limlem  27220  cxp2lim  27221  cxploglim  27222  cxploglim2  27223  divsqrtsumlem  27224  jensenlem2  27232  logdifbnd  27238  emcllem4  27243  harmonicbnd4  27255  fsumharmonic  27256  zetacvg  27259  lgamgulmlem2  27274  lgamgulmlem5  27277  lgamucov  27282  regamcl  27305  relgamcl  27306  ftalem1  27317  ftalem2  27318  ftalem3  27319  ftalem5  27321  basellem1  27325  basellem3  27327  basellem4  27328  basellem8  27332  chtwordi  27400  chpchtsum  27463  logfacrlim  27468  logexprlim  27469  bclbnd  27524  efexple  27525  bposlem1  27528  bposlem2  27529  bposlem6  27533  bposlem7  27534  chebbnd1lem3  27715  chebbnd1  27716  chtppilimlem1  27717  chtppilimlem2  27718  chpo1ubb  27725  rplogsumlem1  27728  rplogsumlem2  27729  dchrisum0lem1a  27730  rpvmasumlem  27731  dchrisumlem2  27734  dchrisumlem3  27735  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumlem1  27739  dchrvmasum2lem  27740  dchrvmasumlema  27744  dchrvmasumiflem1  27745  dchrisum0fno1  27755  dchrisum0lem1b  27759  dchrisum0lem1  27760  dchrisum0lem2  27762  dchrisum0lem3  27763  dchrisum0  27764  mulogsumlem  27775  logdivsum  27777  mulog2sumlem2  27779  vmalogdivsum2  27782  2vmadivsumlem  27784  log2sumbnd  27788  selberglem2  27790  selberg  27792  selberg2lem  27794  chpdifbndlem1  27797  chpdifbndlem2  27798  selberg3lem1  27801  selberg4lem1  27804  pntrsumbnd2  27811  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem5  27825  pntrlog2bndlem6a  27826  pntrlog2bndlem6  27827  pntrlog2bnd  27828  pntpbnd1a  27829  pntpbnd1  27830  pntpbnd2  27831  pntibndlem1  27833  pntibndlem2  27835  pntibndlem3  27836  pntibnd  27837  pntlemc  27839  pntlema  27840  pntlemb  27841  pntlemg  27842  pntlemh  27843  pntlemn  27844  pntlemq  27845  pntlemr  27846  pntlemj  27847  pntlemi  27848  pntlemf  27849  pntlemk  27850  pntlemo  27851  pntleme  27852  pntlem3  27853  pntlemp  27854  pntleml  27855  ostth2lem1  27862  ostth2lem3  27879  ostth2  27881  ostth3  27882  crctcshwlkn0lem5  30290  nrt2irr  30961  smcnlem  31186  blocnilem  31293  blocni  31294  ubthlem2  31360  minvecolem3  31365  minvecolem4  31369  minvecolem5  31370  nmcexi  32515  lnconi  32522  fsumub  33306  rpxdivcld  33387  constrinvcl  34291  constrsqrtcl  34297  sqsscirc1  34426  cnre2csqlem  34428  tpr2rico  34430  xrmulc1cn  34448  xrge0iifiso  34453  xrge0iifhom  34455  esumcst  34581  esumdivc  34601  dya2icoseg  34796  omssubaddlem  34818  omssubadd  34819  probmeasb  34949  signsply0  35067  logdivsqrle  35166  hgt750leme  35174  dnicn  37197  unblimceq0lem  37211  unbdqndv2lem1  37214  unbdqndv2lem2  37215  knoppndvlem18  37234  knoppndvlem21  37237  poimirlem29  38406  heicant  38412  opnmbllem0  38413  mblfinlem3  38416  itg2addnclem3  38430  itg2addnc  38431  itggt0cn  38447  ftc1cnnclem  38448  ftc1anclem6  38455  ftc1anclem7  38456  geomcau  38517  sstotbnd2  38532  isbnd3  38542  equivbnd  38548  prdsbnd2  38553  cntotbnd  38554  heibor1lem  38567  heiborlem6  38574  bfplem1  38580  bfplem2  38581  bfp  38582  rrndstprj2  38589  rrnequiv  38593  lcmineqlem21  42923  aks4d1p1p4  42945  aks4d1p1p7  42948  aks4d1p5  42954  aks4d1p6  42955  aks6d1c2  43004  fltnlta  43517  irrapxlem4  43674  irrapxlem5  43675  irrapx1  43677  pell1qrgaplem  43722  pell14qrgapw  43725  pellqrexplicit  43726  pellqrex  43728  pellfundge  43731  pellfundgt1  43732  rmspecfund  43758  rmxycomplete  43766  rmxypos  43796  binomcxplemnotnn0  45188  suprltrp  46166  supxrge  46176  infrpge  46189  infleinflem1  46207  xralrple4  46210  recnnltrp  46214  rpgtrecnn  46217  cvgcaule  46327  fmul01lt1lem1  46422  fmul01lt1lem2  46423  ltmod  46474  lptre2pt  46476  addlimc  46484  0ellimcdiv  46485  limclner  46487  climleltrp  46512  climisp  46582  climxrrelem  46585  climxrre  46586  limsupgtlem  46613  liminfltlem  46640  cnrefiisplem  46665  climxlim2lem  46681  dvdivbd  46759  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  itgiccshift  46816  itgperiod  46817  stoweidlem1  46837  stoweidlem3  46839  stoweidlem5  46841  stoweidlem7  46843  stoweidlem11  46847  stoweidlem13  46849  stoweidlem14  46850  stoweidlem24  46860  stoweidlem25  46861  stoweidlem26  46862  stoweidlem34  46870  stoweidlem41  46877  stoweidlem42  46878  stoweidlem49  46885  stoweidlem51  46887  stoweidlem52  46888  stoweidlem59  46895  stoweidlem60  46896  stoweidlem62  46898  stoweid  46899  wallispilem5  46905  stirlinglem1  46910  stirlinglem4  46913  stirlinglem5  46914  stirlinglem6  46915  dirkercncflem1  46939  fourierdlem30  46973  fourierdlem39  46982  fourierdlem47  46989  fourierdlem73  47015  fourierdlem81  47023  fourierdlem87  47029  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  rrndistlt  47126  qndenserrnbllem  47130  sge0ltfirp  47236  sge0rpcpnf  47257  sge0xaddlem1  47269  omeiunltfirp  47355  carageniuncllem2  47358  ovnsubaddlem1  47406  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  hoiqssbllem1  47458  hoiqssbllem2  47459  hoiqssbllem3  47460  hspmbllem2  47463  hspmbllem3  47464  ovolval5lem1  47488  ovolval5lem2  47489  iinhoiicc  47510  vonioolem1  47516  pimrecltpos  47544  smflimlem3  47609  smfmullem1  47627  smfmullem2  47628  smfmullem3  47629  modexp2m1d  48523  dignn0flhalflem1  49553  itsclc0yqsol  49702  amgmwlem  50828  amgmw2d  50830  young2d  50831