Theorem rpred 12977

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-rp 12934

This theorem is referenced by:  rpxrd  12978  rpcnd  12979  rpregt0d  12983  rprege0d  12984  rprene0d  12985  rprecred  12988  ltmulgt11d  13012  ltmulgt12d  13013  gt0divd  13014  ge0divd  13015  lediv12ad  13036  prodge0rd  13042  xlemul1  13233  xov1plusxeqvd  13442  ltexp2a  14119  rpexpmord  14121  expcan  14122  ltexp2  14123  leexp2a  14125  expnlbnd2  14187  expmulnbnd  14188  exp11nnd  14214  01sqrexlem6  15200  cau3lem  15308  rlimcld2  15531  addcn2  15547  mulcn2  15549  reccn2  15550  o1rlimmul  15572  rlimno1  15607  caucvgrlem  15626  isumrpcl  15799  isumltss  15804  expcnv  15820  mertenslem1  15840  effsumlt  16069  recoshcl  16116  eirrlem  16162  rpnnen2lem11  16182  bitsmod  16396  prmreclem3  16880  prmreclem5  16882  4sqlem7  16906  ssblex  24403  metss2lem  24486  methaus  24495  met1stc  24496  met2ndci  24497  metustto  24528  metustexhalf  24531  nlmvscnlem2  24660  nlmvscnlem1  24661  nrginvrcnlem  24666  nmoi2  24705  nghmcn  24720  reperflem  24794  iccntr  24797  icccmplem2  24799  reconnlem2  24803  opnreen  24807  metdcnlem  24812  metnrmlem3  24837  addcnlem  24840  cnheibor  24932  cnllycmp  24933  lebnumlem3  24940  lebnumii  24943  nmoleub2lem  25091  nmoleub2lem3  25092  nmoleub2lem2  25093  nmoleub3  25096  nmhmcn  25097  ipcnlem2  25221  ipcnlem1  25222  lmnn  25240  iscfil3  25250  cfilfcls  25251  iscmet3lem1  25268  iscmet3lem2  25269  bcthlem4  25304  bcthlem5  25305  minveclem3b  25405  minveclem3  25406  ivthlem2  25429  ovolgelb  25457  ovollb2lem  25465  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliunlem2  25480  ovolscalem1  25490  ioombl1lem2  25536  ioombl1lem4  25538  uniioombllem1  25558  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  opnmbllem  25578  volcn  25583  vitalilem4  25588  itg2mulclem  25723  itg2monolem3  25729  itg2cnlem2  25739  itg2cn  25740  itggt0  25821  dveflem  25956  dvferm1lem  25961  dvferm2lem  25963  lhop1lem  25990  lhop1  25991  lhop  25993  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  dvfsumrlim  26008  ftc1a  26014  ftc1lem4  26016  plyeq0lem  26185  aalioulem2  26310  aalioulem4  26312  aalioulem5  26313  aalioulem6  26314  aaliou  26315  aaliou2b  26318  aaliou3lem1  26319  aaliou3lem2  26320  aaliou3lem8  26322  aaliou3lem5  26324  aaliou3lem7  26326  aaliou3lem9  26327  ulmcn  26377  ulmdvlem1  26378  mtest  26382  itgulm  26386  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  abelthlem7  26416  pilem2  26430  divlogrlim  26612  logcnlem3  26621  logcnlem4  26622  logccv  26640  divcxp  26664  cxplt  26671  cxple2  26674  recxpf1lem  26706  cxpcn3lem  26724  cxpaddlelem  26728  cxpaddle  26729  loglesqrt  26738  leibpi  26919  rlimcnp3  26944  cxplim  26949  rlimcxp  26951  cxp2limlem  26953  cxp2lim  26954  cxploglim  26955  cxploglim2  26956  divsqrtsumlem  26957  jensenlem2  26965  logdifbnd  26971  emcllem4  26976  harmonicbnd4  26988  fsumharmonic  26989  zetacvg  26992  lgamgulmlem2  27007  lgamgulmlem5  27010  lgamucov  27015  regamcl  27038  relgamcl  27039  ftalem1  27050  ftalem2  27051  ftalem3  27052  ftalem5  27054  basellem1  27058  basellem3  27060  basellem4  27061  basellem8  27065  chtwordi  27133  chpchtsum  27196  logfacrlim  27201  logexprlim  27202  bclbnd  27257  efexple  27258  bposlem1  27261  bposlem2  27262  bposlem6  27266  bposlem7  27267  chebbnd1lem3  27448  chebbnd1  27449  chtppilimlem1  27450  chtppilimlem2  27451  chpo1ubb  27458  rplogsumlem1  27461  rplogsumlem2  27462  dchrisum0lem1a  27463  rpvmasumlem  27464  dchrisumlem2  27467  dchrisumlem3  27468  dchrmusumlema  27470  dchrmusum2  27471  dchrvmasumlem1  27472  dchrvmasum2lem  27473  dchrvmasumlema  27477  dchrvmasumiflem1  27478  dchrisum0fno1  27488  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2  27495  dchrisum0lem3  27496  dchrisum0  27497  mulogsumlem  27508  logdivsum  27510  mulog2sumlem2  27512  vmalogdivsum2  27515  2vmadivsumlem  27517  log2sumbnd  27521  selberglem2  27523  selberg  27525  selberg2lem  27527  chpdifbndlem1  27530  chpdifbndlem2  27531  selberg3lem1  27534  selberg4lem1  27537  pntrsumbnd2  27544  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem5  27558  pntrlog2bndlem6a  27559  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntpbnd1a  27562  pntpbnd1  27563  pntpbnd2  27564  pntibndlem1  27566  pntibndlem2  27568  pntibndlem3  27569  pntibnd  27570  pntlemc  27572  pntlema  27573  pntlemb  27574  pntlemg  27575  pntlemh  27576  pntlemn  27577  pntlemq  27578  pntlemr  27579  pntlemj  27580  pntlemi  27581  pntlemf  27582  pntlemk  27583  pntlemo  27584  pntleme  27585  pntlem3  27586  pntlemp  27587  pntleml  27588  ostth2lem1  27595  ostth2lem3  27612  ostth2  27614  ostth3  27615  crctcshwlkn0lem5  29897  nrt2irr  30558  smcnlem  30783  blocnilem  30890  blocni  30891  ubthlem2  30957  minvecolem3  30962  minvecolem4  30966  minvecolem5  30967  nmcexi  32112  lnconi  32119  fsumub  32916  sgnmulrp2  32924  rpxdivcld  33008  constrinvcl  33933  constrsqrtcl  33939  sqsscirc1  34068  cnre2csqlem  34070  tpr2rico  34072  xrmulc1cn  34090  xrge0iifiso  34095  xrge0iifhom  34097  esumcst  34223  esumdivc  34243  dya2icoseg  34437  omssubaddlem  34459  omssubadd  34460  probmeasb  34590  signsply0  34711  logdivsqrle  34810  hgt750leme  34818  dnicn  36768  unblimceq0lem  36782  unbdqndv2lem1  36785  unbdqndv2lem2  36786  knoppndvlem18  36805  knoppndvlem21  36808  poimirlem29  37984  heicant  37990  opnmbllem0  37991  mblfinlem3  37994  itg2addnclem3  38008  itg2addnc  38009  itggt0cn  38025  ftc1cnnclem  38026  ftc1anclem6  38033  ftc1anclem7  38034  geomcau  38094  sstotbnd2  38109  isbnd3  38119  equivbnd  38125  prdsbnd2  38130  cntotbnd  38131  heibor1lem  38144  heiborlem6  38151  bfplem1  38157  bfplem2  38158  bfp  38159  rrndstprj2  38166  rrnequiv  38170  lcmineqlem21  42502  aks4d1p1p4  42524  aks4d1p1p7  42527  aks4d1p5  42533  aks4d1p6  42534  aks6d1c2  42583  fltnlta  43110  irrapxlem4  43271  irrapxlem5  43272  irrapx1  43274  pell1qrgaplem  43319  pell14qrgapw  43322  pellqrexplicit  43323  pellqrex  43325  pellfundge  43328  pellfundgt1  43329  rmspecfund  43355  rmxycomplete  43363  rmxypos  43393  binomcxplemnotnn0  44801  suprltrp  45776  supxrge  45786  infrpge  45799  infleinflem1  45817  xralrple4  45820  recnnltrp  45824  rpgtrecnn  45827  cvgcaule  45937  fmul01lt1lem1  46032  fmul01lt1lem2  46033  ltmod  46084  lptre2pt  46086  addlimc  46094  0ellimcdiv  46095  limclner  46097  climleltrp  46122  climisp  46192  climxrrelem  46195  climxrre  46196  limsupgtlem  46223  liminfltlem  46250  cnrefiisplem  46275  climxlim2lem  46291  dvdivbd  46369  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  itgiccshift  46426  itgperiod  46427  stoweidlem1  46447  stoweidlem3  46449  stoweidlem5  46451  stoweidlem7  46453  stoweidlem11  46457  stoweidlem13  46459  stoweidlem14  46460  stoweidlem24  46470  stoweidlem25  46471  stoweidlem26  46472  stoweidlem34  46480  stoweidlem41  46487  stoweidlem42  46488  stoweidlem49  46495  stoweidlem51  46497  stoweidlem52  46498  stoweidlem59  46505  stoweidlem60  46506  stoweidlem62  46508  stoweid  46509  wallispilem5  46515  stirlinglem1  46520  stirlinglem4  46523  stirlinglem5  46524  stirlinglem6  46525  dirkercncflem1  46549  fourierdlem30  46583  fourierdlem39  46592  fourierdlem47  46599  fourierdlem73  46625  fourierdlem81  46633  fourierdlem87  46639  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  rrndistlt  46736  qndenserrnbllem  46740  sge0ltfirp  46846  sge0rpcpnf  46867  sge0xaddlem1  46879  omeiunltfirp  46965  carageniuncllem2  46968  ovnsubaddlem1  47016  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoiqssbllem1  47068  hoiqssbllem2  47069  hoiqssbllem3  47070  hspmbllem2  47073  hspmbllem3  47074  ovolval5lem1  47098  ovolval5lem2  47099  iinhoiicc  47120  vonioolem1  47126  pimrecltpos  47154  smflimlem3  47219  smfmullem1  47237  smfmullem2  47238  smfmullem3  47239  modexp2m1d  48087  dignn0flhalflem1  49103  itsclc0yqsol  49252  amgmwlem  50289  amgmw2d  50291  young2d  50292