Theorem rpred 13051

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-rp 13008

This theorem is referenced by:  rpxrd  13052  rpcnd  13053  rpregt0d  13057  rprege0d  13058  rprene0d  13059  rprecred  13062  ltmulgt11d  13086  ltmulgt12d  13087  gt0divd  13088  ge0divd  13089  lediv12ad  13110  prodge0rd  13116  xlemul1  13307  xov1plusxeqvd  13516  ltexp2a  14193  rpexpmord  14195  expcan  14196  ltexp2  14197  leexp2a  14199  expnlbnd2  14261  expmulnbnd  14262  exp11nnd  14288  sgnmulrp2  15135  01sqrexlem6  15288  cau3lem  15396  rlimcld2  15619  addcn2  15635  mulcn2  15637  reccn2  15638  o1rlimmul  15660  rlimno1  15695  caucvgrlem  15714  isumrpcl  15887  isumltss  15892  expcnv  15908  mertenslem1  15928  effsumlt  16157  recoshcl  16204  eirrlem  16250  rpnnen2lem11  16270  bitsmod  16484  prmreclem3  16968  prmreclem5  16970  4sqlem7  16994  ssblex  24546  metss2lem  24629  methaus  24638  met1stc  24639  met2ndci  24640  metustto  24671  metustexhalf  24674  nlmvscnlem2  24803  nlmvscnlem1  24804  nrginvrcnlem  24809  nmoi2  24848  nghmcn  24863  reperflem  24937  iccntr  24940  icccmplem2  24942  reconnlem2  24946  opnreen  24950  metdcnlem  24955  metnrmlem3  24980  addcnlem  24983  cnheibor  25075  cnllycmp  25076  lebnumlem3  25083  lebnumii  25086  nmoleub2lem  25234  nmoleub2lem3  25235  nmoleub2lem2  25236  nmoleub3  25239  nmhmcn  25240  ipcnlem2  25364  ipcnlem1  25365  lmnn  25383  iscfil3  25393  cfilfcls  25394  iscmet3lem1  25411  iscmet3lem2  25412  bcthlem4  25447  bcthlem5  25448  minveclem3b  25548  minveclem3  25549  ivthlem2  25572  ovolgelb  25600  ovollb2lem  25608  ovolunlem1a  25616  ovolunlem1  25617  ovoliunlem1  25622  ovoliunlem2  25623  ovolscalem1  25633  ioombl1lem2  25679  ioombl1lem4  25681  uniioombllem1  25701  uniioombllem3  25705  uniioombllem4  25706  uniioombllem5  25707  opnmbllem  25721  volcn  25726  vitalilem4  25731  itg2mulclem  25866  itg2monolem3  25872  itg2cnlem2  25882  itg2cn  25883  itggt0  25964  dveflem  26099  dvferm1lem  26104  dvferm2lem  26106  lhop1lem  26133  lhop1  26134  lhop  26136  dvcnvrelem1  26137  dvcnvrelem2  26138  dvcnvre  26139  dvfsumrlim  26151  ftc1a  26157  ftc1lem4  26159  plyeq0lem  26328  aalioulem2  26455  aalioulem4  26457  aalioulem5  26458  aalioulem6  26459  aaliou  26460  aaliou2b  26463  aaliou3lem1  26464  aaliou3lem2  26465  aaliou3lem8  26467  aaliou3lem5  26469  aaliou3lem7  26471  aaliou3lem9  26472  ulmcn  26520  ulmdvlem1  26521  mtest  26525  itgulm  26529  psercn  26547  pserdvlem1  26548  pserdvlem2  26549  pserdv  26550  abelthlem7  26559  pilem2  26573  divlogrlim  26758  logcnlem3  26767  logcnlem4  26768  logccv  26786  divcxp  26810  cxplt  26817  cxple2  26820  recxpf1lem  26852  cxpcn3lem  26870  cxpaddlelem  26874  cxpaddle  26875  loglesqrt  26884  leibpi  27065  rlimcnp3  27090  cxplim  27094  rlimcxp  27096  cxp2limlem  27098  cxp2lim  27099  cxploglim  27100  cxploglim2  27101  divsqrtsumlem  27102  jensenlem2  27110  logdifbnd  27116  emcllem4  27121  harmonicbnd4  27133  fsumharmonic  27134  zetacvg  27137  lgamgulmlem2  27152  lgamgulmlem5  27155  lgamucov  27160  regamcl  27183  relgamcl  27184  ftalem1  27195  ftalem2  27196  ftalem3  27197  ftalem5  27199  basellem1  27203  basellem3  27205  basellem4  27206  basellem8  27210  chtwordi  27278  chpchtsum  27341  logfacrlim  27346  logexprlim  27347  bclbnd  27402  efexple  27403  bposlem1  27406  bposlem2  27407  bposlem6  27411  bposlem7  27412  chebbnd1lem3  27593  chebbnd1  27594  chtppilimlem1  27595  chtppilimlem2  27596  chpo1ubb  27603  rplogsumlem1  27606  rplogsumlem2  27607  dchrisum0lem1a  27608  rpvmasumlem  27609  dchrisumlem2  27612  dchrisumlem3  27613  dchrmusumlema  27615  dchrmusum2  27616  dchrvmasumlem1  27617  dchrvmasum2lem  27618  dchrvmasumlema  27622  dchrvmasumiflem1  27623  dchrisum0fno1  27633  dchrisum0lem1b  27637  dchrisum0lem1  27638  dchrisum0lem2  27640  dchrisum0lem3  27641  dchrisum0  27642  mulogsumlem  27653  logdivsum  27655  mulog2sumlem2  27657  vmalogdivsum2  27660  2vmadivsumlem  27662  log2sumbnd  27666  selberglem2  27668  selberg  27670  selberg2lem  27672  chpdifbndlem1  27675  chpdifbndlem2  27676  selberg3lem1  27679  selberg4lem1  27682  pntrsumbnd2  27689  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem5  27703  pntrlog2bndlem6a  27704  pntrlog2bndlem6  27705  pntrlog2bnd  27706  pntpbnd1a  27707  pntpbnd1  27708  pntpbnd2  27709  pntibndlem1  27711  pntibndlem2  27713  pntibndlem3  27714  pntibnd  27715  pntlemc  27717  pntlema  27718  pntlemb  27719  pntlemg  27720  pntlemh  27721  pntlemn  27722  pntlemq  27723  pntlemr  27724  pntlemj  27725  pntlemi  27726  pntlemf  27727  pntlemk  27728  pntlemo  27729  pntleme  27730  pntlem3  27731  pntlemp  27732  pntleml  27733  ostth2lem1  27740  ostth2lem3  27757  ostth2  27759  ostth3  27760  crctcshwlkn0lem5  30072  nrt2irr  30733  smcnlem  30958  blocnilem  31065  blocni  31066  ubthlem2  31132  minvecolem3  31137  minvecolem4  31141  minvecolem5  31142  nmcexi  32287  lnconi  32294  fsumub  33085  rpxdivcld  33166  constrinvcl  34080  constrsqrtcl  34086  sqsscirc1  34215  cnre2csqlem  34217  tpr2rico  34219  xrmulc1cn  34237  xrge0iifiso  34242  xrge0iifhom  34244  esumcst  34370  esumdivc  34390  dya2icoseg  34584  omssubaddlem  34606  omssubadd  34607  probmeasb  34737  signsply0  34855  logdivsqrle  34954  hgt750leme  34962  dnicn  36943  unblimceq0lem  36957  unbdqndv2lem1  36960  unbdqndv2lem2  36961  knoppndvlem18  36980  knoppndvlem21  36983  poimirlem29  38160  heicant  38166  opnmbllem0  38167  mblfinlem3  38170  itg2addnclem3  38184  itg2addnc  38185  itggt0cn  38201  ftc1cnnclem  38202  ftc1anclem6  38209  ftc1anclem7  38210  geomcau  38270  sstotbnd2  38285  isbnd3  38295  equivbnd  38301  prdsbnd2  38306  cntotbnd  38307  heibor1lem  38320  heiborlem6  38327  bfplem1  38333  bfplem2  38334  bfp  38335  rrndstprj2  38342  rrnequiv  38346  lcmineqlem21  42678  aks4d1p1p4  42700  aks4d1p1p7  42703  aks4d1p5  42709  aks4d1p6  42710  aks6d1c2  42759  fltnlta  43257  irrapxlem4  43414  irrapxlem5  43415  irrapx1  43417  pell1qrgaplem  43462  pell14qrgapw  43465  pellqrexplicit  43466  pellqrex  43468  pellfundge  43471  pellfundgt1  43472  rmspecfund  43498  rmxycomplete  43506  rmxypos  43536  binomcxplemnotnn0  44930  suprltrp  45902  supxrge  45912  infrpge  45925  infleinflem1  45943  xralrple4  45946  recnnltrp  45950  rpgtrecnn  45953  cvgcaule  46063  fmul01lt1lem1  46158  fmul01lt1lem2  46159  ltmod  46210  lptre2pt  46212  addlimc  46220  0ellimcdiv  46221  limclner  46223  climleltrp  46248  climisp  46318  climxrrelem  46321  climxrre  46322  limsupgtlem  46349  liminfltlem  46376  cnrefiisplem  46401  climxlim2lem  46417  dvdivbd  46495  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  itgiccshift  46552  itgperiod  46553  stoweidlem1  46573  stoweidlem3  46575  stoweidlem5  46577  stoweidlem7  46579  stoweidlem11  46583  stoweidlem13  46585  stoweidlem14  46586  stoweidlem24  46596  stoweidlem25  46597  stoweidlem26  46598  stoweidlem34  46606  stoweidlem41  46613  stoweidlem42  46614  stoweidlem49  46621  stoweidlem51  46623  stoweidlem52  46624  stoweidlem59  46631  stoweidlem60  46632  stoweidlem62  46634  stoweid  46635  wallispilem5  46641  stirlinglem1  46646  stirlinglem4  46649  stirlinglem5  46650  stirlinglem6  46651  dirkercncflem1  46675  fourierdlem30  46709  fourierdlem39  46718  fourierdlem47  46725  fourierdlem73  46751  fourierdlem81  46759  fourierdlem87  46765  fourierdlem103  46781  fourierdlem104  46782  fourierdlem107  46785  rrndistlt  46862  qndenserrnbllem  46866  sge0ltfirp  46972  sge0rpcpnf  46993  sge0xaddlem1  47005  omeiunltfirp  47091  carageniuncllem2  47094  ovnsubaddlem1  47142  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem4  47170  hoiqssbllem1  47194  hoiqssbllem2  47195  hoiqssbllem3  47196  hspmbllem2  47199  hspmbllem3  47200  ovolval5lem1  47224  ovolval5lem2  47225  iinhoiicc  47246  vonioolem1  47252  pimrecltpos  47280  smflimlem3  47345  smfmullem1  47363  smfmullem2  47364  smfmullem3  47365  modexp2m1d  48219  dignn0flhalflem1  49246  itsclc0yqsol  49395  amgmwlem  50431  amgmw2d  50433  young2d  50434