Theorem rpred 13075

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 11152  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-ss 3980  df-rp 13033

This theorem is referenced by:  rpxrd  13076  rpcnd  13077  rpregt0d  13081  rprege0d  13082  rprene0d  13083  rprecred  13086  ltmulgt11d  13110  ltmulgt12d  13111  gt0divd  13112  ge0divd  13113  lediv12ad  13134  prodge0rd  13140  xlemul1  13329  xov1plusxeqvd  13535  ltexp2a  14203  rpexpmord  14205  expcan  14206  ltexp2  14207  leexp2a  14209  expnlbnd2  14270  expmulnbnd  14271  exp11nnd  14297  01sqrexlem6  15283  cau3lem  15390  rlimcld2  15611  addcn2  15627  mulcn2  15629  reccn2  15630  o1rlimmul  15652  rlimno1  15687  caucvgrlem  15706  isumrpcl  15876  isumltss  15881  expcnv  15897  mertenslem1  15917  effsumlt  16144  recoshcl  16191  eirrlem  16237  rpnnen2lem11  16257  bitsmod  16470  prmreclem3  16952  prmreclem5  16954  4sqlem7  16978  ssblex  24454  metss2lem  24540  methaus  24549  met1stc  24550  met2ndci  24551  metustto  24582  metustexhalf  24585  nlmvscnlem2  24722  nlmvscnlem1  24723  nrginvrcnlem  24728  nmoi2  24767  nghmcn  24782  reperflem  24854  iccntr  24857  icccmplem2  24859  reconnlem2  24863  opnreen  24867  metdcnlem  24872  metnrmlem3  24897  addcnlem  24900  cnheibor  25001  cnllycmp  25002  lebnumlem3  25009  lebnumii  25012  nmoleub2lem  25161  nmoleub2lem3  25162  nmoleub2lem2  25163  nmoleub3  25166  nmhmcn  25167  ipcnlem2  25292  ipcnlem1  25293  lmnn  25311  iscfil3  25321  cfilfcls  25322  iscmet3lem1  25339  iscmet3lem2  25340  bcthlem4  25375  bcthlem5  25376  minveclem3b  25476  minveclem3  25477  ivthlem2  25501  ovolgelb  25529  ovollb2lem  25537  ovolunlem1a  25545  ovolunlem1  25546  ovoliunlem1  25551  ovoliunlem2  25552  ovolscalem1  25562  ioombl1lem2  25608  ioombl1lem4  25610  uniioombllem1  25630  uniioombllem3  25634  uniioombllem4  25635  uniioombllem5  25636  opnmbllem  25650  volcn  25655  vitalilem4  25660  itg2mulclem  25796  itg2monolem3  25802  itg2cnlem2  25812  itg2cn  25813  itggt0  25894  dveflem  26032  dvferm1lem  26037  dvferm2lem  26039  lhop1lem  26067  lhop1  26068  lhop  26070  dvcnvrelem1  26071  dvcnvrelem2  26072  dvcnvre  26073  dvfsumrlim  26087  ftc1a  26093  ftc1lem4  26095  plyeq0lem  26264  aalioulem2  26390  aalioulem4  26392  aalioulem5  26393  aalioulem6  26394  aaliou  26395  aaliou2b  26398  aaliou3lem1  26399  aaliou3lem2  26400  aaliou3lem8  26402  aaliou3lem5  26404  aaliou3lem7  26406  aaliou3lem9  26407  ulmcn  26457  ulmdvlem1  26458  mtest  26462  itgulm  26466  psercn  26485  pserdvlem1  26486  pserdvlem2  26487  pserdv  26488  abelthlem7  26497  pilem2  26511  divlogrlim  26692  logcnlem3  26701  logcnlem4  26702  logccv  26720  divcxp  26744  cxplt  26751  cxple2  26754  recxpf1lem  26786  cxpcn3lem  26805  cxpaddlelem  26809  cxpaddle  26810  loglesqrt  26819  leibpi  27000  rlimcnp3  27025  cxplim  27030  rlimcxp  27032  cxp2limlem  27034  cxp2lim  27035  cxploglim  27036  cxploglim2  27037  divsqrtsumlem  27038  jensenlem2  27046  logdifbnd  27052  emcllem4  27057  harmonicbnd4  27069  fsumharmonic  27070  zetacvg  27073  lgamgulmlem2  27088  lgamgulmlem5  27091  lgamucov  27096  regamcl  27119  relgamcl  27120  ftalem1  27131  ftalem2  27132  ftalem3  27133  ftalem5  27135  basellem1  27139  basellem3  27141  basellem4  27142  basellem8  27146  chtwordi  27214  chpchtsum  27278  logfacrlim  27283  logexprlim  27284  bclbnd  27339  efexple  27340  bposlem1  27343  bposlem2  27344  bposlem6  27348  bposlem7  27349  chebbnd1lem3  27530  chebbnd1  27531  chtppilimlem1  27532  chtppilimlem2  27533  chpo1ubb  27540  rplogsumlem1  27543  rplogsumlem2  27544  dchrisum0lem1a  27545  rpvmasumlem  27546  dchrisumlem2  27549  dchrisumlem3  27550  dchrmusumlema  27552  dchrmusum2  27553  dchrvmasumlem1  27554  dchrvmasum2lem  27555  dchrvmasumlema  27559  dchrvmasumiflem1  27560  dchrisum0fno1  27570  dchrisum0lem1b  27574  dchrisum0lem1  27575  dchrisum0lem2  27577  dchrisum0lem3  27578  dchrisum0  27579  mulogsumlem  27590  logdivsum  27592  mulog2sumlem2  27594  vmalogdivsum2  27597  2vmadivsumlem  27599  log2sumbnd  27603  selberglem2  27605  selberg  27607  selberg2lem  27609  chpdifbndlem1  27612  chpdifbndlem2  27613  selberg3lem1  27616  selberg4lem1  27619  pntrsumbnd2  27626  pntrlog2bndlem2  27637  pntrlog2bndlem3  27638  pntrlog2bndlem5  27640  pntrlog2bndlem6a  27641  pntrlog2bndlem6  27642  pntrlog2bnd  27643  pntpbnd1a  27644  pntpbnd1  27645  pntpbnd2  27646  pntibndlem1  27648  pntibndlem2  27650  pntibndlem3  27651  pntibnd  27652  pntlemc  27654  pntlema  27655  pntlemb  27656  pntlemg  27657  pntlemh  27658  pntlemn  27659  pntlemq  27660  pntlemr  27661  pntlemj  27662  pntlemi  27663  pntlemf  27664  pntlemk  27665  pntlemo  27666  pntleme  27667  pntlem3  27668  pntlemp  27669  pntleml  27670  ostth2lem1  27677  ostth2lem3  27694  ostth2  27696  ostth3  27697  crctcshwlkn0lem5  29844  nrt2irr  30502  smcnlem  30726  blocnilem  30833  blocni  30834  ubthlem2  30900  minvecolem3  30905  minvecolem4  30909  minvecolem5  30910  nmcexi  32055  lnconi  32062  fsumub  32835  rpxdivcld  32901  sqsscirc1  33869  cnre2csqlem  33871  tpr2rico  33873  xrmulc1cn  33891  xrge0iifiso  33896  xrge0iifhom  33898  esumcst  34044  esumdivc  34064  dya2icoseg  34259  omssubaddlem  34281  omssubadd  34282  probmeasb  34412  sgnmulrp2  34525  signsply0  34545  logdivsqrle  34644  hgt750leme  34652  dnicn  36475  unblimceq0lem  36489  unbdqndv2lem1  36492  unbdqndv2lem2  36493  knoppndvlem18  36512  knoppndvlem21  36515  poimirlem29  37636  heicant  37642  opnmbllem0  37643  mblfinlem3  37646  itg2addnclem3  37660  itg2addnc  37661  itggt0cn  37677  ftc1cnnclem  37678  ftc1anclem6  37685  ftc1anclem7  37686  geomcau  37746  sstotbnd2  37761  isbnd3  37771  equivbnd  37777  prdsbnd2  37782  cntotbnd  37783  heibor1lem  37796  heiborlem6  37803  bfplem1  37809  bfplem2  37810  bfp  37811  rrndstprj2  37818  rrnequiv  37822  lcmineqlem21  42031  aks4d1p1p4  42053  aks4d1p1p7  42056  aks4d1p5  42062  aks4d1p6  42063  aks6d1c2  42112  fltnlta  42650  irrapxlem4  42813  irrapxlem5  42814  irrapx1  42816  pell1qrgaplem  42861  pell14qrgapw  42864  pellqrexplicit  42865  pellqrex  42867  pellfundge  42870  pellfundgt1  42871  rmspecfund  42897  rmxycomplete  42906  rmxypos  42936  binomcxplemnotnn0  44352  suprltrp  45278  supxrge  45288  infrpge  45301  infleinflem1  45320  xralrple4  45323  recnnltrp  45327  rpgtrecnn  45330  cvgcaule  45442  fmul01lt1lem1  45540  fmul01lt1lem2  45541  ltmod  45594  lptre2pt  45596  addlimc  45604  0ellimcdiv  45605  limclner  45607  climleltrp  45632  climisp  45702  climxrrelem  45705  climxrre  45706  limsupgtlem  45733  liminfltlem  45760  cnrefiisplem  45785  climxlim2lem  45801  dvdivbd  45879  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  itgiccshift  45936  itgperiod  45937  stoweidlem1  45957  stoweidlem3  45959  stoweidlem5  45961  stoweidlem7  45963  stoweidlem11  45967  stoweidlem13  45969  stoweidlem14  45970  stoweidlem24  45980  stoweidlem25  45981  stoweidlem26  45982  stoweidlem34  45990  stoweidlem41  45997  stoweidlem42  45998  stoweidlem49  46005  stoweidlem51  46007  stoweidlem52  46008  stoweidlem59  46015  stoweidlem60  46016  stoweidlem62  46018  stoweid  46019  wallispilem5  46025  stirlinglem1  46030  stirlinglem4  46033  stirlinglem5  46034  stirlinglem6  46035  dirkercncflem1  46059  fourierdlem30  46093  fourierdlem39  46102  fourierdlem47  46109  fourierdlem73  46135  fourierdlem81  46143  fourierdlem87  46149  fourierdlem103  46165  fourierdlem104  46166  fourierdlem107  46169  rrndistlt  46246  qndenserrnbllem  46250  sge0ltfirp  46356  sge0rpcpnf  46377  sge0xaddlem1  46389  omeiunltfirp  46475  carageniuncllem2  46478  ovnsubaddlem1  46526  hoidmvlelem1  46551  hoidmvlelem2  46552  hoidmvlelem3  46553  hoidmvlelem4  46554  hoiqssbllem1  46578  hoiqssbllem2  46579  hoiqssbllem3  46580  hspmbllem2  46583  hspmbllem3  46584  ovolval5lem1  46608  ovolval5lem2  46609  iinhoiicc  46630  vonioolem1  46636  pimrecltpos  46664  smflimlem3  46729  smfmullem1  46747  smfmullem2  46748  smfmullem3  46749  modexp2m1d  47537  dignn0flhalflem1  48465  itsclc0yqsol  48614  amgmwlem  49033  amgmw2d  49035  young2d  49036