Theorem rpred 12936

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11012  ℝ⁺crp 12892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915  df-rp 12893

This theorem is referenced by:  rpxrd  12937  rpcnd  12938  rpregt0d  12942  rprege0d  12943  rprene0d  12944  rprecred  12947  ltmulgt11d  12971  ltmulgt12d  12972  gt0divd  12973  ge0divd  12974  lediv12ad  12995  prodge0rd  13001  xlemul1  13191  xov1plusxeqvd  13400  ltexp2a  14075  rpexpmord  14077  expcan  14078  ltexp2  14079  leexp2a  14081  expnlbnd2  14143  expmulnbnd  14144  exp11nnd  14170  01sqrexlem6  15156  cau3lem  15264  rlimcld2  15487  addcn2  15503  mulcn2  15505  reccn2  15506  o1rlimmul  15528  rlimno1  15563  caucvgrlem  15582  isumrpcl  15752  isumltss  15757  expcnv  15773  mertenslem1  15793  effsumlt  16022  recoshcl  16069  eirrlem  16115  rpnnen2lem11  16135  bitsmod  16349  prmreclem3  16832  prmreclem5  16834  4sqlem7  16858  ssblex  24344  metss2lem  24427  methaus  24436  met1stc  24437  met2ndci  24438  metustto  24469  metustexhalf  24472  nlmvscnlem2  24601  nlmvscnlem1  24602  nrginvrcnlem  24607  nmoi2  24646  nghmcn  24661  reperflem  24735  iccntr  24738  icccmplem2  24740  reconnlem2  24744  opnreen  24748  metdcnlem  24753  metnrmlem3  24778  addcnlem  24781  cnheibor  24882  cnllycmp  24883  lebnumlem3  24890  lebnumii  24893  nmoleub2lem  25042  nmoleub2lem3  25043  nmoleub2lem2  25044  nmoleub3  25047  nmhmcn  25048  ipcnlem2  25172  ipcnlem1  25173  lmnn  25191  iscfil3  25201  cfilfcls  25202  iscmet3lem1  25219  iscmet3lem2  25220  bcthlem4  25255  bcthlem5  25256  minveclem3b  25356  minveclem3  25357  ivthlem2  25381  ovolgelb  25409  ovollb2lem  25417  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliunlem2  25432  ovolscalem1  25442  ioombl1lem2  25488  ioombl1lem4  25490  uniioombllem1  25510  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  opnmbllem  25530  volcn  25535  vitalilem4  25540  itg2mulclem  25675  itg2monolem3  25681  itg2cnlem2  25691  itg2cn  25692  itggt0  25773  dveflem  25911  dvferm1lem  25916  dvferm2lem  25918  lhop1lem  25946  lhop1  25947  lhop  25949  dvcnvrelem1  25950  dvcnvrelem2  25951  dvcnvre  25952  dvfsumrlim  25966  ftc1a  25972  ftc1lem4  25974  plyeq0lem  26143  aalioulem2  26269  aalioulem4  26271  aalioulem5  26272  aalioulem6  26273  aaliou  26274  aaliou2b  26277  aaliou3lem1  26278  aaliou3lem2  26279  aaliou3lem8  26281  aaliou3lem5  26283  aaliou3lem7  26285  aaliou3lem9  26286  ulmcn  26336  ulmdvlem1  26337  mtest  26341  itgulm  26345  psercn  26364  pserdvlem1  26365  pserdvlem2  26366  pserdv  26367  abelthlem7  26376  pilem2  26390  divlogrlim  26572  logcnlem3  26581  logcnlem4  26582  logccv  26600  divcxp  26624  cxplt  26631  cxple2  26634  recxpf1lem  26666  cxpcn3lem  26685  cxpaddlelem  26689  cxpaddle  26690  loglesqrt  26699  leibpi  26880  rlimcnp3  26905  cxplim  26910  rlimcxp  26912  cxp2limlem  26914  cxp2lim  26915  cxploglim  26916  cxploglim2  26917  divsqrtsumlem  26918  jensenlem2  26926  logdifbnd  26932  emcllem4  26937  harmonicbnd4  26949  fsumharmonic  26950  zetacvg  26953  lgamgulmlem2  26968  lgamgulmlem5  26971  lgamucov  26976  regamcl  26999  relgamcl  27000  ftalem1  27011  ftalem2  27012  ftalem3  27013  ftalem5  27015  basellem1  27019  basellem3  27021  basellem4  27022  basellem8  27026  chtwordi  27094  chpchtsum  27158  logfacrlim  27163  logexprlim  27164  bclbnd  27219  efexple  27220  bposlem1  27223  bposlem2  27224  bposlem6  27228  bposlem7  27229  chebbnd1lem3  27410  chebbnd1  27411  chtppilimlem1  27412  chtppilimlem2  27413  chpo1ubb  27420  rplogsumlem1  27423  rplogsumlem2  27424  dchrisum0lem1a  27425  rpvmasumlem  27426  dchrisumlem2  27429  dchrisumlem3  27430  dchrmusumlema  27432  dchrmusum2  27433  dchrvmasumlem1  27434  dchrvmasum2lem  27435  dchrvmasumlema  27439  dchrvmasumiflem1  27440  dchrisum0fno1  27450  dchrisum0lem1b  27454  dchrisum0lem1  27455  dchrisum0lem2  27457  dchrisum0lem3  27458  dchrisum0  27459  mulogsumlem  27470  logdivsum  27472  mulog2sumlem2  27474  vmalogdivsum2  27477  2vmadivsumlem  27479  log2sumbnd  27483  selberglem2  27485  selberg  27487  selberg2lem  27489  chpdifbndlem1  27492  chpdifbndlem2  27493  selberg3lem1  27496  selberg4lem1  27499  pntrsumbnd2  27506  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem5  27520  pntrlog2bndlem6a  27521  pntrlog2bndlem6  27522  pntrlog2bnd  27523  pntpbnd1a  27524  pntpbnd1  27525  pntpbnd2  27526  pntibndlem1  27528  pntibndlem2  27530  pntibndlem3  27531  pntibnd  27532  pntlemc  27534  pntlema  27535  pntlemb  27536  pntlemg  27537  pntlemh  27538  pntlemn  27539  pntlemq  27540  pntlemr  27541  pntlemj  27542  pntlemi  27543  pntlemf  27544  pntlemk  27545  pntlemo  27546  pntleme  27547  pntlem3  27548  pntlemp  27549  pntleml  27550  ostth2lem1  27557  ostth2lem3  27574  ostth2  27576  ostth3  27577  crctcshwlkn0lem5  29794  nrt2irr  30455  smcnlem  30679  blocnilem  30786  blocni  30787  ubthlem2  30853  minvecolem3  30858  minvecolem4  30862  minvecolem5  30863  nmcexi  32008  lnconi  32015  fsumub  32816  sgnmulrp2  32824  rpxdivcld  32921  constrinvcl  33807  constrsqrtcl  33813  sqsscirc1  33942  cnre2csqlem  33944  tpr2rico  33946  xrmulc1cn  33964  xrge0iifiso  33969  xrge0iifhom  33971  esumcst  34097  esumdivc  34117  dya2icoseg  34311  omssubaddlem  34333  omssubadd  34334  probmeasb  34464  signsply0  34585  logdivsqrle  34684  hgt750leme  34692  dnicn  36557  unblimceq0lem  36571  unbdqndv2lem1  36574  unbdqndv2lem2  36575  knoppndvlem18  36594  knoppndvlem21  36597  poimirlem29  37709  heicant  37715  opnmbllem0  37716  mblfinlem3  37719  itg2addnclem3  37733  itg2addnc  37734  itggt0cn  37750  ftc1cnnclem  37751  ftc1anclem6  37758  ftc1anclem7  37759  geomcau  37819  sstotbnd2  37834  isbnd3  37844  equivbnd  37850  prdsbnd2  37855  cntotbnd  37856  heibor1lem  37869  heiborlem6  37876  bfplem1  37882  bfplem2  37883  bfp  37884  rrndstprj2  37891  rrnequiv  37895  lcmineqlem21  42162  aks4d1p1p4  42184  aks4d1p1p7  42187  aks4d1p5  42193  aks4d1p6  42194  aks6d1c2  42243  fltnlta  42781  irrapxlem4  42942  irrapxlem5  42943  irrapx1  42945  pell1qrgaplem  42990  pell14qrgapw  42993  pellqrexplicit  42994  pellqrex  42996  pellfundge  42999  pellfundgt1  43000  rmspecfund  43026  rmxycomplete  43034  rmxypos  43064  binomcxplemnotnn0  44473  suprltrp  45451  supxrge  45461  infrpge  45474  infleinflem1  45492  xralrple4  45495  recnnltrp  45499  rpgtrecnn  45502  cvgcaule  45613  fmul01lt1lem1  45708  fmul01lt1lem2  45709  ltmod  45760  lptre2pt  45762  addlimc  45770  0ellimcdiv  45771  limclner  45773  climleltrp  45798  climisp  45868  climxrrelem  45871  climxrre  45872  limsupgtlem  45899  liminfltlem  45926  cnrefiisplem  45951  climxlim2lem  45967  dvdivbd  46045  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  itgiccshift  46102  itgperiod  46103  stoweidlem1  46123  stoweidlem3  46125  stoweidlem5  46127  stoweidlem7  46129  stoweidlem11  46133  stoweidlem13  46135  stoweidlem14  46136  stoweidlem24  46146  stoweidlem25  46147  stoweidlem26  46148  stoweidlem34  46156  stoweidlem41  46163  stoweidlem42  46164  stoweidlem49  46171  stoweidlem51  46173  stoweidlem52  46174  stoweidlem59  46181  stoweidlem60  46182  stoweidlem62  46184  stoweid  46185  wallispilem5  46191  stirlinglem1  46196  stirlinglem4  46199  stirlinglem5  46200  stirlinglem6  46201  dirkercncflem1  46225  fourierdlem30  46259  fourierdlem39  46268  fourierdlem47  46275  fourierdlem73  46301  fourierdlem81  46309  fourierdlem87  46315  fourierdlem103  46331  fourierdlem104  46332  fourierdlem107  46335  rrndistlt  46412  qndenserrnbllem  46416  sge0ltfirp  46522  sge0rpcpnf  46543  sge0xaddlem1  46555  omeiunltfirp  46641  carageniuncllem2  46644  ovnsubaddlem1  46692  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hoiqssbllem1  46744  hoiqssbllem2  46745  hoiqssbllem3  46746  hspmbllem2  46749  hspmbllem3  46750  ovolval5lem1  46774  ovolval5lem2  46775  iinhoiicc  46796  vonioolem1  46802  pimrecltpos  46830  smflimlem3  46895  smfmullem1  46913  smfmullem2  46914  smfmullem3  46915  modexp2m1d  47736  dignn0flhalflem1  48740  itsclc0yqsol  48889  amgmwlem  49927  amgmw2d  49929  young2d  49930