Theorem rpred 12949

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℝ⁺crp 12905

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918  df-rp 12906

This theorem is referenced by:  rpxrd  12950  rpcnd  12951  rpregt0d  12955  rprege0d  12956  rprene0d  12957  rprecred  12960  ltmulgt11d  12984  ltmulgt12d  12985  gt0divd  12986  ge0divd  12987  lediv12ad  13008  prodge0rd  13014  xlemul1  13205  xov1plusxeqvd  13414  ltexp2a  14089  rpexpmord  14091  expcan  14092  ltexp2  14093  leexp2a  14095  expnlbnd2  14157  expmulnbnd  14158  exp11nnd  14184  01sqrexlem6  15170  cau3lem  15278  rlimcld2  15501  addcn2  15517  mulcn2  15519  reccn2  15520  o1rlimmul  15542  rlimno1  15577  caucvgrlem  15596  isumrpcl  15766  isumltss  15771  expcnv  15787  mertenslem1  15807  effsumlt  16036  recoshcl  16083  eirrlem  16129  rpnnen2lem11  16149  bitsmod  16363  prmreclem3  16846  prmreclem5  16848  4sqlem7  16872  ssblex  24372  metss2lem  24455  methaus  24464  met1stc  24465  met2ndci  24466  metustto  24497  metustexhalf  24500  nlmvscnlem2  24629  nlmvscnlem1  24630  nrginvrcnlem  24635  nmoi2  24674  nghmcn  24689  reperflem  24763  iccntr  24766  icccmplem2  24768  reconnlem2  24772  opnreen  24776  metdcnlem  24781  metnrmlem3  24806  addcnlem  24809  cnheibor  24910  cnllycmp  24911  lebnumlem3  24918  lebnumii  24921  nmoleub2lem  25070  nmoleub2lem3  25071  nmoleub2lem2  25072  nmoleub3  25075  nmhmcn  25076  ipcnlem2  25200  ipcnlem1  25201  lmnn  25219  iscfil3  25229  cfilfcls  25230  iscmet3lem1  25247  iscmet3lem2  25248  bcthlem4  25283  bcthlem5  25284  minveclem3b  25384  minveclem3  25385  ivthlem2  25409  ovolgelb  25437  ovollb2lem  25445  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliunlem2  25460  ovolscalem1  25470  ioombl1lem2  25516  ioombl1lem4  25518  uniioombllem1  25538  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  opnmbllem  25558  volcn  25563  vitalilem4  25568  itg2mulclem  25703  itg2monolem3  25709  itg2cnlem2  25719  itg2cn  25720  itggt0  25801  dveflem  25939  dvferm1lem  25944  dvferm2lem  25946  lhop1lem  25974  lhop1  25975  lhop  25977  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcnvre  25980  dvfsumrlim  25994  ftc1a  26000  ftc1lem4  26002  plyeq0lem  26171  aalioulem2  26297  aalioulem4  26299  aalioulem5  26300  aalioulem6  26301  aaliou  26302  aaliou2b  26305  aaliou3lem1  26306  aaliou3lem2  26307  aaliou3lem8  26309  aaliou3lem5  26311  aaliou3lem7  26313  aaliou3lem9  26314  ulmcn  26364  ulmdvlem1  26365  mtest  26369  itgulm  26373  psercn  26392  pserdvlem1  26393  pserdvlem2  26394  pserdv  26395  abelthlem7  26404  pilem2  26418  divlogrlim  26600  logcnlem3  26609  logcnlem4  26610  logccv  26628  divcxp  26652  cxplt  26659  cxple2  26662  recxpf1lem  26694  cxpcn3lem  26713  cxpaddlelem  26717  cxpaddle  26718  loglesqrt  26727  leibpi  26908  rlimcnp3  26933  cxplim  26938  rlimcxp  26940  cxp2limlem  26942  cxp2lim  26943  cxploglim  26944  cxploglim2  26945  divsqrtsumlem  26946  jensenlem2  26954  logdifbnd  26960  emcllem4  26965  harmonicbnd4  26977  fsumharmonic  26978  zetacvg  26981  lgamgulmlem2  26996  lgamgulmlem5  26999  lgamucov  27004  regamcl  27027  relgamcl  27028  ftalem1  27039  ftalem2  27040  ftalem3  27041  ftalem5  27043  basellem1  27047  basellem3  27049  basellem4  27050  basellem8  27054  chtwordi  27122  chpchtsum  27186  logfacrlim  27191  logexprlim  27192  bclbnd  27247  efexple  27248  bposlem1  27251  bposlem2  27252  bposlem6  27256  bposlem7  27257  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chpo1ubb  27448  rplogsumlem1  27451  rplogsumlem2  27452  dchrisum0lem1a  27453  rpvmasumlem  27454  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasumlema  27467  dchrvmasumiflem1  27468  dchrisum0fno1  27478  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2  27485  dchrisum0lem3  27486  dchrisum0  27487  mulogsumlem  27498  logdivsum  27500  mulog2sumlem2  27502  vmalogdivsum2  27505  2vmadivsumlem  27507  log2sumbnd  27511  selberglem2  27513  selberg  27515  selberg2lem  27517  chpdifbndlem1  27520  chpdifbndlem2  27521  selberg3lem1  27524  selberg4lem1  27527  pntrsumbnd2  27534  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntrlog2bndlem6a  27549  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem1  27556  pntibndlem2  27558  pntibndlem3  27559  pntibnd  27560  pntlemc  27562  pntlema  27563  pntlemb  27564  pntlemg  27565  pntlemh  27566  pntlemn  27567  pntlemq  27568  pntlemr  27569  pntlemj  27570  pntlemi  27571  pntlemf  27572  pntlemk  27573  pntlemo  27574  pntleme  27575  pntlem3  27576  pntlemp  27577  pntleml  27578  ostth2lem1  27585  ostth2lem3  27602  ostth2  27604  ostth3  27605  crctcshwlkn0lem5  29887  nrt2irr  30548  smcnlem  30772  blocnilem  30879  blocni  30880  ubthlem2  30946  minvecolem3  30951  minvecolem4  30955  minvecolem5  30956  nmcexi  32101  lnconi  32108  fsumub  32909  sgnmulrp2  32917  rpxdivcld  33015  constrinvcl  33930  constrsqrtcl  33936  sqsscirc1  34065  cnre2csqlem  34067  tpr2rico  34069  xrmulc1cn  34087  xrge0iifiso  34092  xrge0iifhom  34094  esumcst  34220  esumdivc  34240  dya2icoseg  34434  omssubaddlem  34456  omssubadd  34457  probmeasb  34587  signsply0  34708  logdivsqrle  34807  hgt750leme  34815  dnicn  36692  unblimceq0lem  36706  unbdqndv2lem1  36709  unbdqndv2lem2  36710  knoppndvlem18  36729  knoppndvlem21  36732  poimirlem29  37846  heicant  37852  opnmbllem0  37853  mblfinlem3  37856  itg2addnclem3  37870  itg2addnc  37871  itggt0cn  37887  ftc1cnnclem  37888  ftc1anclem6  37895  ftc1anclem7  37896  geomcau  37956  sstotbnd2  37971  isbnd3  37981  equivbnd  37987  prdsbnd2  37992  cntotbnd  37993  heibor1lem  38006  heiborlem6  38013  bfplem1  38019  bfplem2  38020  bfp  38021  rrndstprj2  38028  rrnequiv  38032  lcmineqlem21  42299  aks4d1p1p4  42321  aks4d1p1p7  42324  aks4d1p5  42330  aks4d1p6  42331  aks6d1c2  42380  fltnlta  42902  irrapxlem4  43063  irrapxlem5  43064  irrapx1  43066  pell1qrgaplem  43111  pell14qrgapw  43114  pellqrexplicit  43115  pellqrex  43117  pellfundge  43120  pellfundgt1  43121  rmspecfund  43147  rmxycomplete  43155  rmxypos  43185  binomcxplemnotnn0  44593  suprltrp  45569  supxrge  45579  infrpge  45592  infleinflem1  45610  xralrple4  45613  recnnltrp  45617  rpgtrecnn  45620  cvgcaule  45731  fmul01lt1lem1  45826  fmul01lt1lem2  45827  ltmod  45878  lptre2pt  45880  addlimc  45888  0ellimcdiv  45889  limclner  45891  climleltrp  45916  climisp  45986  climxrrelem  45989  climxrre  45990  limsupgtlem  46017  liminfltlem  46044  cnrefiisplem  46069  climxlim2lem  46085  dvdivbd  46163  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  itgiccshift  46220  itgperiod  46221  stoweidlem1  46241  stoweidlem3  46243  stoweidlem5  46245  stoweidlem7  46247  stoweidlem11  46251  stoweidlem13  46253  stoweidlem14  46254  stoweidlem24  46264  stoweidlem25  46265  stoweidlem26  46266  stoweidlem34  46274  stoweidlem41  46281  stoweidlem42  46282  stoweidlem49  46289  stoweidlem51  46291  stoweidlem52  46292  stoweidlem59  46299  stoweidlem60  46300  stoweidlem62  46302  stoweid  46303  wallispilem5  46309  stirlinglem1  46314  stirlinglem4  46317  stirlinglem5  46318  stirlinglem6  46319  dirkercncflem1  46343  fourierdlem30  46377  fourierdlem39  46386  fourierdlem47  46393  fourierdlem73  46419  fourierdlem81  46427  fourierdlem87  46433  fourierdlem103  46449  fourierdlem104  46450  fourierdlem107  46453  rrndistlt  46530  qndenserrnbllem  46534  sge0ltfirp  46640  sge0rpcpnf  46661  sge0xaddlem1  46673  omeiunltfirp  46759  carageniuncllem2  46762  ovnsubaddlem1  46810  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hoiqssbllem1  46862  hoiqssbllem2  46863  hoiqssbllem3  46864  hspmbllem2  46867  hspmbllem3  46868  ovolval5lem1  46892  ovolval5lem2  46893  iinhoiicc  46914  vonioolem1  46920  pimrecltpos  46948  smflimlem3  47013  smfmullem1  47031  smfmullem2  47032  smfmullem3  47033  modexp2m1d  47854  dignn0flhalflem1  48857  itsclc0yqsol  49006  amgmwlem  50043  amgmw2d  50045  young2d  50046