Theorem rpred 13002

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℝ⁺crp 12958

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-rp 12959

This theorem is referenced by:  rpxrd  13003  rpcnd  13004  rpregt0d  13008  rprege0d  13009  rprene0d  13010  rprecred  13013  ltmulgt11d  13037  ltmulgt12d  13038  gt0divd  13039  ge0divd  13040  lediv12ad  13061  prodge0rd  13067  xlemul1  13257  xov1plusxeqvd  13466  ltexp2a  14138  rpexpmord  14140  expcan  14141  ltexp2  14142  leexp2a  14144  expnlbnd2  14206  expmulnbnd  14207  exp11nnd  14233  01sqrexlem6  15220  cau3lem  15328  rlimcld2  15551  addcn2  15567  mulcn2  15569  reccn2  15570  o1rlimmul  15592  rlimno1  15627  caucvgrlem  15646  isumrpcl  15816  isumltss  15821  expcnv  15837  mertenslem1  15857  effsumlt  16086  recoshcl  16133  eirrlem  16179  rpnnen2lem11  16199  bitsmod  16413  prmreclem3  16896  prmreclem5  16898  4sqlem7  16922  ssblex  24323  metss2lem  24406  methaus  24415  met1stc  24416  met2ndci  24417  metustto  24448  metustexhalf  24451  nlmvscnlem2  24580  nlmvscnlem1  24581  nrginvrcnlem  24586  nmoi2  24625  nghmcn  24640  reperflem  24714  iccntr  24717  icccmplem2  24719  reconnlem2  24723  opnreen  24727  metdcnlem  24732  metnrmlem3  24757  addcnlem  24760  cnheibor  24861  cnllycmp  24862  lebnumlem3  24869  lebnumii  24872  nmoleub2lem  25021  nmoleub2lem3  25022  nmoleub2lem2  25023  nmoleub3  25026  nmhmcn  25027  ipcnlem2  25151  ipcnlem1  25152  lmnn  25170  iscfil3  25180  cfilfcls  25181  iscmet3lem1  25198  iscmet3lem2  25199  bcthlem4  25234  bcthlem5  25235  minveclem3b  25335  minveclem3  25336  ivthlem2  25360  ovolgelb  25388  ovollb2lem  25396  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliunlem2  25411  ovolscalem1  25421  ioombl1lem2  25467  ioombl1lem4  25469  uniioombllem1  25489  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  opnmbllem  25509  volcn  25514  vitalilem4  25519  itg2mulclem  25654  itg2monolem3  25660  itg2cnlem2  25670  itg2cn  25671  itggt0  25752  dveflem  25890  dvferm1lem  25895  dvferm2lem  25897  lhop1lem  25925  lhop1  25926  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvfsumrlim  25945  ftc1a  25951  ftc1lem4  25953  plyeq0lem  26122  aalioulem2  26248  aalioulem4  26250  aalioulem5  26251  aalioulem6  26252  aaliou  26253  aaliou2b  26256  aaliou3lem1  26257  aaliou3lem2  26258  aaliou3lem8  26260  aaliou3lem5  26262  aaliou3lem7  26264  aaliou3lem9  26265  ulmcn  26315  ulmdvlem1  26316  mtest  26320  itgulm  26324  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  pserdv  26346  abelthlem7  26355  pilem2  26369  divlogrlim  26551  logcnlem3  26560  logcnlem4  26561  logccv  26579  divcxp  26603  cxplt  26610  cxple2  26613  recxpf1lem  26645  cxpcn3lem  26664  cxpaddlelem  26668  cxpaddle  26669  loglesqrt  26678  leibpi  26859  rlimcnp3  26884  cxplim  26889  rlimcxp  26891  cxp2limlem  26893  cxp2lim  26894  cxploglim  26895  cxploglim2  26896  divsqrtsumlem  26897  jensenlem2  26905  logdifbnd  26911  emcllem4  26916  harmonicbnd4  26928  fsumharmonic  26929  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem5  26950  lgamucov  26955  regamcl  26978  relgamcl  26979  ftalem1  26990  ftalem2  26991  ftalem3  26992  ftalem5  26994  basellem1  26998  basellem3  27000  basellem4  27001  basellem8  27005  chtwordi  27073  chpchtsum  27137  logfacrlim  27142  logexprlim  27143  bclbnd  27198  efexple  27199  bposlem1  27202  bposlem2  27203  bposlem6  27207  bposlem7  27208  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem1  27391  chtppilimlem2  27392  chpo1ubb  27399  rplogsumlem1  27402  rplogsumlem2  27403  dchrisum0lem1a  27404  rpvmasumlem  27405  dchrisumlem2  27408  dchrisumlem3  27409  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasumlema  27418  dchrvmasumiflem1  27419  dchrisum0fno1  27429  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrisum0  27438  mulogsumlem  27449  logdivsum  27451  mulog2sumlem2  27453  vmalogdivsum2  27456  2vmadivsumlem  27458  log2sumbnd  27462  selberglem2  27464  selberg  27466  selberg2lem  27468  chpdifbndlem1  27471  chpdifbndlem2  27472  selberg3lem1  27475  selberg4lem1  27478  pntrsumbnd2  27485  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntrlog2bndlem6a  27500  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntibndlem1  27507  pntibndlem2  27509  pntibndlem3  27510  pntibnd  27511  pntlemc  27513  pntlema  27514  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemn  27518  pntlemq  27519  pntlemr  27520  pntlemj  27521  pntlemi  27522  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntleme  27526  pntlem3  27527  pntlemp  27528  pntleml  27529  ostth2lem1  27536  ostth2lem3  27553  ostth2  27555  ostth3  27556  crctcshwlkn0lem5  29751  nrt2irr  30409  smcnlem  30633  blocnilem  30740  blocni  30741  ubthlem2  30807  minvecolem3  30812  minvecolem4  30816  minvecolem5  30817  nmcexi  31962  lnconi  31969  fsumub  32760  sgnmulrp2  32768  rpxdivcld  32861  constrinvcl  33770  constrsqrtcl  33776  sqsscirc1  33905  cnre2csqlem  33907  tpr2rico  33909  xrmulc1cn  33927  xrge0iifiso  33932  xrge0iifhom  33934  esumcst  34060  esumdivc  34080  dya2icoseg  34275  omssubaddlem  34297  omssubadd  34298  probmeasb  34428  signsply0  34549  logdivsqrle  34648  hgt750leme  34656  dnicn  36487  unblimceq0lem  36501  unbdqndv2lem1  36504  unbdqndv2lem2  36505  knoppndvlem18  36524  knoppndvlem21  36527  poimirlem29  37650  heicant  37656  opnmbllem0  37657  mblfinlem3  37660  itg2addnclem3  37674  itg2addnc  37675  itggt0cn  37691  ftc1cnnclem  37692  ftc1anclem6  37699  ftc1anclem7  37700  geomcau  37760  sstotbnd2  37775  isbnd3  37785  equivbnd  37791  prdsbnd2  37796  cntotbnd  37797  heibor1lem  37810  heiborlem6  37817  bfplem1  37823  bfplem2  37824  bfp  37825  rrndstprj2  37832  rrnequiv  37836  lcmineqlem21  42044  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p5  42075  aks4d1p6  42076  aks6d1c2  42125  fltnlta  42658  irrapxlem4  42820  irrapxlem5  42821  irrapx1  42823  pell1qrgaplem  42868  pell14qrgapw  42871  pellqrexplicit  42872  pellqrex  42874  pellfundge  42877  pellfundgt1  42878  rmspecfund  42904  rmxycomplete  42913  rmxypos  42943  binomcxplemnotnn0  44352  suprltrp  45331  supxrge  45341  infrpge  45354  infleinflem1  45373  xralrple4  45376  recnnltrp  45380  rpgtrecnn  45383  cvgcaule  45494  fmul01lt1lem1  45589  fmul01lt1lem2  45590  ltmod  45643  lptre2pt  45645  addlimc  45653  0ellimcdiv  45654  limclner  45656  climleltrp  45681  climisp  45751  climxrrelem  45754  climxrre  45755  limsupgtlem  45782  liminfltlem  45809  cnrefiisplem  45834  climxlim2lem  45850  dvdivbd  45928  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  itgiccshift  45985  itgperiod  45986  stoweidlem1  46006  stoweidlem3  46008  stoweidlem5  46010  stoweidlem7  46012  stoweidlem11  46016  stoweidlem13  46018  stoweidlem14  46019  stoweidlem24  46029  stoweidlem25  46030  stoweidlem26  46031  stoweidlem34  46039  stoweidlem41  46046  stoweidlem42  46047  stoweidlem49  46054  stoweidlem51  46056  stoweidlem52  46057  stoweidlem59  46064  stoweidlem60  46065  stoweidlem62  46067  stoweid  46068  wallispilem5  46074  stirlinglem1  46079  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  dirkercncflem1  46108  fourierdlem30  46142  fourierdlem39  46151  fourierdlem47  46158  fourierdlem73  46184  fourierdlem81  46192  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  rrndistlt  46295  qndenserrnbllem  46299  sge0ltfirp  46405  sge0rpcpnf  46426  sge0xaddlem1  46438  omeiunltfirp  46524  carageniuncllem2  46527  ovnsubaddlem1  46575  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoiqssbllem1  46627  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem2  46632  hspmbllem3  46633  ovolval5lem1  46657  ovolval5lem2  46658  iinhoiicc  46679  vonioolem1  46685  pimrecltpos  46713  smflimlem3  46778  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  modexp2m1d  47617  dignn0flhalflem1  48608  itsclc0yqsol  48757  amgmwlem  49795  amgmw2d  49797  young2d  49798