Theorem rpred 12593

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℝcr 10693  ℝ⁺crp 12551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-rp 12552

This theorem is referenced by:  rpxrd  12594  rpcnd  12595  rpregt0d  12599  rprege0d  12600  rprene0d  12601  rprecred  12604  ltmulgt11d  12628  ltmulgt12d  12629  gt0divd  12630  ge0divd  12631  lediv12ad  12652  prodge0rd  12658  xlemul1  12845  xov1plusxeqvd  13051  ltexp2a  13701  rpexpmord  13703  expcan  13704  ltexp2  13705  leexp2a  13707  expnlbnd2  13766  expmulnbnd  13767  sqrlem6  14776  cau3lem  14883  rlimcld2  15104  addcn2  15120  mulcn2  15122  reccn2  15123  o1rlimmul  15145  rlimno1  15182  caucvgrlem  15201  isumrpcl  15370  isumltss  15375  expcnv  15391  mertenslem1  15411  effsumlt  15635  recoshcl  15682  eirrlem  15728  rpnnen2lem11  15748  bitsmod  15958  prmreclem3  16434  prmreclem5  16436  4sqlem7  16460  ssblex  23280  metss2lem  23363  methaus  23372  met1stc  23373  met2ndci  23374  metustto  23405  metustexhalf  23408  nlmvscnlem2  23537  nlmvscnlem1  23538  nrginvrcnlem  23543  nmoi2  23582  nghmcn  23597  reperflem  23669  iccntr  23672  icccmplem2  23674  reconnlem2  23678  opnreen  23682  metdcnlem  23687  metnrmlem3  23712  addcnlem  23715  cnheibor  23806  cnllycmp  23807  lebnumlem3  23814  lebnumii  23817  nmoleub2lem  23965  nmoleub2lem3  23966  nmoleub2lem2  23967  nmoleub3  23970  nmhmcn  23971  ipcnlem2  24095  ipcnlem1  24096  lmnn  24114  iscfil3  24124  cfilfcls  24125  iscmet3lem1  24142  iscmet3lem2  24143  bcthlem4  24178  bcthlem5  24179  minveclem3b  24279  minveclem3  24280  ivthlem2  24303  ovolgelb  24331  ovollb2lem  24339  ovolunlem1a  24347  ovolunlem1  24348  ovoliunlem1  24353  ovoliunlem2  24354  ovolscalem1  24364  ioombl1lem2  24410  ioombl1lem4  24412  uniioombllem1  24432  uniioombllem3  24436  uniioombllem4  24437  uniioombllem5  24438  opnmbllem  24452  volcn  24457  vitalilem4  24462  itg2mulclem  24598  itg2monolem3  24604  itg2cnlem2  24614  itg2cn  24615  itggt0  24695  dveflem  24830  dvferm1lem  24835  dvferm2lem  24837  lhop1lem  24864  lhop1  24865  lhop  24867  dvcnvrelem1  24868  dvcnvrelem2  24869  dvcnvre  24870  dvfsumrlim  24882  ftc1a  24888  ftc1lem4  24890  plyeq0lem  25058  aalioulem2  25180  aalioulem4  25182  aalioulem5  25183  aalioulem6  25184  aaliou  25185  aaliou2b  25188  aaliou3lem1  25189  aaliou3lem2  25190  aaliou3lem8  25192  aaliou3lem5  25194  aaliou3lem7  25196  aaliou3lem9  25197  ulmcn  25245  ulmdvlem1  25246  mtest  25250  itgulm  25254  psercn  25272  pserdvlem1  25273  pserdvlem2  25274  pserdv  25275  abelthlem7  25284  pilem2  25298  divlogrlim  25477  logcnlem3  25486  logcnlem4  25487  logccv  25505  divcxp  25529  cxplt  25536  cxple2  25539  cxpcn3lem  25587  cxpaddlelem  25591  cxpaddle  25592  loglesqrt  25598  leibpi  25779  rlimcnp3  25804  cxplim  25808  rlimcxp  25810  cxp2limlem  25812  cxp2lim  25813  cxploglim  25814  cxploglim2  25815  divsqrtsumlem  25816  jensenlem2  25824  logdifbnd  25830  emcllem4  25835  harmonicbnd4  25847  fsumharmonic  25848  zetacvg  25851  lgamgulmlem2  25866  lgamgulmlem5  25869  lgamucov  25874  regamcl  25897  relgamcl  25898  ftalem1  25909  ftalem2  25910  ftalem3  25911  ftalem5  25913  basellem1  25917  basellem3  25919  basellem4  25920  basellem8  25924  chtwordi  25992  chpchtsum  26054  logfacrlim  26059  logexprlim  26060  bclbnd  26115  efexple  26116  bposlem1  26119  bposlem2  26120  bposlem6  26124  bposlem7  26125  chebbnd1lem3  26306  chebbnd1  26307  chtppilimlem1  26308  chtppilimlem2  26309  chpo1ubb  26316  rplogsumlem1  26319  rplogsumlem2  26320  dchrisum0lem1a  26321  rpvmasumlem  26322  dchrisumlem2  26325  dchrisumlem3  26326  dchrmusumlema  26328  dchrmusum2  26329  dchrvmasumlem1  26330  dchrvmasum2lem  26331  dchrvmasumlema  26335  dchrvmasumiflem1  26336  dchrisum0fno1  26346  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2  26353  dchrisum0lem3  26354  dchrisum0  26355  mulogsumlem  26366  logdivsum  26368  mulog2sumlem2  26370  vmalogdivsum2  26373  2vmadivsumlem  26375  log2sumbnd  26379  selberglem2  26381  selberg  26383  selberg2lem  26385  chpdifbndlem1  26388  chpdifbndlem2  26389  selberg3lem1  26392  selberg4lem1  26395  pntrsumbnd2  26402  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem5  26416  pntrlog2bndlem6a  26417  pntrlog2bndlem6  26418  pntrlog2bnd  26419  pntpbnd1a  26420  pntpbnd1  26421  pntpbnd2  26422  pntibndlem1  26424  pntibndlem2  26426  pntibndlem3  26427  pntibnd  26428  pntlemc  26430  pntlema  26431  pntlemb  26432  pntlemg  26433  pntlemh  26434  pntlemn  26435  pntlemq  26436  pntlemr  26437  pntlemj  26438  pntlemi  26439  pntlemf  26440  pntlemk  26441  pntlemo  26442  pntleme  26443  pntlem3  26444  pntlemp  26445  pntleml  26446  ostth2lem1  26453  ostth2lem3  26470  ostth2  26472  ostth3  26473  crctcshwlkn0lem5  27852  smcnlem  28732  blocnilem  28839  blocni  28840  ubthlem2  28906  minvecolem3  28911  minvecolem4  28915  minvecolem5  28916  nmcexi  30061  lnconi  30068  fsumub  30816  rpxdivcld  30882  sqsscirc1  31526  cnre2csqlem  31528  tpr2rico  31530  xrmulc1cn  31548  xrge0iifiso  31553  xrge0iifhom  31555  esumcst  31697  esumdivc  31717  dya2icoseg  31910  omssubaddlem  31932  omssubadd  31933  probmeasb  32063  sgnmulrp2  32176  signsply0  32196  logdivsqrle  32296  hgt750leme  32304  dnicn  34358  unblimceq0lem  34372  unbdqndv2lem1  34375  unbdqndv2lem2  34376  knoppndvlem18  34395  knoppndvlem21  34398  poimirlem29  35492  heicant  35498  opnmbllem0  35499  mblfinlem3  35502  itg2addnclem3  35516  itg2addnc  35517  itggt0cn  35533  ftc1cnnclem  35534  ftc1anclem6  35541  ftc1anclem7  35542  geomcau  35603  sstotbnd2  35618  isbnd3  35628  equivbnd  35634  prdsbnd2  35639  cntotbnd  35640  heibor1lem  35653  heiborlem6  35660  bfplem1  35666  bfplem2  35667  bfp  35668  rrndstprj2  35675  rrnequiv  35679  lcmineqlem21  39740  aks4d1p1p4  39761  aks4d1p1p7  39764  exp11nnd  39973  fltnlta  40144  irrapxlem4  40291  irrapxlem5  40292  irrapx1  40294  pell1qrgaplem  40339  pell14qrgapw  40342  pellqrexplicit  40343  pellqrex  40345  pellfundge  40348  pellfundgt1  40349  rmspecfund  40375  rmxycomplete  40383  rmxypos  40413  binomcxplemnotnn0  41588  suprltrp  42481  supxrge  42491  infrpge  42504  infleinflem1  42523  xralrple4  42526  recnnltrp  42530  rpgtrecnn  42533  fmul01lt1lem1  42743  fmul01lt1lem2  42744  ltmod  42797  lptre2pt  42799  addlimc  42807  0ellimcdiv  42808  limclner  42810  climleltrp  42835  climisp  42905  climxrrelem  42908  climxrre  42909  limsupgtlem  42936  liminfltlem  42963  cnrefiisplem  42988  climxlim2lem  43004  dvdivbd  43082  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  itgiccshift  43139  itgperiod  43140  stoweidlem1  43160  stoweidlem3  43162  stoweidlem5  43164  stoweidlem7  43166  stoweidlem11  43170  stoweidlem13  43172  stoweidlem14  43173  stoweidlem24  43183  stoweidlem25  43184  stoweidlem26  43185  stoweidlem34  43193  stoweidlem41  43200  stoweidlem42  43201  stoweidlem49  43208  stoweidlem51  43210  stoweidlem52  43211  stoweidlem59  43218  stoweidlem60  43219  stoweidlem62  43221  stoweid  43222  wallispilem5  43228  stirlinglem1  43233  stirlinglem4  43236  stirlinglem5  43237  stirlinglem6  43238  dirkercncflem1  43262  fourierdlem30  43296  fourierdlem39  43305  fourierdlem47  43312  fourierdlem73  43338  fourierdlem81  43346  fourierdlem87  43352  fourierdlem103  43368  fourierdlem104  43369  fourierdlem107  43372  rrndistlt  43449  qndenserrnbllem  43453  sge0ltfirp  43556  sge0rpcpnf  43577  sge0xaddlem1  43589  omeiunltfirp  43675  carageniuncllem2  43678  ovnsubaddlem1  43726  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hoiqssbllem1  43778  hoiqssbllem2  43779  hoiqssbllem3  43780  hspmbllem2  43783  hspmbllem3  43784  ovolval5lem1  43808  ovolval5lem2  43809  iinhoiicc  43830  vonioolem1  43836  pimrecltpos  43861  smflimlem3  43923  smfmullem1  43940  smfmullem2  43941  smfmullem3  43942  modexp2m1d  44680  dignn0flhalflem1  45577  itsclc0yqsol  45726  amgmwlem  46120  amgmw2d  46122  young2d  46123