Theorem rpre 13051

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11123  ℝ⁺crp 13042

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3916  df-rp 13043

This theorem is used by:  rpxr  13052  rpcn  13053  rpge0  13056  rprege0  13058  rprene0  13060  neglt  13062  rpaddcl  13066  rpmulcl  13067  rpdivcl  13069  rpgecl  13072  ledivge1le  13115  addlelt  13158  xralrple  13257  xlemul1  13342  infmrp1  13397  iccdil  13543  ltdifltdiv  13895  modcl  13934  mod0  13937  mulmod0  13938  modge0  13940  modlt  13941  modid0  13958  modabs  13965  modabs2  13966  modcyc  13967  muladdmod  13976  modmuladd  13977  modmuladdnn0  13979  modltm1p1mod  13987  2txmodxeq0  13995  2submod  13996  moddi  14003  modsubdir  14004  modeqmodmin  14005  modirr  14006  rpexpmord  14232  expnlbnd  14297  rennim  15326  cnpart  15327  01sqrexlem1  15329  01sqrexlem2  15330  01sqrexlem4  15332  01sqrexlem5  15333  01sqrexlem6  15334  01sqrexlem7  15335  resqrex  15337  rpsqrtcl  15351  sqreulem  15447  eqsqrt2d  15456  2clim  15659  reccn2  15684  cn1lem  15685  climsqz  15728  climsqz2  15729  rlimsqzlem  15736  climsup  15757  climcau  15758  caucvgrlem2  15762  iseralt  15772  cvgcmp  15903  cvgcmpce  15905  divrcnv  15941  rprisefaccl  16110  efgt1  16204  ef01bndlem  16272  sinltx  16277  stdbdmet  24742  stdbdmopn  24744  met2ndci  24748  cfilucfil  24785  ngptgp  24862  reperflem  25045  iccntr  25048  reconnlem2  25054  opnreen  25058  metdseq0  25081  xlebnum  25193  cphsqrtcl3  25415  iscmet3lem3  25518  iscmet3lem1  25519  iscmet3lem2  25520  caubl  25536  lmcau  25541  bcthlem4  25555  minveclem3b  25656  minveclem3  25657  ivthlem2  25680  ivthlem3  25681  nulmbl2  25764  opnmbllem  25829  itg2const2  25969  itg2mulclem  25974  dveflem  26206  lhop  26243  dvcnvre  26246  aalioulem2  26569  aaliou  26574  aaliou3lem4  26582  ulmcaulem  26630  ulmcau  26631  ulmcn  26635  itgulm  26644  reeff1o  26683  pilem2  26688  logleb  26840  logcj  26843  argimgt0  26849  logdmnrp  26878  logcnlem3  26881  logcnlem4  26882  advlog  26891  efopnlem1  26893  cxple2  26934  cxplt2  26935  cxple3  26938  2irrexpq  26968  cxpcn3  26985  resqrtcn  26986  relogbf  27028  asinneg  27123  atanbndlem  27162  cxplim  27208  cxp2limlem  27212  cxp2lim  27213  cxploglim  27214  cxploglim2  27215  logdiflbnd  27231  harmoniclbnd  27245  harmonicbnd4  27247  chtrpcl  27411  ppiltx  27413  chtleppi  27446  logfacubnd  27457  logfaclbnd  27458  logfacbnd3  27459  logexprlim  27461  bposlem7  27526  bposlem8  27527  bposlem9  27528  chebbnd1  27708  chtppilim  27711  chto1ub  27712  chpo1ub  27716  vmadivsum  27718  rpvmasumlem  27723  dchrisumlem3  27727  dchrvmasumlem2  27734  dchrvmasumiflem1  27737  dchrisum0  27756  mudivsum  27766  mulogsumlem  27767  mulogsum  27768  mulog2sumlem2  27771  log2sumbnd  27780  selberglem2  27782  selberglem3  27783  selberg  27784  selberg2lem  27786  selberg2  27787  pntrf  27799  pntrmax  27800  pntrsumo1  27801  selbergr  27804  selbergs  27810  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntibndlem1  27825  pntlem3  27845  pntlemp  27846  pntleml  27847  pnt2  27849  padicabvcxp  27868  vacn  31175  nmcvcn  31176  smcnlem  31178  blocnilem  31285  chscllem2  32119  nmcexi  32507  nmcopexi  32508  nmcfnexi  32532  dp2ltsuc  33331  dpval3rp  33345  dplti  33350  dpgti  33351  dpexpp1  33353  dpadd2  33355  pnfinf  33623  sqsscirc1  34418  dya2icoseg2  34789  probfinmeasb  34939  probfinmeasbALTV  34940  signshf  35096  divsqrtid  35102  logdivsqrle  35158  hgt750lem2  35160  subfacval3  35768  opnrebl  36939  opnrebl2  36940  taupilem1  38073  opnmbllem0  38405  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  ftc1anclem5  38446  ftc1anclem7  38448  ftc1anc  38450  areacirclem1  38457  areacirclem4  38460  areacirc  38462  geomcau  38509  isbnd2  38533  ssbnd  38538  heiborlem7  38567  heiborlem8  38568  bfplem2  38573  rrncmslem  38582  rrnequiv  38585  dvrelog3  42931  aks4d1p1p6  42939  rpabsid  43196  irrapxlem1  43663  irrapxlem2  43664  irrapxlem3  43665  irrapxlem5  43667  2timesgt  46121  supxrge  46168  suplesup  46169  xrlexaddrp  46182  xralrple2  46184  infleinflem1  46199  xralrple4  46202  xralrple3  46203  xrralrecnnle  46212  climinf  46436  mullimc  46446  mullimcf  46453  limcrecl  46459  limcleqr  46472  addlimc  46476  0ellimcdiv  46477  limclner  46479  liminflimsupclim  46635  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  stoweidlem7  46835  fourierdlem73  47007  fourierdlem87  47021  fourierdlem103  47037  fourierdlem104  47038  sge0iunmptlemre  47243  smflimlem4  47602  fldivexpfllog2  49495  blenre  49504  itscnhlc0yqe  49689  itscnhlc0xyqsol  49695  itschlc0xyqsol  49697  itsclc0xyqsolr  49699  itsclinecirc0in  49705  itsclquadb  49706  itscnhlinecirc02plem3  49714  itscnhlinecirc02p  49715  inlinecirc02plem  49716  inlinecirc02p  49717  amgmwlem  50820