Theorem rpred 12931

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11002  ℝ⁺crp 12887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919  df-rp 12888

This theorem is referenced by:  rpxrd  12932  rpcnd  12933  rpregt0d  12937  rprege0d  12938  rprene0d  12939  rprecred  12942  ltmulgt11d  12966  ltmulgt12d  12967  gt0divd  12968  ge0divd  12969  lediv12ad  12990  prodge0rd  12996  xlemul1  13186  xov1plusxeqvd  13395  ltexp2a  14070  rpexpmord  14072  expcan  14073  ltexp2  14074  leexp2a  14076  expnlbnd2  14138  expmulnbnd  14139  exp11nnd  14165  01sqrexlem6  15151  cau3lem  15259  rlimcld2  15482  addcn2  15498  mulcn2  15500  reccn2  15501  o1rlimmul  15523  rlimno1  15558  caucvgrlem  15577  isumrpcl  15747  isumltss  15752  expcnv  15768  mertenslem1  15788  effsumlt  16017  recoshcl  16064  eirrlem  16110  rpnnen2lem11  16130  bitsmod  16344  prmreclem3  16827  prmreclem5  16829  4sqlem7  16853  ssblex  24341  metss2lem  24424  methaus  24433  met1stc  24434  met2ndci  24435  metustto  24466  metustexhalf  24469  nlmvscnlem2  24598  nlmvscnlem1  24599  nrginvrcnlem  24604  nmoi2  24643  nghmcn  24658  reperflem  24732  iccntr  24735  icccmplem2  24737  reconnlem2  24741  opnreen  24745  metdcnlem  24750  metnrmlem3  24775  addcnlem  24778  cnheibor  24879  cnllycmp  24880  lebnumlem3  24887  lebnumii  24890  nmoleub2lem  25039  nmoleub2lem3  25040  nmoleub2lem2  25041  nmoleub3  25044  nmhmcn  25045  ipcnlem2  25169  ipcnlem1  25170  lmnn  25188  iscfil3  25198  cfilfcls  25199  iscmet3lem1  25216  iscmet3lem2  25217  bcthlem4  25252  bcthlem5  25253  minveclem3b  25353  minveclem3  25354  ivthlem2  25378  ovolgelb  25406  ovollb2lem  25414  ovolunlem1a  25422  ovolunlem1  25423  ovoliunlem1  25428  ovoliunlem2  25429  ovolscalem1  25439  ioombl1lem2  25485  ioombl1lem4  25487  uniioombllem1  25507  uniioombllem3  25511  uniioombllem4  25512  uniioombllem5  25513  opnmbllem  25527  volcn  25532  vitalilem4  25537  itg2mulclem  25672  itg2monolem3  25678  itg2cnlem2  25688  itg2cn  25689  itggt0  25770  dveflem  25908  dvferm1lem  25913  dvferm2lem  25915  lhop1lem  25943  lhop1  25944  lhop  25946  dvcnvrelem1  25947  dvcnvrelem2  25948  dvcnvre  25949  dvfsumrlim  25963  ftc1a  25969  ftc1lem4  25971  plyeq0lem  26140  aalioulem2  26266  aalioulem4  26268  aalioulem5  26269  aalioulem6  26270  aaliou  26271  aaliou2b  26274  aaliou3lem1  26275  aaliou3lem2  26276  aaliou3lem8  26278  aaliou3lem5  26280  aaliou3lem7  26282  aaliou3lem9  26283  ulmcn  26333  ulmdvlem1  26334  mtest  26338  itgulm  26342  psercn  26361  pserdvlem1  26362  pserdvlem2  26363  pserdv  26364  abelthlem7  26373  pilem2  26387  divlogrlim  26569  logcnlem3  26578  logcnlem4  26579  logccv  26597  divcxp  26621  cxplt  26628  cxple2  26631  recxpf1lem  26663  cxpcn3lem  26682  cxpaddlelem  26686  cxpaddle  26687  loglesqrt  26696  leibpi  26877  rlimcnp3  26902  cxplim  26907  rlimcxp  26909  cxp2limlem  26911  cxp2lim  26912  cxploglim  26913  cxploglim2  26914  divsqrtsumlem  26915  jensenlem2  26923  logdifbnd  26929  emcllem4  26934  harmonicbnd4  26946  fsumharmonic  26947  zetacvg  26950  lgamgulmlem2  26965  lgamgulmlem5  26968  lgamucov  26973  regamcl  26996  relgamcl  26997  ftalem1  27008  ftalem2  27009  ftalem3  27010  ftalem5  27012  basellem1  27016  basellem3  27018  basellem4  27019  basellem8  27023  chtwordi  27091  chpchtsum  27155  logfacrlim  27160  logexprlim  27161  bclbnd  27216  efexple  27217  bposlem1  27220  bposlem2  27221  bposlem6  27225  bposlem7  27226  chebbnd1lem3  27407  chebbnd1  27408  chtppilimlem1  27409  chtppilimlem2  27410  chpo1ubb  27417  rplogsumlem1  27420  rplogsumlem2  27421  dchrisum0lem1a  27422  rpvmasumlem  27423  dchrisumlem2  27426  dchrisumlem3  27427  dchrmusumlema  27429  dchrmusum2  27430  dchrvmasumlem1  27431  dchrvmasum2lem  27432  dchrvmasumlema  27436  dchrvmasumiflem1  27437  dchrisum0fno1  27447  dchrisum0lem1b  27451  dchrisum0lem1  27452  dchrisum0lem2  27454  dchrisum0lem3  27455  dchrisum0  27456  mulogsumlem  27467  logdivsum  27469  mulog2sumlem2  27471  vmalogdivsum2  27474  2vmadivsumlem  27476  log2sumbnd  27480  selberglem2  27482  selberg  27484  selberg2lem  27486  chpdifbndlem1  27489  chpdifbndlem2  27490  selberg3lem1  27493  selberg4lem1  27496  pntrsumbnd2  27503  pntrlog2bndlem2  27514  pntrlog2bndlem3  27515  pntrlog2bndlem5  27517  pntrlog2bndlem6a  27518  pntrlog2bndlem6  27519  pntrlog2bnd  27520  pntpbnd1a  27521  pntpbnd1  27522  pntpbnd2  27523  pntibndlem1  27525  pntibndlem2  27527  pntibndlem3  27528  pntibnd  27529  pntlemc  27531  pntlema  27532  pntlemb  27533  pntlemg  27534  pntlemh  27535  pntlemn  27536  pntlemq  27537  pntlemr  27538  pntlemj  27539  pntlemi  27540  pntlemf  27541  pntlemk  27542  pntlemo  27543  pntleme  27544  pntlem3  27545  pntlemp  27546  pntleml  27547  ostth2lem1  27554  ostth2lem3  27571  ostth2  27573  ostth3  27574  crctcshwlkn0lem5  29790  nrt2irr  30448  smcnlem  30672  blocnilem  30779  blocni  30780  ubthlem2  30846  minvecolem3  30851  minvecolem4  30855  minvecolem5  30856  nmcexi  32001  lnconi  32008  fsumub  32806  sgnmulrp2  32814  rpxdivcld  32909  constrinvcl  33781  constrsqrtcl  33787  sqsscirc1  33916  cnre2csqlem  33918  tpr2rico  33920  xrmulc1cn  33938  xrge0iifiso  33943  xrge0iifhom  33945  esumcst  34071  esumdivc  34091  dya2icoseg  34285  omssubaddlem  34307  omssubadd  34308  probmeasb  34438  signsply0  34559  logdivsqrle  34658  hgt750leme  34666  dnicn  36525  unblimceq0lem  36539  unbdqndv2lem1  36542  unbdqndv2lem2  36543  knoppndvlem18  36562  knoppndvlem21  36565  poimirlem29  37688  heicant  37694  opnmbllem0  37695  mblfinlem3  37698  itg2addnclem3  37712  itg2addnc  37713  itggt0cn  37729  ftc1cnnclem  37730  ftc1anclem6  37737  ftc1anclem7  37738  geomcau  37798  sstotbnd2  37813  isbnd3  37823  equivbnd  37829  prdsbnd2  37834  cntotbnd  37835  heibor1lem  37848  heiborlem6  37855  bfplem1  37861  bfplem2  37862  bfp  37863  rrndstprj2  37870  rrnequiv  37874  lcmineqlem21  42081  aks4d1p1p4  42103  aks4d1p1p7  42106  aks4d1p5  42112  aks4d1p6  42113  aks6d1c2  42162  fltnlta  42695  irrapxlem4  42857  irrapxlem5  42858  irrapx1  42860  pell1qrgaplem  42905  pell14qrgapw  42908  pellqrexplicit  42909  pellqrex  42911  pellfundge  42914  pellfundgt1  42915  rmspecfund  42941  rmxycomplete  42949  rmxypos  42979  binomcxplemnotnn0  44388  suprltrp  45366  supxrge  45376  infrpge  45389  infleinflem1  45407  xralrple4  45410  recnnltrp  45414  rpgtrecnn  45417  cvgcaule  45528  fmul01lt1lem1  45623  fmul01lt1lem2  45624  ltmod  45675  lptre2pt  45677  addlimc  45685  0ellimcdiv  45686  limclner  45688  climleltrp  45713  climisp  45783  climxrrelem  45786  climxrre  45787  limsupgtlem  45814  liminfltlem  45841  cnrefiisplem  45866  climxlim2lem  45882  dvdivbd  45960  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  itgiccshift  46017  itgperiod  46018  stoweidlem1  46038  stoweidlem3  46040  stoweidlem5  46042  stoweidlem7  46044  stoweidlem11  46048  stoweidlem13  46050  stoweidlem14  46051  stoweidlem24  46061  stoweidlem25  46062  stoweidlem26  46063  stoweidlem34  46071  stoweidlem41  46078  stoweidlem42  46079  stoweidlem49  46086  stoweidlem51  46088  stoweidlem52  46089  stoweidlem59  46096  stoweidlem60  46097  stoweidlem62  46099  stoweid  46100  wallispilem5  46106  stirlinglem1  46111  stirlinglem4  46114  stirlinglem5  46115  stirlinglem6  46116  dirkercncflem1  46140  fourierdlem30  46174  fourierdlem39  46183  fourierdlem47  46190  fourierdlem73  46216  fourierdlem81  46224  fourierdlem87  46230  fourierdlem103  46246  fourierdlem104  46247  fourierdlem107  46250  rrndistlt  46327  qndenserrnbllem  46331  sge0ltfirp  46437  sge0rpcpnf  46458  sge0xaddlem1  46470  omeiunltfirp  46556  carageniuncllem2  46559  ovnsubaddlem1  46607  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hoiqssbllem1  46659  hoiqssbllem2  46660  hoiqssbllem3  46661  hspmbllem2  46664  hspmbllem3  46665  ovolval5lem1  46689  ovolval5lem2  46690  iinhoiicc  46711  vonioolem1  46717  pimrecltpos  46745  smflimlem3  46810  smfmullem1  46828  smfmullem2  46829  smfmullem3  46830  modexp2m1d  47642  dignn0flhalflem1  48646  itsclc0yqsol  48795  amgmwlem  49833  amgmw2d  49835  young2d  49836