Theorem rpred 12940

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11011  ℝ⁺crp 12896

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-rp 12897

This theorem is referenced by:  rpxrd  12941  rpcnd  12942  rpregt0d  12946  rprege0d  12947  rprene0d  12948  rprecred  12951  ltmulgt11d  12975  ltmulgt12d  12976  gt0divd  12977  ge0divd  12978  lediv12ad  12999  prodge0rd  13005  xlemul1  13195  xov1plusxeqvd  13404  ltexp2a  14079  rpexpmord  14081  expcan  14082  ltexp2  14083  leexp2a  14085  expnlbnd2  14147  expmulnbnd  14148  exp11nnd  14174  01sqrexlem6  15160  cau3lem  15268  rlimcld2  15491  addcn2  15507  mulcn2  15509  reccn2  15510  o1rlimmul  15532  rlimno1  15567  caucvgrlem  15586  isumrpcl  15756  isumltss  15761  expcnv  15777  mertenslem1  15797  effsumlt  16026  recoshcl  16073  eirrlem  16119  rpnnen2lem11  16139  bitsmod  16353  prmreclem3  16836  prmreclem5  16838  4sqlem7  16862  ssblex  24349  metss2lem  24432  methaus  24441  met1stc  24442  met2ndci  24443  metustto  24474  metustexhalf  24477  nlmvscnlem2  24606  nlmvscnlem1  24607  nrginvrcnlem  24612  nmoi2  24651  nghmcn  24666  reperflem  24740  iccntr  24743  icccmplem2  24745  reconnlem2  24749  opnreen  24753  metdcnlem  24758  metnrmlem3  24783  addcnlem  24786  cnheibor  24887  cnllycmp  24888  lebnumlem3  24895  lebnumii  24898  nmoleub2lem  25047  nmoleub2lem3  25048  nmoleub2lem2  25049  nmoleub3  25052  nmhmcn  25053  ipcnlem2  25177  ipcnlem1  25178  lmnn  25196  iscfil3  25206  cfilfcls  25207  iscmet3lem1  25224  iscmet3lem2  25225  bcthlem4  25260  bcthlem5  25261  minveclem3b  25361  minveclem3  25362  ivthlem2  25386  ovolgelb  25414  ovollb2lem  25422  ovolunlem1a  25430  ovolunlem1  25431  ovoliunlem1  25436  ovoliunlem2  25437  ovolscalem1  25447  ioombl1lem2  25493  ioombl1lem4  25495  uniioombllem1  25515  uniioombllem3  25519  uniioombllem4  25520  uniioombllem5  25521  opnmbllem  25535  volcn  25540  vitalilem4  25545  itg2mulclem  25680  itg2monolem3  25686  itg2cnlem2  25696  itg2cn  25697  itggt0  25778  dveflem  25916  dvferm1lem  25921  dvferm2lem  25923  lhop1lem  25951  lhop1  25952  lhop  25954  dvcnvrelem1  25955  dvcnvrelem2  25956  dvcnvre  25957  dvfsumrlim  25971  ftc1a  25977  ftc1lem4  25979  plyeq0lem  26148  aalioulem2  26274  aalioulem4  26276  aalioulem5  26277  aalioulem6  26278  aaliou  26279  aaliou2b  26282  aaliou3lem1  26283  aaliou3lem2  26284  aaliou3lem8  26286  aaliou3lem5  26288  aaliou3lem7  26290  aaliou3lem9  26291  ulmcn  26341  ulmdvlem1  26342  mtest  26346  itgulm  26350  psercn  26369  pserdvlem1  26370  pserdvlem2  26371  pserdv  26372  abelthlem7  26381  pilem2  26395  divlogrlim  26577  logcnlem3  26586  logcnlem4  26587  logccv  26605  divcxp  26629  cxplt  26636  cxple2  26639  recxpf1lem  26671  cxpcn3lem  26690  cxpaddlelem  26694  cxpaddle  26695  loglesqrt  26704  leibpi  26885  rlimcnp3  26910  cxplim  26915  rlimcxp  26917  cxp2limlem  26919  cxp2lim  26920  cxploglim  26921  cxploglim2  26922  divsqrtsumlem  26923  jensenlem2  26931  logdifbnd  26937  emcllem4  26942  harmonicbnd4  26954  fsumharmonic  26955  zetacvg  26958  lgamgulmlem2  26973  lgamgulmlem5  26976  lgamucov  26981  regamcl  27004  relgamcl  27005  ftalem1  27016  ftalem2  27017  ftalem3  27018  ftalem5  27020  basellem1  27024  basellem3  27026  basellem4  27027  basellem8  27031  chtwordi  27099  chpchtsum  27163  logfacrlim  27168  logexprlim  27169  bclbnd  27224  efexple  27225  bposlem1  27228  bposlem2  27229  bposlem6  27233  bposlem7  27234  chebbnd1lem3  27415  chebbnd1  27416  chtppilimlem1  27417  chtppilimlem2  27418  chpo1ubb  27425  rplogsumlem1  27428  rplogsumlem2  27429  dchrisum0lem1a  27430  rpvmasumlem  27431  dchrisumlem2  27434  dchrisumlem3  27435  dchrmusumlema  27437  dchrmusum2  27438  dchrvmasumlem1  27439  dchrvmasum2lem  27440  dchrvmasumlema  27444  dchrvmasumiflem1  27445  dchrisum0fno1  27455  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2  27462  dchrisum0lem3  27463  dchrisum0  27464  mulogsumlem  27475  logdivsum  27477  mulog2sumlem2  27479  vmalogdivsum2  27482  2vmadivsumlem  27484  log2sumbnd  27488  selberglem2  27490  selberg  27492  selberg2lem  27494  chpdifbndlem1  27497  chpdifbndlem2  27498  selberg3lem1  27501  selberg4lem1  27504  pntrsumbnd2  27511  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem5  27525  pntrlog2bndlem6a  27526  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem1  27533  pntibndlem2  27535  pntibndlem3  27536  pntibnd  27537  pntlemc  27539  pntlema  27540  pntlemb  27541  pntlemg  27542  pntlemh  27543  pntlemn  27544  pntlemq  27545  pntlemr  27546  pntlemj  27547  pntlemi  27548  pntlemf  27549  pntlemk  27550  pntlemo  27551  pntleme  27552  pntlem3  27553  pntlemp  27554  pntleml  27555  ostth2lem1  27562  ostth2lem3  27579  ostth2  27581  ostth3  27582  crctcshwlkn0lem5  29799  nrt2irr  30460  smcnlem  30684  blocnilem  30791  blocni  30792  ubthlem2  30858  minvecolem3  30863  minvecolem4  30867  minvecolem5  30868  nmcexi  32013  lnconi  32020  fsumub  32818  sgnmulrp2  32826  rpxdivcld  32921  constrinvcl  33793  constrsqrtcl  33799  sqsscirc1  33928  cnre2csqlem  33930  tpr2rico  33932  xrmulc1cn  33950  xrge0iifiso  33955  xrge0iifhom  33957  esumcst  34083  esumdivc  34103  dya2icoseg  34297  omssubaddlem  34319  omssubadd  34320  probmeasb  34450  signsply0  34571  logdivsqrle  34670  hgt750leme  34678  dnicn  36543  unblimceq0lem  36557  unbdqndv2lem1  36560  unbdqndv2lem2  36561  knoppndvlem18  36580  knoppndvlem21  36583  poimirlem29  37695  heicant  37701  opnmbllem0  37702  mblfinlem3  37705  itg2addnclem3  37719  itg2addnc  37720  itggt0cn  37736  ftc1cnnclem  37737  ftc1anclem6  37744  ftc1anclem7  37745  geomcau  37805  sstotbnd2  37820  isbnd3  37830  equivbnd  37836  prdsbnd2  37841  cntotbnd  37842  heibor1lem  37855  heiborlem6  37862  bfplem1  37868  bfplem2  37869  bfp  37870  rrndstprj2  37877  rrnequiv  37881  lcmineqlem21  42148  aks4d1p1p4  42170  aks4d1p1p7  42173  aks4d1p5  42179  aks4d1p6  42180  aks6d1c2  42229  fltnlta  42762  irrapxlem4  42923  irrapxlem5  42924  irrapx1  42926  pell1qrgaplem  42971  pell14qrgapw  42974  pellqrexplicit  42975  pellqrex  42977  pellfundge  42980  pellfundgt1  42981  rmspecfund  43007  rmxycomplete  43015  rmxypos  43045  binomcxplemnotnn0  44454  suprltrp  45432  supxrge  45442  infrpge  45455  infleinflem1  45473  xralrple4  45476  recnnltrp  45480  rpgtrecnn  45483  cvgcaule  45594  fmul01lt1lem1  45689  fmul01lt1lem2  45690  ltmod  45741  lptre2pt  45743  addlimc  45751  0ellimcdiv  45752  limclner  45754  climleltrp  45779  climisp  45849  climxrrelem  45852  climxrre  45853  limsupgtlem  45880  liminfltlem  45907  cnrefiisplem  45932  climxlim2lem  45948  dvdivbd  46026  ioodvbdlimc1lem2  46035  ioodvbdlimc2lem  46037  itgiccshift  46083  itgperiod  46084  stoweidlem1  46104  stoweidlem3  46106  stoweidlem5  46108  stoweidlem7  46110  stoweidlem11  46114  stoweidlem13  46116  stoweidlem14  46117  stoweidlem24  46127  stoweidlem25  46128  stoweidlem26  46129  stoweidlem34  46137  stoweidlem41  46144  stoweidlem42  46145  stoweidlem49  46152  stoweidlem51  46154  stoweidlem52  46155  stoweidlem59  46162  stoweidlem60  46163  stoweidlem62  46165  stoweid  46166  wallispilem5  46172  stirlinglem1  46177  stirlinglem4  46180  stirlinglem5  46181  stirlinglem6  46182  dirkercncflem1  46206  fourierdlem30  46240  fourierdlem39  46249  fourierdlem47  46256  fourierdlem73  46282  fourierdlem81  46290  fourierdlem87  46296  fourierdlem103  46312  fourierdlem104  46313  fourierdlem107  46316  rrndistlt  46393  qndenserrnbllem  46397  sge0ltfirp  46503  sge0rpcpnf  46524  sge0xaddlem1  46536  omeiunltfirp  46622  carageniuncllem2  46625  ovnsubaddlem1  46673  hoidmvlelem1  46698  hoidmvlelem2  46699  hoidmvlelem3  46700  hoidmvlelem4  46701  hoiqssbllem1  46725  hoiqssbllem2  46726  hoiqssbllem3  46727  hspmbllem2  46730  hspmbllem3  46731  ovolval5lem1  46755  ovolval5lem2  46756  iinhoiicc  46777  vonioolem1  46783  pimrecltpos  46811  smflimlem3  46876  smfmullem1  46894  smfmullem2  46895  smfmullem3  46896  modexp2m1d  47717  dignn0flhalflem1  48721  itsclc0yqsol  48870  amgmwlem  49908  amgmw2d  49910  young2d  49911