Theorem rpred 13145

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11180  ℝ⁺crp 13101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-rp 13102

This theorem is used by:  rpxrd  13146  rpcnd  13147  rpregt0d  13151  rprege0d  13152  rprene0d  13153  rprecred  13156  ltmulgt11d  13180  ltmulgt12d  13181  gt0divd  13182  ge0divd  13183  lediv12ad  13204  prodge0rd  13210  xlemul1  13401  xov1plusxeqvd  13610  ltexp2a  14289  rpexpmord  14291  expcan  14292  ltexp2  14293  leexp2a  14295  expnlbnd2  14358  expmulnbnd  14359  exp11nnd  14385  sgnmulrp2  15241  01sqrexlem6  15394  cau3lem  15502  rlimcld2  15725  addcn2  15741  mulcn2  15743  reccn2  15744  o1rlimmul  15766  rlimno1  15801  caucvgrlem  15820  isumrpcl  15992  isumltss  15997  expcnv  16013  mertenslem1  16033  effsumlt  16259  recoshcl  16306  eirrlem  16352  rpnnen2lem11  16372  bitsmod  16586  prmreclem3  17076  prmreclem5  17078  4sqlem7  17102  ssblex  24727  metss2lem  24810  methaus  24819  met1stc  24820  met2ndci  24821  metustto  24852  metustexhalf  24855  nlmvscnlem2  24984  nlmvscnlem1  24985  nrginvrcnlem  24990  nmoi2  25029  nghmcn  25044  reperflem  25118  iccntr  25121  icccmplem2  25123  reconnlem2  25127  opnreen  25131  metdcnlem  25136  metnrmlem3  25161  addcnlem  25164  cnheibor  25256  cnllycmp  25257  lebnumlem3  25264  lebnumii  25267  nmoleub2lem  25415  nmoleub2lem3  25416  nmoleub2lem2  25417  nmoleub3  25420  nmhmcn  25421  ipcnlem2  25545  ipcnlem1  25546  lmnn  25564  iscfil3  25574  cfilfcls  25575  iscmet3lem1  25592  iscmet3lem2  25593  bcthlem4  25628  bcthlem5  25629  minveclem3b  25729  minveclem3  25730  ivthlem2  25753  ovolgelb  25781  ovollb2lem  25789  ovolunlem1a  25797  ovolunlem1  25798  ovoliunlem1  25803  ovoliunlem2  25804  ovolscalem1  25814  ioombl1lem2  25860  ioombl1lem4  25862  uniioombllem1  25882  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  opnmbllem  25902  volcn  25907  vitalilem4  25912  itg2mulclem  26047  itg2monolem3  26053  itg2cnlem2  26063  itg2cn  26064  itggt0  26144  dveflem  26279  dvferm1lem  26284  dvferm2lem  26286  lhop1lem  26313  lhop1  26314  lhop  26316  dvcnvrelem1  26317  dvcnvrelem2  26318  dvcnvre  26319  dvfsumrlim  26331  ftc1a  26337  ftc1lem4  26339  plyeq0lem  26509  aalioulem2  26642  aalioulem4  26644  aalioulem5  26645  aalioulem6  26646  aaliou  26647  aaliou2b  26650  aaliou3lem1  26651  aaliou3lem2  26652  aaliou3lem8  26654  aaliou3lem5  26656  aaliou3lem7  26658  aaliou3lem9  26659  ulmcn  26708  ulmdvlem1  26709  mtest  26713  itgulm  26717  psercn  26735  pserdvlem1  26736  pserdvlem2  26737  pserdv  26738  abelthlem7  26747  pilem2  26761  divlogrlim  26945  logcnlem3  26954  logcnlem4  26955  logccv  26973  divcxp  26997  cxplt  27004  cxple2  27007  recxpf1lem  27039  cxpcn3lem  27057  cxpaddlelem  27061  cxpaddle  27062  loglesqrt  27071  leibpi  27252  rlimcnp3  27277  cxplim  27281  rlimcxp  27283  cxp2limlem  27285  cxp2lim  27286  cxploglim  27287  cxploglim2  27288  divsqrtsumlem  27289  jensenlem2  27297  logdifbnd  27303  emcllem4  27308  harmonicbnd4  27320  fsumharmonic  27321  zetacvg  27324  lgamgulmlem2  27339  lgamgulmlem5  27342  lgamucov  27347  regamcl  27370  relgamcl  27371  ftalem1  27382  ftalem2  27383  ftalem3  27384  ftalem5  27386  basellem1  27390  basellem3  27392  basellem4  27393  basellem8  27397  chtwordi  27465  chpchtsum  27528  logfacrlim  27533  logexprlim  27534  bclbnd  27589  efexple  27590  bposlem1  27593  bposlem2  27594  bposlem6  27598  bposlem7  27599  chebbnd1lem3  27780  chebbnd1  27781  chtppilimlem1  27782  chtppilimlem2  27783  chpo1ubb  27790  rplogsumlem1  27793  rplogsumlem2  27794  dchrisum0lem1a  27795  rpvmasumlem  27796  dchrisumlem2  27799  dchrisumlem3  27800  dchrmusumlema  27802  dchrmusum2  27803  dchrvmasumlem1  27804  dchrvmasum2lem  27805  dchrvmasumlema  27809  dchrvmasumiflem1  27810  dchrisum0fno1  27820  dchrisum0lem1b  27824  dchrisum0lem1  27825  dchrisum0lem2  27827  dchrisum0lem3  27828  dchrisum0  27829  mulogsumlem  27840  logdivsum  27842  mulog2sumlem2  27844  vmalogdivsum2  27847  2vmadivsumlem  27849  log2sumbnd  27853  selberglem2  27855  selberg  27857  selberg2lem  27859  chpdifbndlem1  27862  chpdifbndlem2  27863  selberg3lem1  27866  selberg4lem1  27869  pntrsumbnd2  27876  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem5  27890  pntrlog2bndlem6a  27891  pntrlog2bndlem6  27892  pntrlog2bnd  27893  pntpbnd1a  27894  pntpbnd1  27895  pntpbnd2  27896  pntibndlem1  27898  pntibndlem2  27900  pntibndlem3  27901  pntibnd  27902  pntlemc  27904  pntlema  27905  pntlemb  27906  pntlemg  27907  pntlemh  27908  pntlemn  27909  pntlemq  27910  pntlemr  27911  pntlemj  27912  pntlemi  27913  pntlemf  27914  pntlemk  27915  pntlemo  27916  pntleme  27917  pntlem3  27918  pntlemp  27919  pntleml  27920  ostth2lem1  27927  ostth2lem3  27944  ostth2  27946  ostth3  27947  crctcshwlkn0lem5  30385  nrt2irr  31056  smcnlem  31281  blocnilem  31388  blocni  31389  ubthlem2  31455  minvecolem3  31460  minvecolem4  31464  minvecolem5  31465  nmcexi  32610  lnconi  32617  fsumub  33401  rpxdivcld  33482  constrinvcl  34387  constrsqrtcl  34393  sqsscirc1  34522  cnre2csqlem  34524  tpr2rico  34526  xrmulc1cn  34544  xrge0iifiso  34549  xrge0iifhom  34551  esumcst  34677  esumdivc  34697  dya2icoseg  34892  omssubaddlem  34914  omssubadd  34915  probmeasb  35045  signsply0  35163  logdivsqrle  35262  hgt750leme  35270  dnicn  37328  unblimceq0lem  37342  unbdqndv2lem1  37345  unbdqndv2lem2  37346  knoppndvlem18  37365  knoppndvlem21  37368  poimirlem29  38535  heicant  38541  opnmbllem0  38542  mblfinlem3  38545  itg2addnclem3  38559  itg2addnc  38560  itggt0cn  38576  ftc1cnnclem  38577  ftc1anclem6  38584  ftc1anclem7  38585  geomcau  38661  sstotbnd2  38676  isbnd3  38686  equivbnd  38692  prdsbnd2  38697  cntotbnd  38698  heibor1lem  38711  heiborlem6  38718  bfplem1  38724  bfplem2  38725  bfp  38726  rrndstprj2  38733  rrnequiv  38737  lcmineqlem21  43067  aks4d1p1p4  43089  aks4d1p1p7  43092  aks4d1p5  43098  aks4d1p6  43099  aks6d1c2  43148  fltnlta  43628  irrapxlem4  43785  irrapxlem5  43786  irrapx1  43788  pell1qrgaplem  43833  pell14qrgapw  43836  pellqrexplicit  43837  pellqrex  43839  pellfundge  43842  pellfundgt1  43843  rmspecfund  43869  rmxycomplete  43877  rmxypos  43907  binomcxplemnotnn0  45299  suprltrp  46284  supxrge  46294  infrpge  46307  infleinflem1  46325  xralrple4  46328  recnnltrp  46332  rpgtrecnn  46335  cvgcaule  46445  fmul01lt1lem1  46540  fmul01lt1lem2  46541  ltmod  46592  lptre2pt  46594  addlimc  46602  0ellimcdiv  46603  limclner  46605  climleltrp  46630  climisp  46700  climxrrelem  46703  climxrre  46704  limsupgtlem  46731  liminfltlem  46758  cnrefiisplem  46783  climxlim2lem  46799  dvdivbd  46877  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  itgiccshift  46934  itgperiod  46935  stoweidlem1  46955  stoweidlem3  46957  stoweidlem5  46959  stoweidlem7  46961  stoweidlem11  46965  stoweidlem13  46967  stoweidlem14  46968  stoweidlem24  46978  stoweidlem25  46979  stoweidlem26  46980  stoweidlem34  46988  stoweidlem41  46995  stoweidlem42  46996  stoweidlem49  47003  stoweidlem51  47005  stoweidlem52  47006  stoweidlem59  47013  stoweidlem60  47014  stoweidlem62  47016  stoweid  47017  wallispilem5  47023  stirlinglem1  47028  stirlinglem4  47031  stirlinglem5  47032  stirlinglem6  47033  dirkercncflem1  47057  fourierdlem30  47091  fourierdlem39  47100  fourierdlem47  47107  fourierdlem73  47133  fourierdlem81  47141  fourierdlem87  47147  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  rrndistlt  47244  qndenserrnbllem  47248  sge0ltfirp  47354  sge0rpcpnf  47375  sge0xaddlem1  47387  omeiunltfirp  47473  carageniuncllem2  47476  ovnsubaddlem1  47524  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  hoiqssbllem1  47576  hoiqssbllem2  47577  hoiqssbllem3  47578  hspmbllem2  47581  hspmbllem3  47582  ovolval5lem1  47606  ovolval5lem2  47607  iinhoiicc  47628  vonioolem1  47634  pimrecltpos  47662  smflimlem3  47727  smfmullem1  47745  smfmullem2  47746  smfmullem3  47747  modexp2m1d  48641  dignn0flhalflem1  49671  itsclc0yqsol  49820  amgmwlem  50931  amgmw2d  50933  young2d  50934