Theorem rpred 12984

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907  df-rp 12941

This theorem is referenced by:  rpxrd  12985  rpcnd  12986  rpregt0d  12990  rprege0d  12991  rprene0d  12992  rprecred  12995  ltmulgt11d  13019  ltmulgt12d  13020  gt0divd  13021  ge0divd  13022  lediv12ad  13043  prodge0rd  13049  xlemul1  13240  xov1plusxeqvd  13449  ltexp2a  14126  rpexpmord  14128  expcan  14129  ltexp2  14130  leexp2a  14132  expnlbnd2  14194  expmulnbnd  14195  exp11nnd  14221  01sqrexlem6  15207  cau3lem  15315  rlimcld2  15538  addcn2  15554  mulcn2  15556  reccn2  15557  o1rlimmul  15579  rlimno1  15614  caucvgrlem  15633  isumrpcl  15806  isumltss  15811  expcnv  15827  mertenslem1  15847  effsumlt  16076  recoshcl  16123  eirrlem  16169  rpnnen2lem11  16189  bitsmod  16403  prmreclem3  16887  prmreclem5  16889  4sqlem7  16913  ssblex  24418  metss2lem  24501  methaus  24510  met1stc  24511  met2ndci  24512  metustto  24543  metustexhalf  24546  nlmvscnlem2  24675  nlmvscnlem1  24676  nrginvrcnlem  24681  nmoi2  24720  nghmcn  24735  reperflem  24809  iccntr  24812  icccmplem2  24814  reconnlem2  24818  opnreen  24822  metdcnlem  24827  metnrmlem3  24852  addcnlem  24855  cnheibor  24947  cnllycmp  24948  lebnumlem3  24955  lebnumii  24958  nmoleub2lem  25106  nmoleub2lem3  25107  nmoleub2lem2  25108  nmoleub3  25111  nmhmcn  25112  ipcnlem2  25236  ipcnlem1  25237  lmnn  25255  iscfil3  25265  cfilfcls  25266  iscmet3lem1  25283  iscmet3lem2  25284  bcthlem4  25319  bcthlem5  25320  minveclem3b  25420  minveclem3  25421  ivthlem2  25444  ovolgelb  25472  ovollb2lem  25480  ovolunlem1a  25488  ovolunlem1  25489  ovoliunlem1  25494  ovoliunlem2  25495  ovolscalem1  25505  ioombl1lem2  25551  ioombl1lem4  25553  uniioombllem1  25573  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  opnmbllem  25593  volcn  25598  vitalilem4  25603  itg2mulclem  25738  itg2monolem3  25744  itg2cnlem2  25754  itg2cn  25755  itggt0  25836  dveflem  25971  dvferm1lem  25976  dvferm2lem  25978  lhop1lem  26005  lhop1  26006  lhop  26008  dvcnvrelem1  26009  dvcnvrelem2  26010  dvcnvre  26011  dvfsumrlim  26023  ftc1a  26029  ftc1lem4  26031  plyeq0lem  26200  aalioulem2  26324  aalioulem4  26326  aalioulem5  26327  aalioulem6  26328  aaliou  26329  aaliou2b  26332  aaliou3lem1  26333  aaliou3lem2  26334  aaliou3lem8  26336  aaliou3lem5  26338  aaliou3lem7  26340  aaliou3lem9  26341  ulmcn  26389  ulmdvlem1  26390  mtest  26394  itgulm  26398  psercn  26416  pserdvlem1  26417  pserdvlem2  26418  pserdv  26419  abelthlem7  26428  pilem2  26442  divlogrlim  26624  logcnlem3  26633  logcnlem4  26634  logccv  26652  divcxp  26676  cxplt  26683  cxple2  26686  recxpf1lem  26718  cxpcn3lem  26736  cxpaddlelem  26740  cxpaddle  26741  loglesqrt  26750  leibpi  26931  rlimcnp3  26956  cxplim  26960  rlimcxp  26962  cxp2limlem  26964  cxp2lim  26965  cxploglim  26966  cxploglim2  26967  divsqrtsumlem  26968  jensenlem2  26976  logdifbnd  26982  emcllem4  26987  harmonicbnd4  26999  fsumharmonic  27000  zetacvg  27003  lgamgulmlem2  27018  lgamgulmlem5  27021  lgamucov  27026  regamcl  27049  relgamcl  27050  ftalem1  27061  ftalem2  27062  ftalem3  27063  ftalem5  27065  basellem1  27069  basellem3  27071  basellem4  27072  basellem8  27076  chtwordi  27144  chpchtsum  27207  logfacrlim  27212  logexprlim  27213  bclbnd  27268  efexple  27269  bposlem1  27272  bposlem2  27273  bposlem6  27277  bposlem7  27278  chebbnd1lem3  27459  chebbnd1  27460  chtppilimlem1  27461  chtppilimlem2  27462  chpo1ubb  27469  rplogsumlem1  27472  rplogsumlem2  27473  dchrisum0lem1a  27474  rpvmasumlem  27475  dchrisumlem2  27478  dchrisumlem3  27479  dchrmusumlema  27481  dchrmusum2  27482  dchrvmasumlem1  27483  dchrvmasum2lem  27484  dchrvmasumlema  27488  dchrvmasumiflem1  27489  dchrisum0fno1  27499  dchrisum0lem1b  27503  dchrisum0lem1  27504  dchrisum0lem2  27506  dchrisum0lem3  27507  dchrisum0  27508  mulogsumlem  27519  logdivsum  27521  mulog2sumlem2  27523  vmalogdivsum2  27526  2vmadivsumlem  27528  log2sumbnd  27532  selberglem2  27534  selberg  27536  selberg2lem  27538  chpdifbndlem1  27541  chpdifbndlem2  27542  selberg3lem1  27545  selberg4lem1  27548  pntrsumbnd2  27555  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem5  27569  pntrlog2bndlem6a  27570  pntrlog2bndlem6  27571  pntrlog2bnd  27572  pntpbnd1a  27573  pntpbnd1  27574  pntpbnd2  27575  pntibndlem1  27577  pntibndlem2  27579  pntibndlem3  27580  pntibnd  27581  pntlemc  27583  pntlema  27584  pntlemb  27585  pntlemg  27586  pntlemh  27587  pntlemn  27588  pntlemq  27589  pntlemr  27590  pntlemj  27591  pntlemi  27592  pntlemf  27593  pntlemk  27594  pntlemo  27595  pntleme  27596  pntlem3  27597  pntlemp  27598  pntleml  27599  ostth2lem1  27606  ostth2lem3  27623  ostth2  27625  ostth3  27626  crctcshwlkn0lem5  29907  nrt2irr  30568  smcnlem  30793  blocnilem  30900  blocni  30901  ubthlem2  30967  minvecolem3  30972  minvecolem4  30976  minvecolem5  30977  nmcexi  32122  lnconi  32129  fsumub  32927  sgnmulrp2  32935  rpxdivcld  33019  constrinvcl  33964  constrsqrtcl  33970  sqsscirc1  34099  cnre2csqlem  34101  tpr2rico  34103  xrmulc1cn  34121  xrge0iifiso  34126  xrge0iifhom  34128  esumcst  34254  esumdivc  34274  dya2icoseg  34468  omssubaddlem  34490  omssubadd  34491  probmeasb  34621  signsply0  34742  logdivsqrle  34841  hgt750leme  34849  dnicn  36805  unblimceq0lem  36819  unbdqndv2lem1  36822  unbdqndv2lem2  36823  knoppndvlem18  36842  knoppndvlem21  36845  poimirlem29  38023  heicant  38029  opnmbllem0  38030  mblfinlem3  38033  itg2addnclem3  38047  itg2addnc  38048  itggt0cn  38064  ftc1cnnclem  38065  ftc1anclem6  38072  ftc1anclem7  38073  geomcau  38133  sstotbnd2  38148  isbnd3  38158  equivbnd  38164  prdsbnd2  38169  cntotbnd  38170  heibor1lem  38183  heiborlem6  38190  bfplem1  38196  bfplem2  38197  bfp  38198  rrndstprj2  38205  rrnequiv  38209  lcmineqlem21  42541  aks4d1p1p4  42563  aks4d1p1p7  42566  aks4d1p5  42572  aks4d1p6  42573  aks6d1c2  42622  fltnlta  43120  irrapxlem4  43277  irrapxlem5  43278  irrapx1  43280  pell1qrgaplem  43325  pell14qrgapw  43328  pellqrexplicit  43329  pellqrex  43331  pellfundge  43334  pellfundgt1  43335  rmspecfund  43361  rmxycomplete  43369  rmxypos  43399  binomcxplemnotnn0  44807  suprltrp  45780  supxrge  45790  infrpge  45803  infleinflem1  45821  xralrple4  45824  recnnltrp  45828  rpgtrecnn  45831  cvgcaule  45941  fmul01lt1lem1  46036  fmul01lt1lem2  46037  ltmod  46088  lptre2pt  46090  addlimc  46098  0ellimcdiv  46099  limclner  46101  climleltrp  46126  climisp  46196  climxrrelem  46199  climxrre  46200  limsupgtlem  46227  liminfltlem  46254  cnrefiisplem  46279  climxlim2lem  46295  dvdivbd  46373  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  itgiccshift  46430  itgperiod  46431  stoweidlem1  46451  stoweidlem3  46453  stoweidlem5  46455  stoweidlem7  46457  stoweidlem11  46461  stoweidlem13  46463  stoweidlem14  46464  stoweidlem24  46474  stoweidlem25  46475  stoweidlem26  46476  stoweidlem34  46484  stoweidlem41  46491  stoweidlem42  46492  stoweidlem49  46499  stoweidlem51  46501  stoweidlem52  46502  stoweidlem59  46509  stoweidlem60  46510  stoweidlem62  46512  stoweid  46513  wallispilem5  46519  stirlinglem1  46524  stirlinglem4  46527  stirlinglem5  46528  stirlinglem6  46529  dirkercncflem1  46553  fourierdlem30  46587  fourierdlem39  46596  fourierdlem47  46603  fourierdlem73  46629  fourierdlem81  46637  fourierdlem87  46643  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  rrndistlt  46740  qndenserrnbllem  46744  sge0ltfirp  46850  sge0rpcpnf  46871  sge0xaddlem1  46883  omeiunltfirp  46969  carageniuncllem2  46972  ovnsubaddlem1  47020  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoiqssbllem1  47072  hoiqssbllem2  47073  hoiqssbllem3  47074  hspmbllem2  47077  hspmbllem3  47078  ovolval5lem1  47102  ovolval5lem2  47103  iinhoiicc  47124  vonioolem1  47130  pimrecltpos  47158  smflimlem3  47223  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243  modexp2m1d  48097  dignn0flhalflem1  49113  itsclc0yqsol  49262  amgmwlem  50299  amgmw2d  50301  young2d  50302