Theorem rpred 13191

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11226  ℝ⁺crp 13147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-rp 13148

This theorem is used by:  rpxrd  13192  rpcnd  13193  rpregt0d  13197  rprege0d  13198  rprene0d  13199  rprecred  13202  ltmulgt11d  13226  ltmulgt12d  13227  gt0divd  13228  ge0divd  13229  lediv12ad  13250  prodge0rd  13256  xlemul1  13447  xov1plusxeqvd  13656  ltexp2a  14336  rpexpmord  14338  expcan  14339  ltexp2  14340  leexp2a  14342  expnlbnd2  14405  expmulnbnd  14406  exp11nnd  14432  sgnmulrp2  15290  01sqrexlem6  15443  cau3lem  15551  rlimcld2  15774  addcn2  15790  mulcn2  15792  reccn2  15793  o1rlimmul  15815  rlimno1  15850  caucvgrlem  15869  isumrpcl  16041  isumltss  16046  expcnv  16062  mertenslem1  16082  effsumlt  16308  recoshcl  16355  eirrlem  16401  rpnnen2lem11  16421  bitsmod  16635  prmreclem3  17125  prmreclem5  17127  4sqlem7  17151  ssblex  24777  metss2lem  24860  methaus  24869  met1stc  24870  met2ndci  24871  metustto  24902  metustexhalf  24905  nlmvscnlem2  25034  nlmvscnlem1  25035  nrginvrcnlem  25040  nmoi2  25079  nghmcn  25094  reperflem  25168  iccntr  25171  icccmplem2  25173  reconnlem2  25177  opnreen  25181  metdcnlem  25186  metnrmlem3  25211  addcnlem  25214  cnheibor  25306  cnllycmp  25307  lebnumlem3  25314  lebnumii  25317  nmoleub2lem  25465  nmoleub2lem3  25466  nmoleub2lem2  25467  nmoleub3  25470  nmhmcn  25471  ipcnlem2  25595  ipcnlem1  25596  lmnn  25614  iscfil3  25624  cfilfcls  25625  iscmet3lem1  25642  iscmet3lem2  25643  bcthlem4  25678  bcthlem5  25679  minveclem3b  25779  minveclem3  25780  ivthlem2  25803  ovolgelb  25831  ovollb2lem  25839  ovolunlem1a  25847  ovolunlem1  25848  ovoliunlem1  25853  ovoliunlem2  25854  ovolscalem1  25864  ioombl1lem2  25910  ioombl1lem4  25912  uniioombllem1  25932  uniioombllem3  25936  uniioombllem4  25937  uniioombllem5  25938  opnmbllem  25952  volcn  25957  vitalilem4  25962  itg2mulclem  26097  itg2monolem3  26103  itg2cnlem2  26113  itg2cn  26114  itggt0  26194  dveflem  26329  dvferm1lem  26334  dvferm2lem  26336  lhop1lem  26363  lhop1  26364  lhop  26366  dvcnvrelem1  26367  dvcnvrelem2  26368  dvcnvre  26369  dvfsumrlim  26381  ftc1a  26387  ftc1lem4  26389  plyeq0lem  26559  aalioulem2  26690  aalioulem4  26692  aalioulem5  26693  aalioulem6  26694  aaliou  26695  aaliou2b  26698  aaliou3lem1  26699  aaliou3lem2  26700  aaliou3lem8  26702  aaliou3lem5  26704  aaliou3lem7  26706  aaliou3lem9  26707  ulmcn  26756  ulmdvlem1  26757  mtest  26761  itgulm  26765  psercn  26783  pserdvlem1  26784  pserdvlem2  26785  pserdv  26786  abelthlem7  26795  pilem2  26809  divlogrlim  26993  logcnlem3  27002  logcnlem4  27003  logccv  27021  divcxp  27045  cxplt  27052  cxple2  27055  recxpf1lem  27087  cxpcn3lem  27105  cxpaddlelem  27109  cxpaddle  27110  loglesqrt  27119  leibpi  27300  rlimcnp3  27325  cxplim  27329  rlimcxp  27331  cxp2limlem  27333  cxp2lim  27334  cxploglim  27335  cxploglim2  27336  divsqrtsumlem  27337  jensenlem2  27345  logdifbnd  27351  emcllem4  27356  harmonicbnd4  27368  fsumharmonic  27369  zetacvg  27372  lgamgulmlem2  27387  lgamgulmlem5  27390  lgamucov  27395  regamcl  27418  relgamcl  27419  ftalem1  27430  ftalem2  27431  ftalem3  27432  ftalem5  27434  basellem1  27438  basellem3  27440  basellem4  27441  basellem8  27445  chtwordi  27513  chpchtsum  27576  logfacrlim  27581  logexprlim  27582  bclbnd  27637  efexple  27638  bposlem1  27641  bposlem2  27642  bposlem6  27646  bposlem7  27647  chebbnd1lem3  27828  chebbnd1  27829  chtppilimlem1  27830  chtppilimlem2  27831  chpo1ubb  27838  rplogsumlem1  27841  rplogsumlem2  27842  dchrisum0lem1a  27843  rpvmasumlem  27844  dchrisumlem2  27847  dchrisumlem3  27848  dchrmusumlema  27850  dchrmusum2  27851  dchrvmasumlem1  27852  dchrvmasum2lem  27853  dchrvmasumlema  27857  dchrvmasumiflem1  27858  dchrisum0fno1  27868  dchrisum0lem1b  27872  dchrisum0lem1  27873  dchrisum0lem2  27875  dchrisum0lem3  27876  dchrisum0  27877  mulogsumlem  27888  logdivsum  27890  mulog2sumlem2  27892  vmalogdivsum2  27895  2vmadivsumlem  27897  log2sumbnd  27901  selberglem2  27903  selberg  27905  selberg2lem  27907  chpdifbndlem1  27910  chpdifbndlem2  27911  selberg3lem1  27914  selberg4lem1  27917  pntrsumbnd2  27924  pntrlog2bndlem2  27935  pntrlog2bndlem3  27936  pntrlog2bndlem5  27938  pntrlog2bndlem6a  27939  pntrlog2bndlem6  27940  pntrlog2bnd  27941  pntpbnd1a  27942  pntpbnd1  27943  pntpbnd2  27944  pntibndlem1  27946  pntibndlem2  27948  pntibndlem3  27949  pntibnd  27950  pntlemc  27952  pntlema  27953  pntlemb  27954  pntlemg  27955  pntlemh  27956  pntlemn  27957  pntlemq  27958  pntlemr  27959  pntlemj  27960  pntlemi  27961  pntlemf  27962  pntlemk  27963  pntlemo  27964  pntleme  27965  pntlem3  27966  pntlemp  27967  pntleml  27968  ostth2lem1  27975  ostth2lem3  27992  ostth2  27994  ostth3  27995  crctcshwlkn0lem5  30433  nrt2irr  31104  smcnlem  31329  blocnilem  31436  blocni  31437  ubthlem2  31503  minvecolem3  31508  minvecolem4  31512  minvecolem5  31513  nmcexi  32658  lnconi  32665  fsumub  33489  rpxdivcld  33570  constrinvcl  34475  constrsqrtcl  34481  sqsscirc1  34610  cnre2csqlem  34612  tpr2rico  34614  xrmulc1cn  34632  xrge0iifiso  34637  xrge0iifhom  34639  esumcst  34765  esumdivc  34785  dya2icoseg  34979  omssubaddlem  35001  omssubadd  35002  probmeasb  35132  signsply0  35250  logdivsqrle  35349  hgt750leme  35357  dnicn  37536  unblimceq0lem  37550  unbdqndv2lem1  37553  unbdqndv2lem2  37554  knoppndvlem18  37573  knoppndvlem21  37576  poimirlem29  38759  heicant  38765  opnmbllem0  38766  mblfinlem3  38769  itg2addnclem3  38783  itg2addnc  38784  itggt0cn  38800  ftc1cnnclem  38801  ftc1anclem6  38808  ftc1anclem7  38809  geomcau  38885  sstotbnd2  38900  isbnd3  38910  equivbnd  38916  prdsbnd2  38921  cntotbnd  38922  heibor1lem  38935  heiborlem6  38942  bfplem1  38948  bfplem2  38949  bfp  38950  rrndstprj2  38957  rrnequiv  38961  lcmineqlem21  43291  aks4d1p1p4  43313  aks4d1p1p7  43316  aks4d1p5  43322  aks4d1p6  43323  aks6d1c2  43372  fltnlta  43867  irrapxlem4  44025  irrapxlem5  44026  irrapx1  44028  pell1qrgaplem  44073  pell14qrgapw  44076  pellqrexplicit  44077  pellqrex  44079  pellfundge  44082  pellfundgt1  44083  rmspecfund  44109  rmxycomplete  44117  rmxypos  44147  binomcxplemnotnn0  45532  suprltrp  46545  supxrge  46555  infrpge  46568  infleinflem1  46586  xralrple4  46589  recnnltrp  46593  rpgtrecnn  46596  cvgcaule  46706  fmul01lt1lem1  46801  fmul01lt1lem2  46802  ltmod  46853  lptre2pt  46855  addlimc  46863  0ellimcdiv  46864  limclner  46866  climleltrp  46891  climisp  46961  climxrrelem  46964  climxrre  46965  limsupgtlem  46992  liminfltlem  47019  cnrefiisplem  47044  climxlim2lem  47060  dvdivbd  47138  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  itgiccshift  47195  itgperiod  47196  stoweidlem1  47216  stoweidlem3  47218  stoweidlem5  47220  stoweidlem7  47222  stoweidlem11  47226  stoweidlem13  47228  stoweidlem14  47229  stoweidlem24  47239  stoweidlem25  47240  stoweidlem26  47241  stoweidlem34  47249  stoweidlem41  47256  stoweidlem42  47257  stoweidlem49  47264  stoweidlem51  47266  stoweidlem52  47267  stoweidlem59  47274  stoweidlem60  47275  stoweidlem62  47277  stoweid  47278  wallispilem5  47284  stirlinglem1  47289  stirlinglem4  47292  stirlinglem5  47293  stirlinglem6  47294  dirkercncflem1  47318  fourierdlem30  47352  fourierdlem39  47361  fourierdlem47  47368  fourierdlem73  47394  fourierdlem81  47402  fourierdlem87  47408  fourierdlem103  47424  fourierdlem104  47425  fourierdlem107  47428  rrndistlt  47505  qndenserrnbllem  47509  sge0ltfirp  47615  sge0rpcpnf  47636  sge0xaddlem1  47648  omeiunltfirp  47734  carageniuncllem2  47737  ovnsubaddlem1  47785  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem3  47812  hoidmvlelem4  47813  hoiqssbllem1  47837  hoiqssbllem2  47838  hoiqssbllem3  47839  hspmbllem2  47842  hspmbllem3  47843  ovolval5lem1  47867  ovolval5lem2  47868  iinhoiicc  47889  vonioolem1  47895  pimrecltpos  47923  smflimlem3  47988  smfmullem1  48006  smfmullem2  48007  smfmullem3  48008  modexp2m1d  48902  dignn0flhalflem1  49932  itsclc0yqsol  50081  amgmwlem  51267  amgmw2d  51269  young2d  51270