Theorem rpred 12432

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  ℝ⁺crp 12390

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3943  df-ss 3952  df-rp 12391

This theorem is referenced by:  rpxrd  12433  rpcnd  12434  rpregt0d  12438  rprege0d  12439  rprene0d  12440  rprecred  12443  ltmulgt11d  12467  ltmulgt12d  12468  gt0divd  12469  ge0divd  12470  lediv12ad  12491  prodge0rd  12497  xlemul1  12684  xov1plusxeqvd  12885  ltexp2a  13531  rpexpmord  13533  expcan  13534  ltexp2  13535  leexp2a  13537  expnlbnd2  13596  expmulnbnd  13597  sqrlem6  14607  cau3lem  14714  rlimcld2  14935  addcn2  14950  mulcn2  14952  reccn2  14953  o1rlimmul  14975  rlimno1  15010  caucvgrlem  15029  isumrpcl  15198  isumltss  15203  expcnv  15219  mertenslem1  15240  effsumlt  15464  recoshcl  15511  eirrlem  15557  rpnnen2lem11  15577  bitsmod  15785  prmreclem3  16254  prmreclem5  16256  4sqlem7  16280  ssblex  23038  metss2lem  23121  methaus  23130  met1stc  23131  met2ndci  23132  metustto  23163  metustexhalf  23166  nlmvscnlem2  23294  nlmvscnlem1  23295  nrginvrcnlem  23300  nmoi2  23339  nghmcn  23354  reperflem  23426  iccntr  23429  icccmplem2  23431  reconnlem2  23435  opnreen  23439  metdcnlem  23444  metnrmlem3  23469  addcnlem  23472  cnheibor  23559  cnllycmp  23560  lebnumlem3  23567  lebnumii  23570  nmoleub2lem  23718  nmoleub2lem3  23719  nmoleub2lem2  23720  nmoleub3  23723  nmhmcn  23724  ipcnlem2  23847  ipcnlem1  23848  lmnn  23866  iscfil3  23876  cfilfcls  23877  iscmet3lem1  23894  iscmet3lem2  23895  bcthlem4  23930  bcthlem5  23931  minveclem3b  24031  minveclem3  24032  ivthlem2  24053  ovolgelb  24081  ovollb2lem  24089  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliunlem2  24104  ovolscalem1  24114  ioombl1lem2  24160  ioombl1lem4  24162  uniioombllem1  24182  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  opnmbllem  24202  volcn  24207  vitalilem4  24212  itg2mulclem  24347  itg2monolem3  24353  itg2cnlem2  24363  itg2cn  24364  itggt0  24442  dveflem  24576  dvferm1lem  24581  dvferm2lem  24583  lhop1lem  24610  lhop1  24611  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvfsumrlim  24628  ftc1a  24634  ftc1lem4  24636  plyeq0lem  24800  aalioulem2  24922  aalioulem4  24924  aalioulem5  24925  aalioulem6  24926  aaliou  24927  aaliou2b  24930  aaliou3lem1  24931  aaliou3lem2  24932  aaliou3lem8  24934  aaliou3lem5  24936  aaliou3lem7  24938  aaliou3lem9  24939  ulmcn  24987  ulmdvlem1  24988  mtest  24992  itgulm  24996  psercn  25014  pserdvlem1  25015  pserdvlem2  25016  pserdv  25017  abelthlem7  25026  pilem2  25040  divlogrlim  25218  logcnlem3  25227  logcnlem4  25228  logccv  25246  divcxp  25270  cxplt  25277  cxple2  25280  cxpcn3lem  25328  cxpaddlelem  25332  cxpaddle  25333  loglesqrt  25339  leibpi  25520  rlimcnp3  25545  cxplim  25549  rlimcxp  25551  cxp2limlem  25553  cxp2lim  25554  cxploglim  25555  cxploglim2  25556  divsqrtsumlem  25557  jensenlem2  25565  logdifbnd  25571  emcllem4  25576  harmonicbnd4  25588  fsumharmonic  25589  zetacvg  25592  lgamgulmlem2  25607  lgamgulmlem5  25610  lgamucov  25615  regamcl  25638  relgamcl  25639  ftalem1  25650  ftalem2  25651  ftalem3  25652  ftalem5  25654  basellem1  25658  basellem3  25660  basellem4  25661  basellem8  25665  chtwordi  25733  chpchtsum  25795  logfacrlim  25800  logexprlim  25801  bclbnd  25856  efexple  25857  bposlem1  25860  bposlem2  25861  bposlem6  25865  bposlem7  25866  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chpo1ubb  26057  rplogsumlem1  26060  rplogsumlem2  26061  dchrisum0lem1a  26062  rpvmasumlem  26063  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0fno1  26087  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2  26094  dchrisum0lem3  26095  dchrisum0  26096  mulogsumlem  26107  logdivsum  26109  mulog2sumlem2  26111  vmalogdivsum2  26114  2vmadivsumlem  26116  log2sumbnd  26120  selberglem2  26122  selberg  26124  selberg2lem  26126  chpdifbndlem1  26129  chpdifbndlem2  26130  selberg3lem1  26133  selberg4lem1  26136  pntrsumbnd2  26143  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntrlog2bndlem6a  26158  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem1  26165  pntibndlem2  26167  pntibndlem3  26168  pntibnd  26169  pntlemc  26171  pntlema  26172  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemn  26176  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemi  26180  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntleme  26184  pntlem3  26185  pntlemp  26186  pntleml  26187  ostth2lem1  26194  ostth2lem3  26211  ostth2  26213  ostth3  26214  crctcshwlkn0lem5  27592  smcnlem  28474  blocnilem  28581  blocni  28582  ubthlem2  28648  minvecolem3  28653  minvecolem4  28657  minvecolem5  28658  nmcexi  29803  lnconi  29810  fsumub  30544  rpxdivcld  30610  sqsscirc1  31151  cnre2csqlem  31153  tpr2rico  31155  xrmulc1cn  31173  xrge0iifiso  31178  xrge0iifhom  31180  esumcst  31322  esumdivc  31342  dya2icoseg  31535  omssubaddlem  31557  omssubadd  31558  probmeasb  31688  sgnmulrp2  31801  signsply0  31821  logdivsqrle  31921  hgt750leme  31929  dnicn  33831  unblimceq0lem  33845  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem18  33868  knoppndvlem21  33871  poimirlem29  34936  heicant  34942  opnmbllem0  34943  mblfinlem3  34946  itg2addnclem3  34960  itg2addnc  34961  itggt0cn  34979  ftc1cnnclem  34980  ftc1anclem6  34987  ftc1anclem7  34988  geomcau  35049  sstotbnd2  35067  isbnd3  35077  equivbnd  35083  prdsbnd2  35088  cntotbnd  35089  heibor1lem  35102  heiborlem6  35109  bfplem1  35115  bfplem2  35116  bfp  35117  rrndstprj2  35124  rrnequiv  35128  fltnlta  39324  irrapxlem4  39471  irrapxlem5  39472  irrapx1  39474  pell1qrgaplem  39519  pell14qrgapw  39522  pellqrexplicit  39523  pellqrex  39525  pellfundge  39528  pellfundgt1  39529  rmspecfund  39555  rmxycomplete  39563  rmxypos  39593  binomcxplemnotnn0  40737  suprltrp  41645  supxrge  41655  infrpge  41668  infleinflem1  41687  xralrple4  41690  recnnltrp  41694  rpgtrecnn  41698  fmul01lt1lem1  41914  fmul01lt1lem2  41915  ltmod  41968  lptre2pt  41970  addlimc  41978  0ellimcdiv  41979  limclner  41981  climleltrp  42006  climisp  42076  climxrrelem  42079  climxrre  42080  limsupgtlem  42107  liminfltlem  42134  cnrefiisplem  42159  climxlim2lem  42175  dvdivbd  42257  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  itgiccshift  42314  itgperiod  42315  stoweidlem1  42335  stoweidlem3  42337  stoweidlem5  42339  stoweidlem7  42341  stoweidlem11  42345  stoweidlem13  42347  stoweidlem14  42348  stoweidlem24  42358  stoweidlem25  42359  stoweidlem26  42360  stoweidlem34  42368  stoweidlem41  42375  stoweidlem42  42376  stoweidlem49  42383  stoweidlem51  42385  stoweidlem52  42386  stoweidlem59  42393  stoweidlem60  42394  stoweidlem62  42396  stoweid  42397  wallispilem5  42403  stirlinglem1  42408  stirlinglem4  42411  stirlinglem5  42412  stirlinglem6  42413  dirkercncflem1  42437  fourierdlem30  42471  fourierdlem39  42480  fourierdlem47  42487  fourierdlem73  42513  fourierdlem81  42521  fourierdlem87  42527  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  rrndistlt  42624  qndenserrnbllem  42628  sge0ltfirp  42731  sge0rpcpnf  42752  sge0xaddlem1  42764  omeiunltfirp  42850  carageniuncllem2  42853  ovnsubaddlem1  42901  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoiqssbllem1  42953  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem2  42958  hspmbllem3  42959  ovolval5lem1  42983  ovolval5lem2  42984  iinhoiicc  43005  vonioolem1  43011  pimrecltpos  43036  smflimlem3  43098  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  modexp2m1d  43826  dignn0flhalflem1  44724  itsclc0yqsol  44800  amgmwlem  44952  amgmw2d  44954  young2d  44955