Theorem rpre 13013

Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.)

Assertion

Ref	Expression
rpre	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		rpssre 13012	. 2 ⊢ ℝ+ ⊆ ℝ
2	1	sseli 3935	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℝ⁺crp 13004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-rp 13005

This theorem is referenced by:  rpxr  13014  rpcn  13015  rpge0  13018  rprege0  13020  rprene0  13022  neglt  13024  rpaddcl  13028  rpmulcl  13029  rpdivcl  13031  rpgecl  13034  ledivge1le  13077  addlelt  13120  xralrple  13219  xlemul1  13304  infmrp1  13359  iccdil  13505  ltdifltdiv  13855  modcl  13894  mod0  13897  mulmod0  13898  modge0  13900  modlt  13901  modid0  13918  modabs  13925  modabs2  13926  modcyc  13927  muladdmod  13936  modmuladd  13937  modmuladdnn0  13939  modltm1p1mod  13947  2txmodxeq0  13955  2submod  13956  moddi  13963  modsubdir  13964  modeqmodmin  13965  modirr  13966  rpexpmord  14192  expnlbnd  14257  rennim  15278  cnpart  15279  01sqrexlem1  15281  01sqrexlem2  15282  01sqrexlem4  15284  01sqrexlem5  15285  01sqrexlem6  15286  01sqrexlem7  15287  resqrex  15289  rpsqrtcl  15303  sqreulem  15399  eqsqrt2d  15408  2clim  15611  reccn2  15636  cn1lem  15637  climsqz  15680  climsqz2  15681  rlimsqzlem  15688  climsup  15709  climcau  15710  caucvgrlem2  15714  iseralt  15724  cvgcmp  15856  cvgcmpce  15858  divrcnv  15894  rprisefaccl  16065  efgt1  16160  ef01bndlem  16228  sinltx  16233  stdbdmet  24630  stdbdmopn  24632  met2ndci  24636  cfilucfil  24673  ngptgp  24750  reperflem  24933  iccntr  24936  reconnlem2  24942  opnreen  24946  metdseq0  24969  xlebnum  25081  cphsqrtcl3  25303  iscmet3lem3  25406  iscmet3lem1  25407  iscmet3lem2  25408  caubl  25424  lmcau  25429  bcthlem4  25443  minveclem3b  25544  minveclem3  25545  ivthlem2  25568  ivthlem3  25569  nulmbl2  25652  opnmbllem  25717  itg2const2  25857  itg2mulclem  25862  dveflem  26095  lhop  26132  dvcnvre  26135  aalioulem2  26451  aaliou  26456  aaliou3lem4  26464  ulmcaulem  26511  ulmcau  26512  ulmcn  26516  itgulm  26525  reeff1o  26564  pilem2  26569  logleb  26722  logcj  26725  argimgt0  26731  logdmnrp  26760  logcnlem3  26763  logcnlem4  26764  advlog  26773  efopnlem1  26775  cxple2  26816  cxplt2  26817  cxple3  26820  2irrexpq  26850  cxpcn3  26867  resqrtcn  26868  relogbf  26910  asinneg  27005  atanbndlem  27044  cxplim  27090  cxp2limlem  27094  cxp2lim  27095  cxploglim  27096  cxploglim2  27097  logdiflbnd  27113  harmoniclbnd  27127  harmonicbnd4  27129  chtrpcl  27293  ppiltx  27295  chtleppi  27328  logfacubnd  27339  logfaclbnd  27340  logfacbnd3  27341  logexprlim  27343  bposlem7  27408  bposlem8  27409  bposlem9  27410  chebbnd1  27590  chtppilim  27593  chto1ub  27594  chpo1ub  27598  vmadivsum  27600  rpvmasumlem  27605  dchrisumlem3  27609  dchrvmasumlem2  27616  dchrvmasumiflem1  27619  dchrisum0  27638  mudivsum  27648  mulogsumlem  27649  mulogsum  27650  mulog2sumlem2  27653  log2sumbnd  27662  selberglem2  27664  selberglem3  27665  selberg  27666  selberg2lem  27668  selberg2  27669  pntrf  27681  pntrmax  27682  pntrsumo1  27683  selbergr  27686  selbergs  27692  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  pntibndlem1  27707  pntlem3  27727  pntlemp  27728  pntleml  27729  pnt2  27731  padicabvcxp  27750  vacn  30951  nmcvcn  30952  smcnlem  30954  blocnilem  31061  chscllem2  31895  nmcexi  32283  nmcopexi  32284  nmcfnexi  32308  dp2ltsuc  33113  dpval3rp  33127  dplti  33132  dpgti  33133  dpexpp1  33135  dpadd2  33137  pnfinf  33411  sqsscirc1  34210  dya2icoseg2  34580  probfinmeasb  34730  probfinmeasbALTV  34731  signshf  34887  divsqrtid  34893  logdivsqrle  34949  hgt750lem2  34951  subfacval3  35547  opnrebl  36688  opnrebl2  36689  taupilem1  37820  opnmbllem0  38162  itg2addnclem  38177  itg2addnclem2  38178  itg2addnclem3  38179  itg2addnc  38180  itg2gt0cn  38181  ftc1anclem5  38203  ftc1anclem7  38205  ftc1anc  38207  areacirclem1  38214  areacirclem4  38217  areacirc  38219  geomcau  38265  isbnd2  38289  ssbnd  38294  heiborlem7  38323  heiborlem8  38324  bfplem2  38329  rrncmslem  38338  rrnequiv  38341  dvrelog3  42689  aks4d1p1p6  42697  rpabsid  42937  irrapxlem1  43406  irrapxlem2  43407  irrapxlem3  43408  irrapxlem5  43410  2timesgt  45866  supxrge  45913  suplesup  45914  xrlexaddrp  45927  xralrple2  45929  infleinflem1  45944  xralrple4  45947  xralrple3  45948  xrralrecnnle  45957  climinf  46181  mullimc  46191  mullimcf  46198  limcrecl  46204  limcleqr  46217  addlimc  46221  0ellimcdiv  46222  limclner  46224  liminflimsupclim  46380  ioodvbdlimc1lem1  46504  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  stoweidlem7  46580  fourierdlem73  46752  fourierdlem87  46766  fourierdlem103  46782  fourierdlem104  46783  sge0iunmptlemre  46988  smflimlem4  47347  fldivexpfllog2  49197  blenre  49206  itscnhlc0yqe  49391  itscnhlc0xyqsol  49397  itschlc0xyqsol  49399  itsclc0xyqsolr  49401  itsclinecirc0in  49407  itsclquadb  49408  itscnhlinecirc02plem3  49416  itscnhlinecirc02p  49417  inlinecirc02plem  49418  inlinecirc02p  49419  amgmwlem  50432