Theorem rpred 12955

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  ℝ⁺crp 12911

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-ss 3922  df-rp 12912

This theorem is referenced by:  rpxrd  12956  rpcnd  12957  rpregt0d  12961  rprege0d  12962  rprene0d  12963  rprecred  12966  ltmulgt11d  12990  ltmulgt12d  12991  gt0divd  12992  ge0divd  12993  lediv12ad  13014  prodge0rd  13020  xlemul1  13210  xov1plusxeqvd  13419  ltexp2a  14091  rpexpmord  14093  expcan  14094  ltexp2  14095  leexp2a  14097  expnlbnd2  14159  expmulnbnd  14160  exp11nnd  14186  01sqrexlem6  15172  cau3lem  15280  rlimcld2  15503  addcn2  15519  mulcn2  15521  reccn2  15522  o1rlimmul  15544  rlimno1  15579  caucvgrlem  15598  isumrpcl  15768  isumltss  15773  expcnv  15789  mertenslem1  15809  effsumlt  16038  recoshcl  16085  eirrlem  16131  rpnnen2lem11  16151  bitsmod  16365  prmreclem3  16848  prmreclem5  16850  4sqlem7  16874  ssblex  24332  metss2lem  24415  methaus  24424  met1stc  24425  met2ndci  24426  metustto  24457  metustexhalf  24460  nlmvscnlem2  24589  nlmvscnlem1  24590  nrginvrcnlem  24595  nmoi2  24634  nghmcn  24649  reperflem  24723  iccntr  24726  icccmplem2  24728  reconnlem2  24732  opnreen  24736  metdcnlem  24741  metnrmlem3  24766  addcnlem  24769  cnheibor  24870  cnllycmp  24871  lebnumlem3  24878  lebnumii  24881  nmoleub2lem  25030  nmoleub2lem3  25031  nmoleub2lem2  25032  nmoleub3  25035  nmhmcn  25036  ipcnlem2  25160  ipcnlem1  25161  lmnn  25179  iscfil3  25189  cfilfcls  25190  iscmet3lem1  25207  iscmet3lem2  25208  bcthlem4  25243  bcthlem5  25244  minveclem3b  25344  minveclem3  25345  ivthlem2  25369  ovolgelb  25397  ovollb2lem  25405  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliunlem2  25420  ovolscalem1  25430  ioombl1lem2  25476  ioombl1lem4  25478  uniioombllem1  25498  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  opnmbllem  25518  volcn  25523  vitalilem4  25528  itg2mulclem  25663  itg2monolem3  25669  itg2cnlem2  25679  itg2cn  25680  itggt0  25761  dveflem  25899  dvferm1lem  25904  dvferm2lem  25906  lhop1lem  25934  lhop1  25935  lhop  25937  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcnvre  25940  dvfsumrlim  25954  ftc1a  25960  ftc1lem4  25962  plyeq0lem  26131  aalioulem2  26257  aalioulem4  26259  aalioulem5  26260  aalioulem6  26261  aaliou  26262  aaliou2b  26265  aaliou3lem1  26266  aaliou3lem2  26267  aaliou3lem8  26269  aaliou3lem5  26271  aaliou3lem7  26273  aaliou3lem9  26274  ulmcn  26324  ulmdvlem1  26325  mtest  26329  itgulm  26333  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  pserdv  26355  abelthlem7  26364  pilem2  26378  divlogrlim  26560  logcnlem3  26569  logcnlem4  26570  logccv  26588  divcxp  26612  cxplt  26619  cxple2  26622  recxpf1lem  26654  cxpcn3lem  26673  cxpaddlelem  26677  cxpaddle  26678  loglesqrt  26687  leibpi  26868  rlimcnp3  26893  cxplim  26898  rlimcxp  26900  cxp2limlem  26902  cxp2lim  26903  cxploglim  26904  cxploglim2  26905  divsqrtsumlem  26906  jensenlem2  26914  logdifbnd  26920  emcllem4  26925  harmonicbnd4  26937  fsumharmonic  26938  zetacvg  26941  lgamgulmlem2  26956  lgamgulmlem5  26959  lgamucov  26964  regamcl  26987  relgamcl  26988  ftalem1  26999  ftalem2  27000  ftalem3  27001  ftalem5  27003  basellem1  27007  basellem3  27009  basellem4  27010  basellem8  27014  chtwordi  27082  chpchtsum  27146  logfacrlim  27151  logexprlim  27152  bclbnd  27207  efexple  27208  bposlem1  27211  bposlem2  27212  bposlem6  27216  bposlem7  27217  chebbnd1lem3  27398  chebbnd1  27399  chtppilimlem1  27400  chtppilimlem2  27401  chpo1ubb  27408  rplogsumlem1  27411  rplogsumlem2  27412  dchrisum0lem1a  27413  rpvmasumlem  27414  dchrisumlem2  27417  dchrisumlem3  27418  dchrmusumlema  27420  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasumlema  27427  dchrvmasumiflem1  27428  dchrisum0fno1  27438  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0lem2  27445  dchrisum0lem3  27446  dchrisum0  27447  mulogsumlem  27458  logdivsum  27460  mulog2sumlem2  27462  vmalogdivsum2  27465  2vmadivsumlem  27467  log2sumbnd  27471  selberglem2  27473  selberg  27475  selberg2lem  27477  chpdifbndlem1  27480  chpdifbndlem2  27481  selberg3lem1  27484  selberg4lem1  27487  pntrsumbnd2  27494  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem5  27508  pntrlog2bndlem6a  27509  pntrlog2bndlem6  27510  pntrlog2bnd  27511  pntpbnd1a  27512  pntpbnd1  27513  pntpbnd2  27514  pntibndlem1  27516  pntibndlem2  27518  pntibndlem3  27519  pntibnd  27520  pntlemc  27522  pntlema  27523  pntlemb  27524  pntlemg  27525  pntlemh  27526  pntlemn  27527  pntlemq  27528  pntlemr  27529  pntlemj  27530  pntlemi  27531  pntlemf  27532  pntlemk  27533  pntlemo  27534  pntleme  27535  pntlem3  27536  pntlemp  27537  pntleml  27538  ostth2lem1  27545  ostth2lem3  27562  ostth2  27564  ostth3  27565  crctcshwlkn0lem5  29777  nrt2irr  30435  smcnlem  30659  blocnilem  30766  blocni  30767  ubthlem2  30833  minvecolem3  30838  minvecolem4  30842  minvecolem5  30843  nmcexi  31988  lnconi  31995  fsumub  32786  sgnmulrp2  32794  rpxdivcld  32887  constrinvcl  33739  constrsqrtcl  33745  sqsscirc1  33874  cnre2csqlem  33876  tpr2rico  33878  xrmulc1cn  33896  xrge0iifiso  33901  xrge0iifhom  33903  esumcst  34029  esumdivc  34049  dya2icoseg  34244  omssubaddlem  34266  omssubadd  34267  probmeasb  34397  signsply0  34518  logdivsqrle  34617  hgt750leme  34625  dnicn  36465  unblimceq0lem  36479  unbdqndv2lem1  36482  unbdqndv2lem2  36483  knoppndvlem18  36502  knoppndvlem21  36505  poimirlem29  37628  heicant  37634  opnmbllem0  37635  mblfinlem3  37638  itg2addnclem3  37652  itg2addnc  37653  itggt0cn  37669  ftc1cnnclem  37670  ftc1anclem6  37677  ftc1anclem7  37678  geomcau  37738  sstotbnd2  37753  isbnd3  37763  equivbnd  37769  prdsbnd2  37774  cntotbnd  37775  heibor1lem  37788  heiborlem6  37795  bfplem1  37801  bfplem2  37802  bfp  37803  rrndstprj2  37810  rrnequiv  37814  lcmineqlem21  42022  aks4d1p1p4  42044  aks4d1p1p7  42047  aks4d1p5  42053  aks4d1p6  42054  aks6d1c2  42103  fltnlta  42636  irrapxlem4  42798  irrapxlem5  42799  irrapx1  42801  pell1qrgaplem  42846  pell14qrgapw  42849  pellqrexplicit  42850  pellqrex  42852  pellfundge  42855  pellfundgt1  42856  rmspecfund  42882  rmxycomplete  42890  rmxypos  42920  binomcxplemnotnn0  44329  suprltrp  45308  supxrge  45318  infrpge  45331  infleinflem1  45350  xralrple4  45353  recnnltrp  45357  rpgtrecnn  45360  cvgcaule  45471  fmul01lt1lem1  45566  fmul01lt1lem2  45567  ltmod  45620  lptre2pt  45622  addlimc  45630  0ellimcdiv  45631  limclner  45633  climleltrp  45658  climisp  45728  climxrrelem  45731  climxrre  45732  limsupgtlem  45759  liminfltlem  45786  cnrefiisplem  45811  climxlim2lem  45827  dvdivbd  45905  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  itgiccshift  45962  itgperiod  45963  stoweidlem1  45983  stoweidlem3  45985  stoweidlem5  45987  stoweidlem7  45989  stoweidlem11  45993  stoweidlem13  45995  stoweidlem14  45996  stoweidlem24  46006  stoweidlem25  46007  stoweidlem26  46008  stoweidlem34  46016  stoweidlem41  46023  stoweidlem42  46024  stoweidlem49  46031  stoweidlem51  46033  stoweidlem52  46034  stoweidlem59  46041  stoweidlem60  46042  stoweidlem62  46044  stoweid  46045  wallispilem5  46051  stirlinglem1  46056  stirlinglem4  46059  stirlinglem5  46060  stirlinglem6  46061  dirkercncflem1  46085  fourierdlem30  46119  fourierdlem39  46128  fourierdlem47  46135  fourierdlem73  46161  fourierdlem81  46169  fourierdlem87  46175  fourierdlem103  46191  fourierdlem104  46192  fourierdlem107  46195  rrndistlt  46272  qndenserrnbllem  46276  sge0ltfirp  46382  sge0rpcpnf  46403  sge0xaddlem1  46415  omeiunltfirp  46501  carageniuncllem2  46504  ovnsubaddlem1  46552  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hoiqssbllem1  46604  hoiqssbllem2  46605  hoiqssbllem3  46606  hspmbllem2  46609  hspmbllem3  46610  ovolval5lem1  46634  ovolval5lem2  46635  iinhoiicc  46656  vonioolem1  46662  pimrecltpos  46690  smflimlem3  46755  smfmullem1  46773  smfmullem2  46774  smfmullem3  46775  modexp2m1d  47597  dignn0flhalflem1  48601  itsclc0yqsol  48750  amgmwlem  49788  amgmw2d  49790  young2d  49791