Theorem rpred 13167

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11202  ℝ⁺crp 13123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-rp 13124

This theorem is used by:  rpxrd  13168  rpcnd  13169  rpregt0d  13173  rprege0d  13174  rprene0d  13175  rprecred  13178  ltmulgt11d  13202  ltmulgt12d  13203  gt0divd  13204  ge0divd  13205  lediv12ad  13226  prodge0rd  13232  xlemul1  13423  xov1plusxeqvd  13632  ltexp2a  14312  rpexpmord  14314  expcan  14315  ltexp2  14316  leexp2a  14318  expnlbnd2  14381  expmulnbnd  14382  exp11nnd  14408  sgnmulrp2  15266  01sqrexlem6  15419  cau3lem  15527  rlimcld2  15750  addcn2  15766  mulcn2  15768  reccn2  15769  o1rlimmul  15791  rlimno1  15826  caucvgrlem  15845  isumrpcl  16017  isumltss  16022  expcnv  16038  mertenslem1  16058  effsumlt  16284  recoshcl  16331  eirrlem  16377  rpnnen2lem11  16397  bitsmod  16611  prmreclem3  17101  prmreclem5  17103  4sqlem7  17127  ssblex  24752  metss2lem  24835  methaus  24844  met1stc  24845  met2ndci  24846  metustto  24877  metustexhalf  24880  nlmvscnlem2  25009  nlmvscnlem1  25010  nrginvrcnlem  25015  nmoi2  25054  nghmcn  25069  reperflem  25143  iccntr  25146  icccmplem2  25148  reconnlem2  25152  opnreen  25156  metdcnlem  25161  metnrmlem3  25186  addcnlem  25189  cnheibor  25281  cnllycmp  25282  lebnumlem3  25289  lebnumii  25292  nmoleub2lem  25440  nmoleub2lem3  25441  nmoleub2lem2  25442  nmoleub3  25445  nmhmcn  25446  ipcnlem2  25570  ipcnlem1  25571  lmnn  25589  iscfil3  25599  cfilfcls  25600  iscmet3lem1  25617  iscmet3lem2  25618  bcthlem4  25653  bcthlem5  25654  minveclem3b  25754  minveclem3  25755  ivthlem2  25778  ovolgelb  25806  ovollb2lem  25814  ovolunlem1a  25822  ovolunlem1  25823  ovoliunlem1  25828  ovoliunlem2  25829  ovolscalem1  25839  ioombl1lem2  25885  ioombl1lem4  25887  uniioombllem1  25907  uniioombllem3  25911  uniioombllem4  25912  uniioombllem5  25913  opnmbllem  25927  volcn  25932  vitalilem4  25937  itg2mulclem  26072  itg2monolem3  26078  itg2cnlem2  26088  itg2cn  26089  itggt0  26169  dveflem  26304  dvferm1lem  26309  dvferm2lem  26311  lhop1lem  26338  lhop1  26339  lhop  26341  dvcnvrelem1  26342  dvcnvrelem2  26343  dvcnvre  26344  dvfsumrlim  26356  ftc1a  26362  ftc1lem4  26364  plyeq0lem  26534  aalioulem2  26665  aalioulem4  26667  aalioulem5  26668  aalioulem6  26669  aaliou  26670  aaliou2b  26673  aaliou3lem1  26674  aaliou3lem2  26675  aaliou3lem8  26677  aaliou3lem5  26679  aaliou3lem7  26681  aaliou3lem9  26682  ulmcn  26731  ulmdvlem1  26732  mtest  26736  itgulm  26740  psercn  26758  pserdvlem1  26759  pserdvlem2  26760  pserdv  26761  abelthlem7  26770  pilem2  26784  divlogrlim  26968  logcnlem3  26977  logcnlem4  26978  logccv  26996  divcxp  27020  cxplt  27027  cxple2  27030  recxpf1lem  27062  cxpcn3lem  27080  cxpaddlelem  27084  cxpaddle  27085  loglesqrt  27094  leibpi  27275  rlimcnp3  27300  cxplim  27304  rlimcxp  27306  cxp2limlem  27308  cxp2lim  27309  cxploglim  27310  cxploglim2  27311  divsqrtsumlem  27312  jensenlem2  27320  logdifbnd  27326  emcllem4  27331  harmonicbnd4  27343  fsumharmonic  27344  zetacvg  27347  lgamgulmlem2  27362  lgamgulmlem5  27365  lgamucov  27370  regamcl  27393  relgamcl  27394  ftalem1  27405  ftalem2  27406  ftalem3  27407  ftalem5  27409  basellem1  27413  basellem3  27415  basellem4  27416  basellem8  27420  chtwordi  27488  chpchtsum  27551  logfacrlim  27556  logexprlim  27557  bclbnd  27612  efexple  27613  bposlem1  27616  bposlem2  27617  bposlem6  27621  bposlem7  27622  chebbnd1lem3  27803  chebbnd1  27804  chtppilimlem1  27805  chtppilimlem2  27806  chpo1ubb  27813  rplogsumlem1  27816  rplogsumlem2  27817  dchrisum0lem1a  27818  rpvmasumlem  27819  dchrisumlem2  27822  dchrisumlem3  27823  dchrmusumlema  27825  dchrmusum2  27826  dchrvmasumlem1  27827  dchrvmasum2lem  27828  dchrvmasumlema  27832  dchrvmasumiflem1  27833  dchrisum0fno1  27843  dchrisum0lem1b  27847  dchrisum0lem1  27848  dchrisum0lem2  27850  dchrisum0lem3  27851  dchrisum0  27852  mulogsumlem  27863  logdivsum  27865  mulog2sumlem2  27867  vmalogdivsum2  27870  2vmadivsumlem  27872  log2sumbnd  27876  selberglem2  27878  selberg  27880  selberg2lem  27882  chpdifbndlem1  27885  chpdifbndlem2  27886  selberg3lem1  27889  selberg4lem1  27892  pntrsumbnd2  27899  pntrlog2bndlem2  27910  pntrlog2bndlem3  27911  pntrlog2bndlem5  27913  pntrlog2bndlem6a  27914  pntrlog2bndlem6  27915  pntrlog2bnd  27916  pntpbnd1a  27917  pntpbnd1  27918  pntpbnd2  27919  pntibndlem1  27921  pntibndlem2  27923  pntibndlem3  27924  pntibnd  27925  pntlemc  27927  pntlema  27928  pntlemb  27929  pntlemg  27930  pntlemh  27931  pntlemn  27932  pntlemq  27933  pntlemr  27934  pntlemj  27935  pntlemi  27936  pntlemf  27937  pntlemk  27938  pntlemo  27939  pntleme  27940  pntlem3  27941  pntlemp  27942  pntleml  27943  ostth2lem1  27950  ostth2lem3  27967  ostth2  27969  ostth3  27970  crctcshwlkn0lem5  30408  nrt2irr  31079  smcnlem  31304  blocnilem  31411  blocni  31412  ubthlem2  31478  minvecolem3  31483  minvecolem4  31487  minvecolem5  31488  nmcexi  32633  lnconi  32640  fsumub  33465  rpxdivcld  33546  constrinvcl  34451  constrsqrtcl  34457  sqsscirc1  34586  cnre2csqlem  34588  tpr2rico  34590  xrmulc1cn  34608  xrge0iifiso  34613  xrge0iifhom  34615  esumcst  34741  esumdivc  34761  dya2icoseg  34955  omssubaddlem  34977  omssubadd  34978  probmeasb  35108  signsply0  35226  logdivsqrle  35325  hgt750leme  35333  dnicn  37450  unblimceq0lem  37464  unbdqndv2lem1  37467  unbdqndv2lem2  37468  knoppndvlem18  37487  knoppndvlem21  37490  poimirlem29  38660  heicant  38666  opnmbllem0  38667  mblfinlem3  38670  itg2addnclem3  38684  itg2addnc  38685  itggt0cn  38701  ftc1cnnclem  38702  ftc1anclem6  38709  ftc1anclem7  38710  geomcau  38786  sstotbnd2  38801  isbnd3  38811  equivbnd  38817  prdsbnd2  38822  cntotbnd  38823  heibor1lem  38836  heiborlem6  38843  bfplem1  38849  bfplem2  38850  bfp  38851  rrndstprj2  38858  rrnequiv  38862  lcmineqlem21  43192  aks4d1p1p4  43214  aks4d1p1p7  43217  aks4d1p5  43223  aks4d1p6  43224  aks6d1c2  43273  fltnlta  43767  irrapxlem4  43925  irrapxlem5  43926  irrapx1  43928  pell1qrgaplem  43973  pell14qrgapw  43976  pellqrexplicit  43977  pellqrex  43979  pellfundge  43982  pellfundgt1  43983  rmspecfund  44009  rmxycomplete  44017  rmxypos  44047  binomcxplemnotnn0  45433  suprltrp  46433  supxrge  46443  infrpge  46456  infleinflem1  46474  xralrple4  46477  recnnltrp  46481  rpgtrecnn  46484  cvgcaule  46594  fmul01lt1lem1  46689  fmul01lt1lem2  46690  ltmod  46741  lptre2pt  46743  addlimc  46751  0ellimcdiv  46752  limclner  46754  climleltrp  46779  climisp  46849  climxrrelem  46852  climxrre  46853  limsupgtlem  46880  liminfltlem  46907  cnrefiisplem  46932  climxlim2lem  46948  dvdivbd  47026  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  itgiccshift  47083  itgperiod  47084  stoweidlem1  47104  stoweidlem3  47106  stoweidlem5  47108  stoweidlem7  47110  stoweidlem11  47114  stoweidlem13  47116  stoweidlem14  47117  stoweidlem24  47127  stoweidlem25  47128  stoweidlem26  47129  stoweidlem34  47137  stoweidlem41  47144  stoweidlem42  47145  stoweidlem49  47152  stoweidlem51  47154  stoweidlem52  47155  stoweidlem59  47162  stoweidlem60  47163  stoweidlem62  47165  stoweid  47166  wallispilem5  47172  stirlinglem1  47177  stirlinglem4  47180  stirlinglem5  47181  stirlinglem6  47182  dirkercncflem1  47206  fourierdlem30  47240  fourierdlem39  47249  fourierdlem47  47256  fourierdlem73  47282  fourierdlem81  47290  fourierdlem87  47296  fourierdlem103  47312  fourierdlem104  47313  fourierdlem107  47316  rrndistlt  47393  qndenserrnbllem  47397  sge0ltfirp  47503  sge0rpcpnf  47524  sge0xaddlem1  47536  omeiunltfirp  47622  carageniuncllem2  47625  ovnsubaddlem1  47673  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  hoidmvlelem4  47701  hoiqssbllem1  47725  hoiqssbllem2  47726  hoiqssbllem3  47727  hspmbllem2  47730  hspmbllem3  47731  ovolval5lem1  47755  ovolval5lem2  47756  iinhoiicc  47777  vonioolem1  47783  pimrecltpos  47811  smflimlem3  47876  smfmullem1  47894  smfmullem2  47895  smfmullem3  47896  modexp2m1d  48790  dignn0flhalflem1  49820  itsclc0yqsol  49969  amgmwlem  51155  amgmw2d  51157  young2d  51158