Theorem rpred 13056

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11133  ℝ⁺crp 13013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-ss 3948  df-rp 13014

This theorem is referenced by:  rpxrd  13057  rpcnd  13058  rpregt0d  13062  rprege0d  13063  rprene0d  13064  rprecred  13067  ltmulgt11d  13091  ltmulgt12d  13092  gt0divd  13093  ge0divd  13094  lediv12ad  13115  prodge0rd  13121  xlemul1  13311  xov1plusxeqvd  13520  ltexp2a  14189  rpexpmord  14191  expcan  14192  ltexp2  14193  leexp2a  14195  expnlbnd2  14257  expmulnbnd  14258  exp11nnd  14284  01sqrexlem6  15271  cau3lem  15378  rlimcld2  15599  addcn2  15615  mulcn2  15617  reccn2  15618  o1rlimmul  15640  rlimno1  15675  caucvgrlem  15694  isumrpcl  15864  isumltss  15869  expcnv  15885  mertenslem1  15905  effsumlt  16134  recoshcl  16181  eirrlem  16227  rpnnen2lem11  16247  bitsmod  16460  prmreclem3  16943  prmreclem5  16945  4sqlem7  16969  ssblex  24372  metss2lem  24455  methaus  24464  met1stc  24465  met2ndci  24466  metustto  24497  metustexhalf  24500  nlmvscnlem2  24629  nlmvscnlem1  24630  nrginvrcnlem  24635  nmoi2  24674  nghmcn  24689  reperflem  24763  iccntr  24766  icccmplem2  24768  reconnlem2  24772  opnreen  24776  metdcnlem  24781  metnrmlem3  24806  addcnlem  24809  cnheibor  24910  cnllycmp  24911  lebnumlem3  24918  lebnumii  24921  nmoleub2lem  25070  nmoleub2lem3  25071  nmoleub2lem2  25072  nmoleub3  25075  nmhmcn  25076  ipcnlem2  25201  ipcnlem1  25202  lmnn  25220  iscfil3  25230  cfilfcls  25231  iscmet3lem1  25248  iscmet3lem2  25249  bcthlem4  25284  bcthlem5  25285  minveclem3b  25385  minveclem3  25386  ivthlem2  25410  ovolgelb  25438  ovollb2lem  25446  ovolunlem1a  25454  ovolunlem1  25455  ovoliunlem1  25460  ovoliunlem2  25461  ovolscalem1  25471  ioombl1lem2  25517  ioombl1lem4  25519  uniioombllem1  25539  uniioombllem3  25543  uniioombllem4  25544  uniioombllem5  25545  opnmbllem  25559  volcn  25564  vitalilem4  25569  itg2mulclem  25704  itg2monolem3  25710  itg2cnlem2  25720  itg2cn  25721  itggt0  25802  dveflem  25940  dvferm1lem  25945  dvferm2lem  25947  lhop1lem  25975  lhop1  25976  lhop  25978  dvcnvrelem1  25979  dvcnvrelem2  25980  dvcnvre  25981  dvfsumrlim  25995  ftc1a  26001  ftc1lem4  26003  plyeq0lem  26172  aalioulem2  26298  aalioulem4  26300  aalioulem5  26301  aalioulem6  26302  aaliou  26303  aaliou2b  26306  aaliou3lem1  26307  aaliou3lem2  26308  aaliou3lem8  26310  aaliou3lem5  26312  aaliou3lem7  26314  aaliou3lem9  26315  ulmcn  26365  ulmdvlem1  26366  mtest  26370  itgulm  26374  psercn  26393  pserdvlem1  26394  pserdvlem2  26395  pserdv  26396  abelthlem7  26405  pilem2  26419  divlogrlim  26601  logcnlem3  26610  logcnlem4  26611  logccv  26629  divcxp  26653  cxplt  26660  cxple2  26663  recxpf1lem  26695  cxpcn3lem  26714  cxpaddlelem  26718  cxpaddle  26719  loglesqrt  26728  leibpi  26909  rlimcnp3  26934  cxplim  26939  rlimcxp  26941  cxp2limlem  26943  cxp2lim  26944  cxploglim  26945  cxploglim2  26946  divsqrtsumlem  26947  jensenlem2  26955  logdifbnd  26961  emcllem4  26966  harmonicbnd4  26978  fsumharmonic  26979  zetacvg  26982  lgamgulmlem2  26997  lgamgulmlem5  27000  lgamucov  27005  regamcl  27028  relgamcl  27029  ftalem1  27040  ftalem2  27041  ftalem3  27042  ftalem5  27044  basellem1  27048  basellem3  27050  basellem4  27051  basellem8  27055  chtwordi  27123  chpchtsum  27187  logfacrlim  27192  logexprlim  27193  bclbnd  27248  efexple  27249  bposlem1  27252  bposlem2  27253  bposlem6  27257  bposlem7  27258  chebbnd1lem3  27439  chebbnd1  27440  chtppilimlem1  27441  chtppilimlem2  27442  chpo1ubb  27449  rplogsumlem1  27452  rplogsumlem2  27453  dchrisum0lem1a  27454  rpvmasumlem  27455  dchrisumlem2  27458  dchrisumlem3  27459  dchrmusumlema  27461  dchrmusum2  27462  dchrvmasumlem1  27463  dchrvmasum2lem  27464  dchrvmasumlema  27468  dchrvmasumiflem1  27469  dchrisum0fno1  27479  dchrisum0lem1b  27483  dchrisum0lem1  27484  dchrisum0lem2  27486  dchrisum0lem3  27487  dchrisum0  27488  mulogsumlem  27499  logdivsum  27501  mulog2sumlem2  27503  vmalogdivsum2  27506  2vmadivsumlem  27508  log2sumbnd  27512  selberglem2  27514  selberg  27516  selberg2lem  27518  chpdifbndlem1  27521  chpdifbndlem2  27522  selberg3lem1  27525  selberg4lem1  27528  pntrsumbnd2  27535  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem5  27549  pntrlog2bndlem6a  27550  pntrlog2bndlem6  27551  pntrlog2bnd  27552  pntpbnd1a  27553  pntpbnd1  27554  pntpbnd2  27555  pntibndlem1  27557  pntibndlem2  27559  pntibndlem3  27560  pntibnd  27561  pntlemc  27563  pntlema  27564  pntlemb  27565  pntlemg  27566  pntlemh  27567  pntlemn  27568  pntlemq  27569  pntlemr  27570  pntlemj  27571  pntlemi  27572  pntlemf  27573  pntlemk  27574  pntlemo  27575  pntleme  27576  pntlem3  27577  pntlemp  27578  pntleml  27579  ostth2lem1  27586  ostth2lem3  27603  ostth2  27605  ostth3  27606  crctcshwlkn0lem5  29801  nrt2irr  30459  smcnlem  30683  blocnilem  30790  blocni  30791  ubthlem2  30857  minvecolem3  30862  minvecolem4  30866  minvecolem5  30867  nmcexi  32012  lnconi  32019  fsumub  32812  sgnmulrp2  32820  rpxdivcld  32913  constrinvcl  33812  constrsqrtcl  33818  sqsscirc1  33944  cnre2csqlem  33946  tpr2rico  33948  xrmulc1cn  33966  xrge0iifiso  33971  xrge0iifhom  33973  esumcst  34099  esumdivc  34119  dya2icoseg  34314  omssubaddlem  34336  omssubadd  34337  probmeasb  34467  signsply0  34588  logdivsqrle  34687  hgt750leme  34695  dnicn  36515  unblimceq0lem  36529  unbdqndv2lem1  36532  unbdqndv2lem2  36533  knoppndvlem18  36552  knoppndvlem21  36555  poimirlem29  37678  heicant  37684  opnmbllem0  37685  mblfinlem3  37688  itg2addnclem3  37702  itg2addnc  37703  itggt0cn  37719  ftc1cnnclem  37720  ftc1anclem6  37727  ftc1anclem7  37728  geomcau  37788  sstotbnd2  37803  isbnd3  37813  equivbnd  37819  prdsbnd2  37824  cntotbnd  37825  heibor1lem  37838  heiborlem6  37845  bfplem1  37851  bfplem2  37852  bfp  37853  rrndstprj2  37860  rrnequiv  37864  lcmineqlem21  42067  aks4d1p1p4  42089  aks4d1p1p7  42092  aks4d1p5  42098  aks4d1p6  42099  aks6d1c2  42148  fltnlta  42661  irrapxlem4  42823  irrapxlem5  42824  irrapx1  42826  pell1qrgaplem  42871  pell14qrgapw  42874  pellqrexplicit  42875  pellqrex  42877  pellfundge  42880  pellfundgt1  42881  rmspecfund  42907  rmxycomplete  42916  rmxypos  42946  binomcxplemnotnn0  44355  suprltrp  45335  supxrge  45345  infrpge  45358  infleinflem1  45377  xralrple4  45380  recnnltrp  45384  rpgtrecnn  45387  cvgcaule  45498  fmul01lt1lem1  45593  fmul01lt1lem2  45594  ltmod  45647  lptre2pt  45649  addlimc  45657  0ellimcdiv  45658  limclner  45660  climleltrp  45685  climisp  45755  climxrrelem  45758  climxrre  45759  limsupgtlem  45786  liminfltlem  45813  cnrefiisplem  45838  climxlim2lem  45854  dvdivbd  45932  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  itgiccshift  45989  itgperiod  45990  stoweidlem1  46010  stoweidlem3  46012  stoweidlem5  46014  stoweidlem7  46016  stoweidlem11  46020  stoweidlem13  46022  stoweidlem14  46023  stoweidlem24  46033  stoweidlem25  46034  stoweidlem26  46035  stoweidlem34  46043  stoweidlem41  46050  stoweidlem42  46051  stoweidlem49  46058  stoweidlem51  46060  stoweidlem52  46061  stoweidlem59  46068  stoweidlem60  46069  stoweidlem62  46071  stoweid  46072  wallispilem5  46078  stirlinglem1  46083  stirlinglem4  46086  stirlinglem5  46087  stirlinglem6  46088  dirkercncflem1  46112  fourierdlem30  46146  fourierdlem39  46155  fourierdlem47  46162  fourierdlem73  46188  fourierdlem81  46196  fourierdlem87  46202  fourierdlem103  46218  fourierdlem104  46219  fourierdlem107  46222  rrndistlt  46299  qndenserrnbllem  46303  sge0ltfirp  46409  sge0rpcpnf  46430  sge0xaddlem1  46442  omeiunltfirp  46528  carageniuncllem2  46531  ovnsubaddlem1  46579  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem3  46606  hoidmvlelem4  46607  hoiqssbllem1  46631  hoiqssbllem2  46632  hoiqssbllem3  46633  hspmbllem2  46636  hspmbllem3  46637  ovolval5lem1  46661  ovolval5lem2  46662  iinhoiicc  46683  vonioolem1  46689  pimrecltpos  46717  smflimlem3  46782  smfmullem1  46800  smfmullem2  46801  smfmullem3  46802  modexp2m1d  47606  dignn0flhalflem1  48575  itsclc0yqsol  48724  amgmwlem  49646  amgmw2d  49648  young2d  49649