Theorem rpre 13136

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 13135	. 2 ⊢ ℝ+ ⊆ ℝ
2	1	sseli 3905	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11206  ℝ⁺crp 13127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3897  df-rp 13128

This theorem is used by:  rpxr  13137  rpcn  13138  rpge0  13141  rprege0  13143  rprene0  13145  neglt  13147  rpaddcl  13151  rpmulcl  13152  rpdivcl  13154  rpgecl  13157  ledivge1le  13200  addlelt  13243  xralrple  13342  xlemul1  13427  infmrp1  13482  iccdil  13628  ltdifltdiv  13981  modcl  14020  mod0  14023  mulmod0  14024  modge0  14026  modlt  14027  modid0  14044  modabs  14051  modabs2  14052  modcyc  14053  muladdmod  14062  modmuladd  14063  modmuladdnn0  14065  modltm1p1mod  14073  2txmodxeq0  14081  2submod  14082  moddi  14089  modsubdir  14090  modeqmodmin  14091  modirr  14092  rpexpmord  14318  expnlbnd  14384  rennim  15415  cnpart  15416  01sqrexlem1  15418  01sqrexlem2  15419  01sqrexlem4  15421  01sqrexlem5  15422  01sqrexlem6  15423  01sqrexlem7  15424  resqrex  15426  rpsqrtcl  15440  sqreulem  15536  eqsqrt2d  15545  2clim  15748  reccn2  15773  cn1lem  15774  climsqz  15817  climsqz2  15818  rlimsqzlem  15825  climsup  15846  climcau  15847  caucvgrlem2  15851  iseralt  15861  cvgcmp  15992  cvgcmpce  15994  divrcnv  16030  rprisefaccl  16199  efgt1  16293  ef01bndlem  16361  sinltx  16366  stdbdmet  24844  stdbdmopn  24846  met2ndci  24850  cfilucfil  24887  ngptgp  24964  reperflem  25147  iccntr  25150  reconnlem2  25156  opnreen  25160  metdseq0  25183  xlebnum  25295  cphsqrtcl3  25517  iscmet3lem3  25620  iscmet3lem1  25621  iscmet3lem2  25622  caubl  25638  lmcau  25643  bcthlem4  25657  minveclem3b  25758  minveclem3  25759  ivthlem2  25782  ivthlem3  25783  nulmbl2  25866  opnmbllem  25931  itg2const2  26071  itg2mulclem  26076  dveflem  26308  lhop  26345  dvcnvre  26348  aalioulem2  26669  aaliou  26674  aaliou3lem4  26682  ulmcaulem  26730  ulmcau  26731  ulmcn  26735  itgulm  26744  reeff1o  26783  pilem2  26788  logleb  26940  logcj  26943  argimgt0  26949  logdmnrp  26978  logcnlem3  26981  logcnlem4  26982  advlog  26991  efopnlem1  26993  cxple2  27034  cxplt2  27035  cxple3  27038  2irrexpq  27068  cxpcn3  27085  resqrtcn  27086  relogbf  27128  asinneg  27223  atanbndlem  27262  cxplim  27308  cxp2limlem  27312  cxp2lim  27313  cxploglim  27314  cxploglim2  27315  logdiflbnd  27331  harmoniclbnd  27345  harmonicbnd4  27347  chtrpcl  27511  ppiltx  27513  chtleppi  27546  logfacubnd  27557  logfaclbnd  27558  logfacbnd3  27559  logexprlim  27561  bposlem7  27626  bposlem8  27627  bposlem9  27628  chebbnd1  27808  chtppilim  27811  chto1ub  27812  chpo1ub  27816  vmadivsum  27818  rpvmasumlem  27823  dchrisumlem3  27827  dchrvmasumlem2  27834  dchrvmasumiflem1  27837  dchrisum0  27856  mudivsum  27866  mulogsumlem  27867  mulogsum  27868  mulog2sumlem2  27871  log2sumbnd  27880  selberglem2  27882  selberglem3  27883  selberg  27884  selberg2lem  27886  selberg2  27887  pntrf  27899  pntrmax  27900  pntrsumo1  27901  selbergr  27904  selbergs  27910  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntibndlem1  27925  pntlem3  27945  pntlemp  27946  pntleml  27947  pnt2  27949  padicabvcxp  27968  vacn  31305  nmcvcn  31306  smcnlem  31308  blocnilem  31415  chscllem2  32249  nmcexi  32637  nmcopexi  32638  nmcfnexi  32662  dp2ltsuc  33502  dpval3rp  33516  dplti  33521  dpgti  33522  dpexpp1  33524  dpadd2  33526  pnfinf  33794  sqsscirc1  34590  dya2icoseg2  34960  probfinmeasb  35110  probfinmeasbALTV  35111  signshf  35267  divsqrtid  35273  logdivsqrle  35329  hgt750lem2  35331  subfacval3  36044  opnrebl  37204  opnrebl2  37205  taupilem1  38351  opnmbllem0  38683  itg2addnclem  38698  itg2addnclem2  38699  itg2addnclem3  38700  itg2addnc  38701  itg2gt0cn  38702  ftc1anclem5  38724  ftc1anclem7  38726  ftc1anc  38728  areacirclem1  38735  areacirclem4  38738  areacirc  38740  geomcau  38802  isbnd2  38826  ssbnd  38831  heiborlem7  38860  heiborlem8  38861  bfplem2  38866  rrncmslem  38875  rrnequiv  38878  dvrelog3  43224  aks4d1p1p6  43232  rpabsid  43487  irrapxlem1  43938  irrapxlem2  43939  irrapxlem3  43940  irrapxlem5  43942  2timesgt  46412  supxrge  46458  suplesup  46459  xrlexaddrp  46472  xralrple2  46474  infleinflem1  46489  xralrple4  46492  xralrple3  46493  xrralrecnnle  46502  climinf  46726  mullimc  46736  mullimcf  46743  limcrecl  46749  limcleqr  46762  addlimc  46766  0ellimcdiv  46767  limclner  46769  liminflimsupclim  46925  ioodvbdlimc1lem1  47049  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  stoweidlem7  47125  fourierdlem73  47297  fourierdlem87  47311  fourierdlem103  47327  fourierdlem104  47328  sge0iunmptlemre  47533  smflimlem4  47892  fldivexpfllog2  49785  blenre  49794  itscnhlc0yqe  49979  itscnhlc0xyqsol  49985  itschlc0xyqsol  49987  itsclc0xyqsolr  49989  itsclinecirc0in  49995  itsclquadb  49996  itscnhlinecirc02plem3  50004  itscnhlinecirc02p  50005  inlinecirc02plem  50006  inlinecirc02p  50007  amgmwlem  51170