Theorem rpred 12781

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  ℝ⁺crp 12739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905  df-rp 12740

This theorem is referenced by:  rpxrd  12782  rpcnd  12783  rpregt0d  12787  rprege0d  12788  rprene0d  12789  rprecred  12792  ltmulgt11d  12816  ltmulgt12d  12817  gt0divd  12818  ge0divd  12819  lediv12ad  12840  prodge0rd  12846  xlemul1  13033  xov1plusxeqvd  13239  ltexp2a  13893  rpexpmord  13895  expcan  13896  ltexp2  13897  leexp2a  13899  expnlbnd2  13958  expmulnbnd  13959  sqrlem6  14968  cau3lem  15075  rlimcld2  15296  addcn2  15312  mulcn2  15314  reccn2  15315  o1rlimmul  15337  rlimno1  15374  caucvgrlem  15393  isumrpcl  15564  isumltss  15569  expcnv  15585  mertenslem1  15605  effsumlt  15829  recoshcl  15876  eirrlem  15922  rpnnen2lem11  15942  bitsmod  16152  prmreclem3  16628  prmreclem5  16630  4sqlem7  16654  ssblex  23590  metss2lem  23676  methaus  23685  met1stc  23686  met2ndci  23687  metustto  23718  metustexhalf  23721  nlmvscnlem2  23858  nlmvscnlem1  23859  nrginvrcnlem  23864  nmoi2  23903  nghmcn  23918  reperflem  23990  iccntr  23993  icccmplem2  23995  reconnlem2  23999  opnreen  24003  metdcnlem  24008  metnrmlem3  24033  addcnlem  24036  cnheibor  24127  cnllycmp  24128  lebnumlem3  24135  lebnumii  24138  nmoleub2lem  24286  nmoleub2lem3  24287  nmoleub2lem2  24288  nmoleub3  24291  nmhmcn  24292  ipcnlem2  24417  ipcnlem1  24418  lmnn  24436  iscfil3  24446  cfilfcls  24447  iscmet3lem1  24464  iscmet3lem2  24465  bcthlem4  24500  bcthlem5  24501  minveclem3b  24601  minveclem3  24602  ivthlem2  24625  ovolgelb  24653  ovollb2lem  24661  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliunlem2  24676  ovolscalem1  24686  ioombl1lem2  24732  ioombl1lem4  24734  uniioombllem1  24754  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  opnmbllem  24774  volcn  24779  vitalilem4  24784  itg2mulclem  24920  itg2monolem3  24926  itg2cnlem2  24936  itg2cn  24937  itggt0  25017  dveflem  25152  dvferm1lem  25157  dvferm2lem  25159  lhop1lem  25186  lhop1  25187  lhop  25189  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcnvre  25192  dvfsumrlim  25204  ftc1a  25210  ftc1lem4  25212  plyeq0lem  25380  aalioulem2  25502  aalioulem4  25504  aalioulem5  25505  aalioulem6  25506  aaliou  25507  aaliou2b  25510  aaliou3lem1  25511  aaliou3lem2  25512  aaliou3lem8  25514  aaliou3lem5  25516  aaliou3lem7  25518  aaliou3lem9  25519  ulmcn  25567  ulmdvlem1  25568  mtest  25572  itgulm  25576  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  pserdv  25597  abelthlem7  25606  pilem2  25620  divlogrlim  25799  logcnlem3  25808  logcnlem4  25809  logccv  25827  divcxp  25851  cxplt  25858  cxple2  25861  cxpcn3lem  25909  cxpaddlelem  25913  cxpaddle  25914  loglesqrt  25920  leibpi  26101  rlimcnp3  26126  cxplim  26130  rlimcxp  26132  cxp2limlem  26134  cxp2lim  26135  cxploglim  26136  cxploglim2  26137  divsqrtsumlem  26138  jensenlem2  26146  logdifbnd  26152  emcllem4  26157  harmonicbnd4  26169  fsumharmonic  26170  zetacvg  26173  lgamgulmlem2  26188  lgamgulmlem5  26191  lgamucov  26196  regamcl  26219  relgamcl  26220  ftalem1  26231  ftalem2  26232  ftalem3  26233  ftalem5  26235  basellem1  26239  basellem3  26241  basellem4  26242  basellem8  26246  chtwordi  26314  chpchtsum  26376  logfacrlim  26381  logexprlim  26382  bclbnd  26437  efexple  26438  bposlem1  26441  bposlem2  26442  bposlem6  26446  bposlem7  26447  chebbnd1lem3  26628  chebbnd1  26629  chtppilimlem1  26630  chtppilimlem2  26631  chpo1ubb  26638  rplogsumlem1  26641  rplogsumlem2  26642  dchrisum0lem1a  26643  rpvmasumlem  26644  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasumlema  26657  dchrvmasumiflem1  26658  dchrisum0fno1  26668  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2  26675  dchrisum0lem3  26676  dchrisum0  26677  mulogsumlem  26688  logdivsum  26690  mulog2sumlem2  26692  vmalogdivsum2  26695  2vmadivsumlem  26697  log2sumbnd  26701  selberglem2  26703  selberg  26705  selberg2lem  26707  chpdifbndlem1  26710  chpdifbndlem2  26711  selberg3lem1  26714  selberg4lem1  26717  pntrsumbnd2  26724  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem5  26738  pntrlog2bndlem6a  26739  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem1  26746  pntibndlem2  26748  pntibndlem3  26749  pntibnd  26750  pntlemc  26752  pntlema  26753  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemn  26757  pntlemq  26758  pntlemr  26759  pntlemj  26760  pntlemi  26761  pntlemf  26762  pntlemk  26763  pntlemo  26764  pntleme  26765  pntlem3  26766  pntlemp  26767  pntleml  26768  ostth2lem1  26775  ostth2lem3  26792  ostth2  26794  ostth3  26795  crctcshwlkn0lem5  28188  smcnlem  29068  blocnilem  29175  blocni  29176  ubthlem2  29242  minvecolem3  29247  minvecolem4  29251  minvecolem5  29252  nmcexi  30397  lnconi  30404  fsumub  31151  rpxdivcld  31217  sqsscirc1  31867  cnre2csqlem  31869  tpr2rico  31871  xrmulc1cn  31889  xrge0iifiso  31894  xrge0iifhom  31896  esumcst  32040  esumdivc  32060  dya2icoseg  32253  omssubaddlem  32275  omssubadd  32276  probmeasb  32406  sgnmulrp2  32519  signsply0  32539  logdivsqrle  32639  hgt750leme  32647  dnicn  34681  unblimceq0lem  34695  unbdqndv2lem1  34698  unbdqndv2lem2  34699  knoppndvlem18  34718  knoppndvlem21  34721  poimirlem29  35815  heicant  35821  opnmbllem0  35822  mblfinlem3  35825  itg2addnclem3  35839  itg2addnc  35840  itggt0cn  35856  ftc1cnnclem  35857  ftc1anclem6  35864  ftc1anclem7  35865  geomcau  35926  sstotbnd2  35941  isbnd3  35951  equivbnd  35957  prdsbnd2  35962  cntotbnd  35963  heibor1lem  35976  heiborlem6  35983  bfplem1  35989  bfplem2  35990  bfp  35991  rrndstprj2  35998  rrnequiv  36002  lcmineqlem21  40064  aks4d1p1p4  40086  aks4d1p1p7  40089  aks4d1p5  40095  aks4d1p6  40096  exp11nnd  40331  fltnlta  40507  irrapxlem4  40654  irrapxlem5  40655  irrapx1  40657  pell1qrgaplem  40702  pell14qrgapw  40705  pellqrexplicit  40706  pellqrex  40708  pellfundge  40711  pellfundgt1  40712  rmspecfund  40738  rmxycomplete  40746  rmxypos  40776  binomcxplemnotnn0  41981  suprltrp  42874  supxrge  42884  infrpge  42897  infleinflem1  42916  xralrple4  42919  recnnltrp  42923  rpgtrecnn  42926  fmul01lt1lem1  43132  fmul01lt1lem2  43133  ltmod  43186  lptre2pt  43188  addlimc  43196  0ellimcdiv  43197  limclner  43199  climleltrp  43224  climisp  43294  climxrrelem  43297  climxrre  43298  limsupgtlem  43325  liminfltlem  43352  cnrefiisplem  43377  climxlim2lem  43393  dvdivbd  43471  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  itgiccshift  43528  itgperiod  43529  stoweidlem1  43549  stoweidlem3  43551  stoweidlem5  43553  stoweidlem7  43555  stoweidlem11  43559  stoweidlem13  43561  stoweidlem14  43562  stoweidlem24  43572  stoweidlem25  43573  stoweidlem26  43574  stoweidlem34  43582  stoweidlem41  43589  stoweidlem42  43590  stoweidlem49  43597  stoweidlem51  43599  stoweidlem52  43600  stoweidlem59  43607  stoweidlem60  43608  stoweidlem62  43610  stoweid  43611  wallispilem5  43617  stirlinglem1  43622  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  dirkercncflem1  43651  fourierdlem30  43685  fourierdlem39  43694  fourierdlem47  43701  fourierdlem73  43727  fourierdlem81  43735  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  rrndistlt  43838  qndenserrnbllem  43842  sge0ltfirp  43945  sge0rpcpnf  43966  sge0xaddlem1  43978  omeiunltfirp  44064  carageniuncllem2  44067  ovnsubaddlem1  44115  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoiqssbllem1  44167  hoiqssbllem2  44168  hoiqssbllem3  44169  hspmbllem2  44172  hspmbllem3  44173  ovolval5lem1  44197  ovolval5lem2  44198  iinhoiicc  44219  vonioolem1  44225  pimrecltpos  44253  smflimlem3  44318  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  modexp2m1d  45075  dignn0flhalflem1  45972  itsclc0yqsol  46121  amgmwlem  46517  amgmw2d  46519  young2d  46520