Theorem rpred 11748

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-rp 11709

This theorem is referenced by:  rpxrd  11749  rpcnd  11750  rpregt0d  11754  rprege0d  11755  rprene0d  11756  rprecred  11759  ltmulgt11d  11783  ltmulgt12d  11784  gt0divd  11785  ge0divd  11786  lediv12ad  11807  xlemul1  11992  xov1plusxeqvd  12189  ltexp2a  12774  expcan  12775  ltexp2  12776  leexp2a  12778  expnlbnd2  12857  expmulnbnd  12858  sqrlem6  13836  cau3lem  13942  rlimcld2  14157  addcn2  14172  mulcn2  14174  reccn2  14175  o1rlimmul  14197  rlimno1  14232  caucvgrlem  14251  isumrpcl  14414  isumltss  14419  expcnv  14435  mertenslem1  14455  effsumlt  14680  recoshcl  14727  eirrlem  14771  rpnnen2lem11  14792  bitsmod  14996  prmreclem3  15460  prmreclem5  15462  4sqlem7  15486  ssblex  22043  metss2lem  22126  methaus  22135  met1stc  22136  met2ndci  22137  metustto  22168  metustexhalf  22171  nlmvscnlem2  22299  nlmvscnlem1  22300  nrginvrcnlem  22305  nmoi2  22344  nghmcn  22359  reperflem  22429  iccntr  22432  icccmplem2  22434  reconnlem2  22438  opnreen  22442  metdcnlem  22447  metnrmlem3  22472  addcnlem  22475  cnheibor  22562  cnllycmp  22563  lebnumlem3  22570  lebnumii  22573  nmoleub2lem  22722  nmoleub2lem3  22723  nmoleub2lem2  22724  nmoleub3  22727  nmhmcn  22728  ipcnlem2  22851  ipcnlem1  22852  lmnn  22869  iscfil3  22879  cfilfcls  22880  iscmet3lem1  22897  iscmet3lem2  22898  bcthlem4  22932  bcthlem5  22933  minveclem3b  23007  minveclem3  23008  ivthlem2  23028  ovolgelb  23055  ovollb2lem  23063  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolscalem1  23088  ioombl1lem2  23134  ioombl1lem4  23136  uniioombllem1  23155  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  opnmbllem  23175  volcn  23180  vitalilem4  23186  itg2mulclem  23319  itg2monolem3  23325  itg2cnlem2  23335  itg2cn  23336  itggt0  23414  dveflem  23546  dvferm1lem  23551  dvferm2lem  23553  lhop1lem  23580  lhop1  23581  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvfsumrlim  23598  ftc1a  23604  ftc1lem4  23606  plyeq0lem  23770  aalioulem2  23892  aalioulem4  23894  aalioulem5  23895  aalioulem6  23896  aaliou  23897  aaliou2b  23900  aaliou3lem1  23901  aaliou3lem2  23902  aaliou3lem8  23904  aaliou3lem5  23906  aaliou3lem7  23908  aaliou3lem9  23909  ulmcn  23957  ulmdvlem1  23958  mtest  23962  itgulm  23966  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  pserdv  23987  abelthlem7  23996  pilem2  24010  divlogrlim  24181  logcnlem3  24190  logcnlem4  24191  logccv  24209  divcxp  24233  cxplt  24240  cxple2  24243  cxpcn3lem  24288  cxpaddlelem  24292  cxpaddle  24293  loglesqrt  24299  leibpi  24469  rlimcnp3  24494  cxplim  24498  rlimcxp  24500  cxp2limlem  24502  cxp2lim  24503  cxploglim  24504  cxploglim2  24505  divsqrtsumlem  24506  jensenlem2  24514  logdifbnd  24520  emcllem4  24525  harmonicbnd4  24537  fsumharmonic  24538  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem5  24559  lgamucov  24564  regamcl  24587  relgamcl  24588  ftalem1  24599  ftalem2  24600  ftalem3  24601  ftalem5  24603  basellem1  24607  basellem3  24609  basellem4  24610  basellem8  24614  chtwordi  24682  chpchtsum  24744  logfacrlim  24749  logexprlim  24750  bclbnd  24805  efexple  24806  bposlem1  24809  bposlem2  24810  bposlem6  24814  bposlem7  24815  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chpo1ubb  24970  rplogsumlem1  24973  rplogsumlem2  24974  dchrisum0lem1a  24975  rpvmasumlem  24976  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasumlema  24989  dchrvmasumiflem1  24990  dchrisum0fno1  25000  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrisum0  25009  mulogsumlem  25020  logdivsum  25022  mulog2sumlem2  25024  vmalogdivsum2  25027  2vmadivsumlem  25029  log2sumbnd  25033  selberglem2  25035  selberg  25037  selberg2lem  25039  chpdifbndlem1  25042  chpdifbndlem2  25043  selberg3lem1  25046  selberg4lem1  25049  pntrsumbnd2  25056  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntrlog2bndlem6a  25071  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem1  25078  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemc  25084  pntlema  25085  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemn  25089  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemi  25093  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntleme  25097  pntlem3  25098  pntlemp  25099  pntleml  25100  ostth2lem1  25107  ostth2lem3  25124  ostth2  25126  ostth3  25127  smcnlem  26936  blocnilem  27043  blocni  27044  ubthlem2  27111  minvecolem3  27116  minvecolem4  27120  minvecolem5  27121  nmcexi  28269  lnconi  28276  rpxdivcld  28973  sqsscirc1  29282  cnre2csqlem  29284  tpr2rico  29286  xrmulc1cn  29304  xrge0iifiso  29309  xrge0iifhom  29311  esumcst  29452  esumdivc  29472  dya2icoseg  29666  omssubaddlem  29688  omssubadd  29689  probmeasb  29819  sgnmulrp2  29932  signsply0  29954  signshf  29991  dnicn  31652  unblimceq0lem  31667  unbdqndv2lem1  31670  unbdqndv2lem2  31671  knoppndvlem18  31690  knoppndvlem21  31693  poimirlem29  32608  heicant  32614  opnmbllem0  32615  mblfinlem3  32618  itg2addnclem3  32633  itg2addnc  32634  itggt0cn  32652  ftc1cnnclem  32653  ftc1anclem6  32660  ftc1anclem7  32661  geomcau  32725  sstotbnd2  32743  isbnd3  32753  equivbnd  32759  prdsbnd2  32764  cntotbnd  32765  heibor1lem  32778  heiborlem6  32785  bfplem1  32791  bfplem2  32792  bfp  32793  rrndstprj2  32800  rrnequiv  32804  irrapxlem4  36407  irrapxlem5  36408  irrapx1  36410  pell1qrgaplem  36455  pell14qrgapw  36458  pellqrexplicit  36459  pellqrex  36461  pellfundge  36464  pellfundgt1  36465  rmspecfund  36492  rmxycomplete  36500  rpexpmord  36531  rmxypos  36532  binomcxplemnotnn0  37577  suprltrp  38485  supxrge  38495  infrpge  38508  infleinflem1  38527  xralrple4  38530  recnnltrp  38534  rpgtrecnn  38538  fmul01lt1lem1  38651  fmul01lt1lem2  38652  ltmod  38705  lptre2pt  38707  addlimc  38715  0ellimcdiv  38716  limclner  38718  climleltrp  38743  dvdivbd  38813  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  itgiccshift  38872  itgperiod  38873  stoweidlem1  38894  stoweidlem3  38896  stoweidlem5  38898  stoweidlem7  38900  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem24  38917  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem41  38934  stoweidlem42  38935  stoweidlem49  38942  stoweidlem51  38944  stoweidlem52  38945  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  stoweid  38956  wallispilem5  38962  stirlinglem1  38967  stirlinglem4  38970  stirlinglem5  38971  stirlinglem6  38972  dirkercncflem1  38996  fourierdlem30  39030  fourierdlem39  39039  fourierdlem47  39046  fourierdlem73  39072  fourierdlem81  39080  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  rrndistlt  39186  qndenserrnbllem  39190  sge0ltfirp  39293  sge0rpcpnf  39314  sge0xaddlem1  39326  omeiunltfirp  39409  carageniuncllem2  39412  ovnsubaddlem1  39460  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoiqssbllem1  39512  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem2  39517  hspmbllem3  39518  ovolval5lem1  39542  ovolval5lem2  39543  iinhoiicc  39565  vonioolem1  39571  pimrecltpos  39596  smflimlem3  39659  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  modexp2m1d  40067  crctcsh1wlkn0lem5  41017  dignn0flhalflem1  42207  amgmwlem  42357  amgmw2d  42359  young2d  42360