Theorem rpred 13099

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-rp 13058

This theorem is referenced by:  rpxrd  13100  rpcnd  13101  rpregt0d  13105  rprege0d  13106  rprene0d  13107  rprecred  13110  ltmulgt11d  13134  ltmulgt12d  13135  gt0divd  13136  ge0divd  13137  lediv12ad  13158  prodge0rd  13164  xlemul1  13352  xov1plusxeqvd  13558  ltexp2a  14216  rpexpmord  14218  expcan  14219  ltexp2  14220  leexp2a  14222  expnlbnd2  14283  expmulnbnd  14284  exp11nnd  14310  01sqrexlem6  15296  cau3lem  15403  rlimcld2  15624  addcn2  15640  mulcn2  15642  reccn2  15643  o1rlimmul  15665  rlimno1  15702  caucvgrlem  15721  isumrpcl  15891  isumltss  15896  expcnv  15912  mertenslem1  15932  effsumlt  16159  recoshcl  16206  eirrlem  16252  rpnnen2lem11  16272  bitsmod  16482  prmreclem3  16965  prmreclem5  16967  4sqlem7  16991  ssblex  24459  metss2lem  24545  methaus  24554  met1stc  24555  met2ndci  24556  metustto  24587  metustexhalf  24590  nlmvscnlem2  24727  nlmvscnlem1  24728  nrginvrcnlem  24733  nmoi2  24772  nghmcn  24787  reperflem  24859  iccntr  24862  icccmplem2  24864  reconnlem2  24868  opnreen  24872  metdcnlem  24877  metnrmlem3  24902  addcnlem  24905  cnheibor  25006  cnllycmp  25007  lebnumlem3  25014  lebnumii  25017  nmoleub2lem  25166  nmoleub2lem3  25167  nmoleub2lem2  25168  nmoleub3  25171  nmhmcn  25172  ipcnlem2  25297  ipcnlem1  25298  lmnn  25316  iscfil3  25326  cfilfcls  25327  iscmet3lem1  25344  iscmet3lem2  25345  bcthlem4  25380  bcthlem5  25381  minveclem3b  25481  minveclem3  25482  ivthlem2  25506  ovolgelb  25534  ovollb2lem  25542  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliunlem2  25557  ovolscalem1  25567  ioombl1lem2  25613  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  opnmbllem  25655  volcn  25660  vitalilem4  25665  itg2mulclem  25801  itg2monolem3  25807  itg2cnlem2  25817  itg2cn  25818  itggt0  25899  dveflem  26037  dvferm1lem  26042  dvferm2lem  26044  lhop1lem  26072  lhop1  26073  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvfsumrlim  26092  ftc1a  26098  ftc1lem4  26100  plyeq0lem  26269  aalioulem2  26393  aalioulem4  26395  aalioulem5  26396  aalioulem6  26397  aaliou  26398  aaliou2b  26401  aaliou3lem1  26402  aaliou3lem2  26403  aaliou3lem8  26405  aaliou3lem5  26407  aaliou3lem7  26409  aaliou3lem9  26410  ulmcn  26460  ulmdvlem1  26461  mtest  26465  itgulm  26469  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  pserdv  26491  abelthlem7  26500  pilem2  26514  divlogrlim  26695  logcnlem3  26704  logcnlem4  26705  logccv  26723  divcxp  26747  cxplt  26754  cxple2  26757  recxpf1lem  26789  cxpcn3lem  26808  cxpaddlelem  26812  cxpaddle  26813  loglesqrt  26822  leibpi  27003  rlimcnp3  27028  cxplim  27033  rlimcxp  27035  cxp2limlem  27037  cxp2lim  27038  cxploglim  27039  cxploglim2  27040  divsqrtsumlem  27041  jensenlem2  27049  logdifbnd  27055  emcllem4  27060  harmonicbnd4  27072  fsumharmonic  27073  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem5  27094  lgamucov  27099  regamcl  27122  relgamcl  27123  ftalem1  27134  ftalem2  27135  ftalem3  27136  ftalem5  27138  basellem1  27142  basellem3  27144  basellem4  27145  basellem8  27149  chtwordi  27217  chpchtsum  27281  logfacrlim  27286  logexprlim  27287  bclbnd  27342  efexple  27343  bposlem1  27346  bposlem2  27347  bposlem6  27351  bposlem7  27352  chebbnd1lem3  27533  chebbnd1  27534  chtppilimlem1  27535  chtppilimlem2  27536  chpo1ubb  27543  rplogsumlem1  27546  rplogsumlem2  27547  dchrisum0lem1a  27548  rpvmasumlem  27549  dchrisumlem2  27552  dchrisumlem3  27553  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrisum0fno1  27573  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2  27580  dchrisum0lem3  27581  dchrisum0  27582  mulogsumlem  27593  logdivsum  27595  mulog2sumlem2  27597  vmalogdivsum2  27600  2vmadivsumlem  27602  log2sumbnd  27606  selberglem2  27608  selberg  27610  selberg2lem  27612  chpdifbndlem1  27615  chpdifbndlem2  27616  selberg3lem1  27619  selberg4lem1  27622  pntrsumbnd2  27629  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntrlog2bndlem6a  27644  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntibndlem1  27651  pntibndlem2  27653  pntibndlem3  27654  pntibnd  27655  pntlemc  27657  pntlema  27658  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemn  27662  pntlemq  27663  pntlemr  27664  pntlemj  27665  pntlemi  27666  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntleme  27670  pntlem3  27671  pntlemp  27672  pntleml  27673  ostth2lem1  27680  ostth2lem3  27697  ostth2  27699  ostth3  27700  crctcshwlkn0lem5  29847  nrt2irr  30505  smcnlem  30729  blocnilem  30836  blocni  30837  ubthlem2  30903  minvecolem3  30908  minvecolem4  30912  minvecolem5  30913  nmcexi  32058  lnconi  32065  fsumub  32832  rpxdivcld  32898  sqsscirc1  33854  cnre2csqlem  33856  tpr2rico  33858  xrmulc1cn  33876  xrge0iifiso  33881  xrge0iifhom  33883  esumcst  34027  esumdivc  34047  dya2icoseg  34242  omssubaddlem  34264  omssubadd  34265  probmeasb  34395  sgnmulrp2  34508  signsply0  34528  logdivsqrle  34627  hgt750leme  34635  dnicn  36458  unblimceq0lem  36472  unbdqndv2lem1  36475  unbdqndv2lem2  36476  knoppndvlem18  36495  knoppndvlem21  36498  poimirlem29  37609  heicant  37615  opnmbllem0  37616  mblfinlem3  37619  itg2addnclem3  37633  itg2addnc  37634  itggt0cn  37650  ftc1cnnclem  37651  ftc1anclem6  37658  ftc1anclem7  37659  geomcau  37719  sstotbnd2  37734  isbnd3  37744  equivbnd  37750  prdsbnd2  37755  cntotbnd  37756  heibor1lem  37769  heiborlem6  37776  bfplem1  37782  bfplem2  37783  bfp  37784  rrndstprj2  37791  rrnequiv  37795  lcmineqlem21  42006  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p5  42037  aks4d1p6  42038  aks6d1c2  42087  fltnlta  42618  irrapxlem4  42781  irrapxlem5  42782  irrapx1  42784  pell1qrgaplem  42829  pell14qrgapw  42832  pellqrexplicit  42833  pellqrex  42835  pellfundge  42838  pellfundgt1  42839  rmspecfund  42865  rmxycomplete  42874  rmxypos  42904  binomcxplemnotnn0  44325  suprltrp  45243  supxrge  45253  infrpge  45266  infleinflem1  45285  xralrple4  45288  recnnltrp  45292  rpgtrecnn  45295  cvgcaule  45407  fmul01lt1lem1  45505  fmul01lt1lem2  45506  ltmod  45559  lptre2pt  45561  addlimc  45569  0ellimcdiv  45570  limclner  45572  climleltrp  45597  climisp  45667  climxrrelem  45670  climxrre  45671  limsupgtlem  45698  liminfltlem  45725  cnrefiisplem  45750  climxlim2lem  45766  dvdivbd  45844  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  itgiccshift  45901  itgperiod  45902  stoweidlem1  45922  stoweidlem3  45924  stoweidlem5  45926  stoweidlem7  45928  stoweidlem11  45932  stoweidlem13  45934  stoweidlem14  45935  stoweidlem24  45945  stoweidlem25  45946  stoweidlem26  45947  stoweidlem34  45955  stoweidlem41  45962  stoweidlem42  45963  stoweidlem49  45970  stoweidlem51  45972  stoweidlem52  45973  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  stoweid  45984  wallispilem5  45990  stirlinglem1  45995  stirlinglem4  45998  stirlinglem5  45999  stirlinglem6  46000  dirkercncflem1  46024  fourierdlem30  46058  fourierdlem39  46067  fourierdlem47  46074  fourierdlem73  46100  fourierdlem81  46108  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  rrndistlt  46211  qndenserrnbllem  46215  sge0ltfirp  46321  sge0rpcpnf  46342  sge0xaddlem1  46354  omeiunltfirp  46440  carageniuncllem2  46443  ovnsubaddlem1  46491  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoiqssbllem1  46543  hoiqssbllem2  46544  hoiqssbllem3  46545  hspmbllem2  46548  hspmbllem3  46549  ovolval5lem1  46573  ovolval5lem2  46574  iinhoiicc  46595  vonioolem1  46601  pimrecltpos  46629  smflimlem3  46694  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  modexp2m1d  47486  dignn0flhalflem1  48349  itsclc0yqsol  48498  amgmwlem  48896  amgmw2d  48898  young2d  48899