Theorem rpred 12995

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-rp 12952

This theorem is referenced by:  rpxrd  12996  rpcnd  12997  rpregt0d  13001  rprege0d  13002  rprene0d  13003  rprecred  13006  ltmulgt11d  13030  ltmulgt12d  13031  gt0divd  13032  ge0divd  13033  lediv12ad  13054  prodge0rd  13060  xlemul1  13250  xov1plusxeqvd  13459  ltexp2a  14131  rpexpmord  14133  expcan  14134  ltexp2  14135  leexp2a  14137  expnlbnd2  14199  expmulnbnd  14200  exp11nnd  14226  01sqrexlem6  15213  cau3lem  15321  rlimcld2  15544  addcn2  15560  mulcn2  15562  reccn2  15563  o1rlimmul  15585  rlimno1  15620  caucvgrlem  15639  isumrpcl  15809  isumltss  15814  expcnv  15830  mertenslem1  15850  effsumlt  16079  recoshcl  16126  eirrlem  16172  rpnnen2lem11  16192  bitsmod  16406  prmreclem3  16889  prmreclem5  16891  4sqlem7  16915  ssblex  24316  metss2lem  24399  methaus  24408  met1stc  24409  met2ndci  24410  metustto  24441  metustexhalf  24444  nlmvscnlem2  24573  nlmvscnlem1  24574  nrginvrcnlem  24579  nmoi2  24618  nghmcn  24633  reperflem  24707  iccntr  24710  icccmplem2  24712  reconnlem2  24716  opnreen  24720  metdcnlem  24725  metnrmlem3  24750  addcnlem  24753  cnheibor  24854  cnllycmp  24855  lebnumlem3  24862  lebnumii  24865  nmoleub2lem  25014  nmoleub2lem3  25015  nmoleub2lem2  25016  nmoleub3  25019  nmhmcn  25020  ipcnlem2  25144  ipcnlem1  25145  lmnn  25163  iscfil3  25173  cfilfcls  25174  iscmet3lem1  25191  iscmet3lem2  25192  bcthlem4  25227  bcthlem5  25228  minveclem3b  25328  minveclem3  25329  ivthlem2  25353  ovolgelb  25381  ovollb2lem  25389  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem2  25404  ovolscalem1  25414  ioombl1lem2  25460  ioombl1lem4  25462  uniioombllem1  25482  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  opnmbllem  25502  volcn  25507  vitalilem4  25512  itg2mulclem  25647  itg2monolem3  25653  itg2cnlem2  25663  itg2cn  25664  itggt0  25745  dveflem  25883  dvferm1lem  25888  dvferm2lem  25890  lhop1lem  25918  lhop1  25919  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvfsumrlim  25938  ftc1a  25944  ftc1lem4  25946  plyeq0lem  26115  aalioulem2  26241  aalioulem4  26243  aalioulem5  26244  aalioulem6  26245  aaliou  26246  aaliou2b  26249  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem8  26253  aaliou3lem5  26255  aaliou3lem7  26257  aaliou3lem9  26258  ulmcn  26308  ulmdvlem1  26309  mtest  26313  itgulm  26317  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  pserdv  26339  abelthlem7  26348  pilem2  26362  divlogrlim  26544  logcnlem3  26553  logcnlem4  26554  logccv  26572  divcxp  26596  cxplt  26603  cxple2  26606  recxpf1lem  26638  cxpcn3lem  26657  cxpaddlelem  26661  cxpaddle  26662  loglesqrt  26671  leibpi  26852  rlimcnp3  26877  cxplim  26882  rlimcxp  26884  cxp2limlem  26886  cxp2lim  26887  cxploglim  26888  cxploglim2  26889  divsqrtsumlem  26890  jensenlem2  26898  logdifbnd  26904  emcllem4  26909  harmonicbnd4  26921  fsumharmonic  26922  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem5  26943  lgamucov  26948  regamcl  26971  relgamcl  26972  ftalem1  26983  ftalem2  26984  ftalem3  26985  ftalem5  26987  basellem1  26991  basellem3  26993  basellem4  26994  basellem8  26998  chtwordi  27066  chpchtsum  27130  logfacrlim  27135  logexprlim  27136  bclbnd  27191  efexple  27192  bposlem1  27195  bposlem2  27196  bposlem6  27200  bposlem7  27201  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chpo1ubb  27392  rplogsumlem1  27395  rplogsumlem2  27396  dchrisum0lem1a  27397  rpvmasumlem  27398  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0fno1  27422  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrisum0  27431  mulogsumlem  27442  logdivsum  27444  mulog2sumlem2  27446  vmalogdivsum2  27449  2vmadivsumlem  27451  log2sumbnd  27455  selberglem2  27457  selberg  27459  selberg2lem  27461  chpdifbndlem1  27464  chpdifbndlem2  27465  selberg3lem1  27468  selberg4lem1  27471  pntrsumbnd2  27478  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntrlog2bndlem6a  27493  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem1  27500  pntibndlem2  27502  pntibndlem3  27503  pntibnd  27504  pntlemc  27506  pntlema  27507  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemn  27511  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemi  27515  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntleme  27519  pntlem3  27520  pntlemp  27521  pntleml  27522  ostth2lem1  27529  ostth2lem3  27546  ostth2  27548  ostth3  27549  crctcshwlkn0lem5  29744  nrt2irr  30402  smcnlem  30626  blocnilem  30733  blocni  30734  ubthlem2  30800  minvecolem3  30805  minvecolem4  30809  minvecolem5  30810  nmcexi  31955  lnconi  31962  fsumub  32753  sgnmulrp2  32761  rpxdivcld  32854  constrinvcl  33763  constrsqrtcl  33769  sqsscirc1  33898  cnre2csqlem  33900  tpr2rico  33902  xrmulc1cn  33920  xrge0iifiso  33925  xrge0iifhom  33927  esumcst  34053  esumdivc  34073  dya2icoseg  34268  omssubaddlem  34290  omssubadd  34291  probmeasb  34421  signsply0  34542  logdivsqrle  34641  hgt750leme  34649  dnicn  36480  unblimceq0lem  36494  unbdqndv2lem1  36497  unbdqndv2lem2  36498  knoppndvlem18  36517  knoppndvlem21  36520  poimirlem29  37643  heicant  37649  opnmbllem0  37650  mblfinlem3  37653  itg2addnclem3  37667  itg2addnc  37668  itggt0cn  37684  ftc1cnnclem  37685  ftc1anclem6  37692  ftc1anclem7  37693  geomcau  37753  sstotbnd2  37768  isbnd3  37778  equivbnd  37784  prdsbnd2  37789  cntotbnd  37790  heibor1lem  37803  heiborlem6  37810  bfplem1  37816  bfplem2  37817  bfp  37818  rrndstprj2  37825  rrnequiv  37829  lcmineqlem21  42037  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p5  42068  aks4d1p6  42069  aks6d1c2  42118  fltnlta  42651  irrapxlem4  42813  irrapxlem5  42814  irrapx1  42816  pell1qrgaplem  42861  pell14qrgapw  42864  pellqrexplicit  42865  pellqrex  42867  pellfundge  42870  pellfundgt1  42871  rmspecfund  42897  rmxycomplete  42906  rmxypos  42936  binomcxplemnotnn0  44345  suprltrp  45324  supxrge  45334  infrpge  45347  infleinflem1  45366  xralrple4  45369  recnnltrp  45373  rpgtrecnn  45376  cvgcaule  45487  fmul01lt1lem1  45582  fmul01lt1lem2  45583  ltmod  45636  lptre2pt  45638  addlimc  45646  0ellimcdiv  45647  limclner  45649  climleltrp  45674  climisp  45744  climxrrelem  45747  climxrre  45748  limsupgtlem  45775  liminfltlem  45802  cnrefiisplem  45827  climxlim2lem  45843  dvdivbd  45921  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  itgiccshift  45978  itgperiod  45979  stoweidlem1  45999  stoweidlem3  46001  stoweidlem5  46003  stoweidlem7  46005  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem24  46022  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem41  46039  stoweidlem42  46040  stoweidlem49  46047  stoweidlem51  46049  stoweidlem52  46050  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  stoweid  46061  wallispilem5  46067  stirlinglem1  46072  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  dirkercncflem1  46101  fourierdlem30  46135  fourierdlem39  46144  fourierdlem47  46151  fourierdlem73  46177  fourierdlem81  46185  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  rrndistlt  46288  qndenserrnbllem  46292  sge0ltfirp  46398  sge0rpcpnf  46419  sge0xaddlem1  46431  omeiunltfirp  46517  carageniuncllem2  46520  ovnsubaddlem1  46568  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoiqssbllem1  46620  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem2  46625  hspmbllem3  46626  ovolval5lem1  46650  ovolval5lem2  46651  iinhoiicc  46672  vonioolem1  46678  pimrecltpos  46706  smflimlem3  46771  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  modexp2m1d  47613  dignn0flhalflem1  48604  itsclc0yqsol  48753  amgmwlem  49791  amgmw2d  49793  young2d  49794