Theorem rpred 12086

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

Syntax hints:   → wi 4   ∈ wcel 2156  ℝcr 10220  ℝ⁺crp 12046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-in 3776  df-ss 3783  df-rp 12047

This theorem is referenced by:  rpxrd  12087  rpcnd  12088  rpregt0d  12092  rprege0d  12093  rprene0d  12094  rprecred  12097  ltmulgt11d  12121  ltmulgt12d  12122  gt0divd  12123  ge0divd  12124  lediv12ad  12145  prodge0rd  12151  xlemul1  12338  xov1plusxeqvd  12541  ltexp2a  13135  expcan  13136  ltexp2  13137  leexp2a  13139  expnlbnd2  13218  expmulnbnd  13219  sqrlem6  14211  cau3lem  14317  rlimcld2  14532  addcn2  14547  mulcn2  14549  reccn2  14550  o1rlimmul  14572  rlimno1  14607  caucvgrlem  14626  isumrpcl  14797  isumltss  14802  expcnv  14818  mertenslem1  14837  effsumlt  15061  recoshcl  15108  eirrlem  15152  rpnnen2lem11  15173  bitsmod  15377  prmreclem3  15839  prmreclem5  15841  4sqlem7  15865  ssblex  22446  metss2lem  22529  methaus  22538  met1stc  22539  met2ndci  22540  metustto  22571  metustexhalf  22574  nlmvscnlem2  22702  nlmvscnlem1  22703  nrginvrcnlem  22708  nmoi2  22747  nghmcn  22762  reperflem  22834  iccntr  22837  icccmplem2  22839  reconnlem2  22843  opnreen  22847  metdcnlem  22852  metnrmlem3  22877  addcnlem  22880  cnheibor  22967  cnllycmp  22968  lebnumlem3  22975  lebnumii  22978  nmoleub2lem  23126  nmoleub2lem3  23127  nmoleub2lem2  23128  nmoleub3  23131  nmhmcn  23132  ipcnlem2  23255  ipcnlem1  23256  lmnn  23273  iscfil3  23283  cfilfcls  23284  iscmet3lem1  23301  iscmet3lem2  23302  bcthlem4  23336  bcthlem5  23337  minveclem3b  23411  minveclem3  23412  ivthlem2  23433  ovolgelb  23461  ovollb2lem  23469  ovolunlem1a  23477  ovolunlem1  23478  ovoliunlem1  23483  ovoliunlem2  23484  ovolscalem1  23494  ioombl1lem2  23540  ioombl1lem4  23542  uniioombllem1  23562  uniioombllem3  23566  uniioombllem4  23567  uniioombllem5  23568  opnmbllem  23582  volcn  23587  vitalilem4  23592  itg2mulclem  23727  itg2monolem3  23733  itg2cnlem2  23743  itg2cn  23744  itggt0  23822  dveflem  23956  dvferm1lem  23961  dvferm2lem  23963  lhop1lem  23990  lhop1  23991  lhop  23993  dvcnvrelem1  23994  dvcnvrelem2  23995  dvcnvre  23996  dvfsumrlim  24008  ftc1a  24014  ftc1lem4  24016  plyeq0lem  24180  aalioulem2  24302  aalioulem4  24304  aalioulem5  24305  aalioulem6  24306  aaliou  24307  aaliou2b  24310  aaliou3lem1  24311  aaliou3lem2  24312  aaliou3lem8  24314  aaliou3lem5  24316  aaliou3lem7  24318  aaliou3lem9  24319  ulmcn  24367  ulmdvlem1  24368  mtest  24372  itgulm  24376  psercn  24394  pserdvlem1  24395  pserdvlem2  24396  pserdv  24397  abelthlem7  24406  pilem2  24420  divlogrlim  24595  logcnlem3  24604  logcnlem4  24605  logccv  24623  divcxp  24647  cxplt  24654  cxple2  24657  cxpcn3lem  24702  cxpaddlelem  24706  cxpaddle  24707  loglesqrt  24713  leibpi  24883  rlimcnp3  24908  cxplim  24912  rlimcxp  24914  cxp2limlem  24916  cxp2lim  24917  cxploglim  24918  cxploglim2  24919  divsqrtsumlem  24920  jensenlem2  24928  logdifbnd  24934  emcllem4  24939  harmonicbnd4  24951  fsumharmonic  24952  zetacvg  24955  lgamgulmlem2  24970  lgamgulmlem5  24973  lgamucov  24978  regamcl  25001  relgamcl  25002  ftalem1  25013  ftalem2  25014  ftalem3  25015  ftalem5  25017  basellem1  25021  basellem3  25023  basellem4  25024  basellem8  25028  chtwordi  25096  chpchtsum  25158  logfacrlim  25163  logexprlim  25164  bclbnd  25219  efexple  25220  bposlem1  25223  bposlem2  25224  bposlem6  25228  bposlem7  25229  chebbnd1lem3  25374  chebbnd1  25375  chtppilimlem1  25376  chtppilimlem2  25377  chpo1ubb  25384  rplogsumlem1  25387  rplogsumlem2  25388  dchrisum0lem1a  25389  rpvmasumlem  25390  dchrisumlem2  25393  dchrisumlem3  25394  dchrmusumlema  25396  dchrmusum2  25397  dchrvmasumlem1  25398  dchrvmasum2lem  25399  dchrvmasumlema  25403  dchrvmasumiflem1  25404  dchrisum0fno1  25414  dchrisum0lem1b  25418  dchrisum0lem1  25419  dchrisum0lem2  25421  dchrisum0lem3  25422  dchrisum0  25423  mulogsumlem  25434  logdivsum  25436  mulog2sumlem2  25438  vmalogdivsum2  25441  2vmadivsumlem  25443  log2sumbnd  25447  selberglem2  25449  selberg  25451  selberg2lem  25453  chpdifbndlem1  25456  chpdifbndlem2  25457  selberg3lem1  25460  selberg4lem1  25463  pntrsumbnd2  25470  pntrlog2bndlem2  25481  pntrlog2bndlem3  25482  pntrlog2bndlem5  25484  pntrlog2bndlem6a  25485  pntrlog2bndlem6  25486  pntrlog2bnd  25487  pntpbnd1a  25488  pntpbnd1  25489  pntpbnd2  25490  pntibndlem1  25492  pntibndlem2  25494  pntibndlem3  25495  pntibnd  25496  pntlemc  25498  pntlema  25499  pntlemb  25500  pntlemg  25501  pntlemh  25502  pntlemn  25503  pntlemq  25504  pntlemr  25505  pntlemj  25506  pntlemi  25507  pntlemf  25508  pntlemk  25509  pntlemo  25510  pntleme  25511  pntlem3  25512  pntlemp  25513  pntleml  25514  ostth2lem1  25521  ostth2lem3  25538  ostth2  25540  ostth3  25541  crctcshwlkn0lem5  26935  smcnlem  27880  blocnilem  27987  blocni  27988  ubthlem2  28055  minvecolem3  28060  minvecolem4  28064  minvecolem5  28065  nmcexi  29213  lnconi  29220  fsumub  29901  rpxdivcld  29967  sqsscirc1  30279  cnre2csqlem  30281  tpr2rico  30283  xrmulc1cn  30301  xrge0iifiso  30306  xrge0iifhom  30308  esumcst  30450  esumdivc  30470  dya2icoseg  30664  omssubaddlem  30686  omssubadd  30687  probmeasb  30817  sgnmulrp2  30930  signsply0  30953  signshf  30990  logdivsqrle  31053  hgt750leme  31061  dnicn  32799  unblimceq0lem  32814  unbdqndv2lem1  32817  unbdqndv2lem2  32818  knoppndvlem18  32837  knoppndvlem21  32840  poimirlem29  33751  heicant  33757  opnmbllem0  33758  mblfinlem3  33761  itg2addnclem3  33775  itg2addnc  33776  itggt0cn  33794  ftc1cnnclem  33795  ftc1anclem6  33802  ftc1anclem7  33803  geomcau  33866  sstotbnd2  33884  isbnd3  33894  equivbnd  33900  prdsbnd2  33905  cntotbnd  33906  heibor1lem  33919  heiborlem6  33926  bfplem1  33932  bfplem2  33933  bfp  33934  rrndstprj2  33941  rrnequiv  33945  irrapxlem4  37891  irrapxlem5  37892  irrapx1  37894  pell1qrgaplem  37939  pell14qrgapw  37942  pellqrexplicit  37943  pellqrex  37945  pellfundge  37948  pellfundgt1  37949  rmspecfund  37975  rmxycomplete  37983  rpexpmord  38014  rmxypos  38015  binomcxplemnotnn0  39055  suprltrp  40024  supxrge  40034  infrpge  40047  infleinflem1  40066  xralrple4  40069  recnnltrp  40073  rpgtrecnn  40077  fmul01lt1lem1  40296  fmul01lt1lem2  40297  ltmod  40350  lptre2pt  40352  addlimc  40360  0ellimcdiv  40361  limclner  40363  climleltrp  40388  climisp  40458  climxrrelem  40461  climxrre  40462  limsupgtlem  40489  liminfltlem  40516  cnrefiisplem  40535  climxlim2lem  40551  dvdivbd  40618  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  itgiccshift  40675  itgperiod  40676  stoweidlem1  40697  stoweidlem3  40699  stoweidlem5  40701  stoweidlem7  40703  stoweidlem11  40707  stoweidlem13  40709  stoweidlem14  40710  stoweidlem24  40720  stoweidlem25  40721  stoweidlem26  40722  stoweidlem34  40730  stoweidlem41  40737  stoweidlem42  40738  stoweidlem49  40745  stoweidlem51  40747  stoweidlem52  40748  stoweidlem59  40755  stoweidlem60  40756  stoweidlem62  40758  stoweid  40759  wallispilem5  40765  stirlinglem1  40770  stirlinglem4  40773  stirlinglem5  40774  stirlinglem6  40775  dirkercncflem1  40799  fourierdlem30  40833  fourierdlem39  40842  fourierdlem47  40849  fourierdlem73  40875  fourierdlem81  40883  fourierdlem87  40889  fourierdlem103  40905  fourierdlem104  40906  fourierdlem107  40909  rrndistlt  40989  qndenserrnbllem  40993  sge0ltfirp  41096  sge0rpcpnf  41117  sge0xaddlem1  41129  omeiunltfirp  41215  carageniuncllem2  41218  ovnsubaddlem1  41266  hoidmvlelem1  41291  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  hoiqssbllem1  41318  hoiqssbllem2  41319  hoiqssbllem3  41320  hspmbllem2  41323  hspmbllem3  41324  ovolval5lem1  41348  ovolval5lem2  41349  iinhoiicc  41370  vonioolem1  41376  pimrecltpos  41401  smflimlem3  41463  smfmullem1  41480  smfmullem2  41481  smfmullem3  41482  modexp2m1d  42104  dignn0flhalflem1  42977  amgmwlem  43119  amgmw2d  43121  young2d  43122