Theorem rpred 12247

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

Syntax hints:   → wi 4   ∈ wcel 2051  ℝcr 10333  ℝ⁺crp 12203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-rab 3092  df-in 3831  df-ss 3838  df-rp 12204

This theorem is referenced by:  rpxrd  12248  rpcnd  12249  rpregt0d  12253  rprege0d  12254  rprene0d  12255  rprecred  12258  ltmulgt11d  12282  ltmulgt12d  12283  gt0divd  12284  ge0divd  12285  lediv12ad  12306  prodge0rd  12312  xlemul1  12498  xov1plusxeqvd  12699  ltexp2a  13344  rpexpmord  13346  expcan  13347  ltexp2  13348  leexp2a  13350  expnlbnd2  13409  expmulnbnd  13410  sqrlem6  14467  cau3lem  14574  rlimcld2  14795  addcn2  14810  mulcn2  14812  reccn2  14813  o1rlimmul  14835  rlimno1  14870  caucvgrlem  14889  isumrpcl  15057  isumltss  15062  expcnv  15078  mertenslem1  15099  effsumlt  15323  recoshcl  15370  eirrlem  15416  rpnnen2lem11  15436  bitsmod  15644  prmreclem3  16109  prmreclem5  16111  4sqlem7  16135  ssblex  22757  metss2lem  22840  methaus  22849  met1stc  22850  met2ndci  22851  metustto  22882  metustexhalf  22885  nlmvscnlem2  23013  nlmvscnlem1  23014  nrginvrcnlem  23019  nmoi2  23058  nghmcn  23073  reperflem  23145  iccntr  23148  icccmplem2  23150  reconnlem2  23154  opnreen  23158  metdcnlem  23163  metnrmlem3  23188  addcnlem  23191  cnheibor  23278  cnllycmp  23279  lebnumlem3  23286  lebnumii  23289  nmoleub2lem  23437  nmoleub2lem3  23438  nmoleub2lem2  23439  nmoleub3  23442  nmhmcn  23443  ipcnlem2  23566  ipcnlem1  23567  lmnn  23585  iscfil3  23595  cfilfcls  23596  iscmet3lem1  23613  iscmet3lem2  23614  bcthlem4  23649  bcthlem5  23650  minveclem3b  23750  minveclem3  23751  ivthlem2  23772  ovolgelb  23800  ovollb2lem  23808  ovolunlem1a  23816  ovolunlem1  23817  ovoliunlem1  23822  ovoliunlem2  23823  ovolscalem1  23833  ioombl1lem2  23879  ioombl1lem4  23881  uniioombllem1  23901  uniioombllem3  23905  uniioombllem4  23906  uniioombllem5  23907  opnmbllem  23921  volcn  23926  vitalilem4  23931  itg2mulclem  24066  itg2monolem3  24072  itg2cnlem2  24082  itg2cn  24083  itggt0  24161  dveflem  24295  dvferm1lem  24300  dvferm2lem  24302  lhop1lem  24329  lhop1  24330  lhop  24332  dvcnvrelem1  24333  dvcnvrelem2  24334  dvcnvre  24335  dvfsumrlim  24347  ftc1a  24353  ftc1lem4  24355  plyeq0lem  24519  aalioulem2  24641  aalioulem4  24643  aalioulem5  24644  aalioulem6  24645  aaliou  24646  aaliou2b  24649  aaliou3lem1  24650  aaliou3lem2  24651  aaliou3lem8  24653  aaliou3lem5  24655  aaliou3lem7  24657  aaliou3lem9  24658  ulmcn  24706  ulmdvlem1  24707  mtest  24711  itgulm  24715  psercn  24733  pserdvlem1  24734  pserdvlem2  24735  pserdv  24736  abelthlem7  24745  pilem2  24759  divlogrlim  24935  logcnlem3  24944  logcnlem4  24945  logccv  24963  divcxp  24987  cxplt  24994  cxple2  24997  cxpcn3lem  25045  cxpaddlelem  25049  cxpaddle  25050  loglesqrt  25056  leibpi  25238  rlimcnp3  25263  cxplim  25267  rlimcxp  25269  cxp2limlem  25271  cxp2lim  25272  cxploglim  25273  cxploglim2  25274  divsqrtsumlem  25275  jensenlem2  25283  logdifbnd  25289  emcllem4  25294  harmonicbnd4  25306  fsumharmonic  25307  zetacvg  25310  lgamgulmlem2  25325  lgamgulmlem5  25328  lgamucov  25333  regamcl  25356  relgamcl  25357  ftalem1  25368  ftalem2  25369  ftalem3  25370  ftalem5  25372  basellem1  25376  basellem3  25378  basellem4  25379  basellem8  25383  chtwordi  25451  chpchtsum  25513  logfacrlim  25518  logexprlim  25519  bclbnd  25574  efexple  25575  bposlem1  25578  bposlem2  25579  bposlem6  25583  bposlem7  25584  chebbnd1lem3  25765  chebbnd1  25766  chtppilimlem1  25767  chtppilimlem2  25768  chpo1ubb  25775  rplogsumlem1  25778  rplogsumlem2  25779  dchrisum0lem1a  25780  rpvmasumlem  25781  dchrisumlem2  25784  dchrisumlem3  25785  dchrmusumlema  25787  dchrmusum2  25788  dchrvmasumlem1  25789  dchrvmasum2lem  25790  dchrvmasumlema  25794  dchrvmasumiflem1  25795  dchrisum0fno1  25805  dchrisum0lem1b  25809  dchrisum0lem1  25810  dchrisum0lem2  25812  dchrisum0lem3  25813  dchrisum0  25814  mulogsumlem  25825  logdivsum  25827  mulog2sumlem2  25829  vmalogdivsum2  25832  2vmadivsumlem  25834  log2sumbnd  25838  selberglem2  25840  selberg  25842  selberg2lem  25844  chpdifbndlem1  25847  chpdifbndlem2  25848  selberg3lem1  25851  selberg4lem1  25854  pntrsumbnd2  25861  pntrlog2bndlem2  25872  pntrlog2bndlem3  25873  pntrlog2bndlem5  25875  pntrlog2bndlem6a  25876  pntrlog2bndlem6  25877  pntrlog2bnd  25878  pntpbnd1a  25879  pntpbnd1  25880  pntpbnd2  25881  pntibndlem1  25883  pntibndlem2  25885  pntibndlem3  25886  pntibnd  25887  pntlemc  25889  pntlema  25890  pntlemb  25891  pntlemg  25892  pntlemh  25893  pntlemn  25894  pntlemq  25895  pntlemr  25896  pntlemj  25897  pntlemi  25898  pntlemf  25899  pntlemk  25900  pntlemo  25901  pntleme  25902  pntlem3  25903  pntlemp  25904  pntleml  25905  ostth2lem1  25912  ostth2lem3  25929  ostth2  25931  ostth3  25932  crctcshwlkn0lem5  27316  smcnlem  28267  blocnilem  28374  blocni  28375  ubthlem2  28442  minvecolem3  28447  minvecolem4  28451  minvecolem5  28452  nmcexi  29600  lnconi  29607  fsumub  30315  rpxdivcld  30381  sqsscirc1  30828  cnre2csqlem  30830  tpr2rico  30832  xrmulc1cn  30850  xrge0iifiso  30855  xrge0iifhom  30857  esumcst  30999  esumdivc  31019  dya2icoseg  31213  omssubaddlem  31235  omssubadd  31236  probmeasb  31367  sgnmulrp2  31480  signsply0  31500  signshf  31539  logdivsqrle  31602  hgt750leme  31610  dnicn  33384  unblimceq0lem  33398  unbdqndv2lem1  33401  unbdqndv2lem2  33402  knoppndvlem18  33421  knoppndvlem21  33424  poimirlem29  34395  heicant  34401  opnmbllem0  34402  mblfinlem3  34405  itg2addnclem3  34419  itg2addnc  34420  itggt0cn  34438  ftc1cnnclem  34439  ftc1anclem6  34446  ftc1anclem7  34447  geomcau  34509  sstotbnd2  34527  isbnd3  34537  equivbnd  34543  prdsbnd2  34548  cntotbnd  34549  heibor1lem  34562  heiborlem6  34569  bfplem1  34575  bfplem2  34576  bfp  34577  rrndstprj2  34584  rrnequiv  34588  fltnlta  38716  irrapxlem4  38852  irrapxlem5  38853  irrapx1  38855  pell1qrgaplem  38900  pell14qrgapw  38903  pellqrexplicit  38904  pellqrex  38906  pellfundge  38909  pellfundgt1  38910  rmspecfund  38936  rmxycomplete  38944  rmxypos  38974  binomcxplemnotnn0  40138  suprltrp  41055  supxrge  41065  infrpge  41078  infleinflem1  41097  xralrple4  41100  recnnltrp  41104  rpgtrecnn  41108  fmul01lt1lem1  41326  fmul01lt1lem2  41327  ltmod  41380  lptre2pt  41382  addlimc  41390  0ellimcdiv  41391  limclner  41393  climleltrp  41418  climisp  41488  climxrrelem  41491  climxrre  41492  limsupgtlem  41519  liminfltlem  41546  cnrefiisplem  41571  climxlim2lem  41587  dvdivbd  41668  ioodvbdlimc1lem2  41677  ioodvbdlimc2lem  41679  itgiccshift  41725  itgperiod  41726  stoweidlem1  41747  stoweidlem3  41749  stoweidlem5  41751  stoweidlem7  41753  stoweidlem11  41757  stoweidlem13  41759  stoweidlem14  41760  stoweidlem24  41770  stoweidlem25  41771  stoweidlem26  41772  stoweidlem34  41780  stoweidlem41  41787  stoweidlem42  41788  stoweidlem49  41795  stoweidlem51  41797  stoweidlem52  41798  stoweidlem59  41805  stoweidlem60  41806  stoweidlem62  41808  stoweid  41809  wallispilem5  41815  stirlinglem1  41820  stirlinglem4  41823  stirlinglem5  41824  stirlinglem6  41825  dirkercncflem1  41849  fourierdlem30  41883  fourierdlem39  41892  fourierdlem47  41899  fourierdlem73  41925  fourierdlem81  41933  fourierdlem87  41939  fourierdlem103  41955  fourierdlem104  41956  fourierdlem107  41959  rrndistlt  42036  qndenserrnbllem  42040  sge0ltfirp  42143  sge0rpcpnf  42164  sge0xaddlem1  42176  omeiunltfirp  42262  carageniuncllem2  42265  ovnsubaddlem1  42313  hoidmvlelem1  42338  hoidmvlelem2  42339  hoidmvlelem3  42340  hoidmvlelem4  42341  hoiqssbllem1  42365  hoiqssbllem2  42366  hoiqssbllem3  42367  hspmbllem2  42370  hspmbllem3  42371  ovolval5lem1  42395  ovolval5lem2  42396  iinhoiicc  42417  vonioolem1  42423  pimrecltpos  42448  smflimlem3  42510  smfmullem1  42527  smfmullem2  42528  smfmullem3  42529  modexp2m1d  43175  dignn0flhalflem1  44073  itsclc0yqsol  44149  amgmwlem  44300  amgmw2d  44302  young2d  44303