Theorem rpre 12982

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-rp 12975

This theorem is referenced by:  rpxr  12983  rpcn  12984  rpge0  12987  rprege0  12989  rprene0  12991  rpaddcl  12996  rpmulcl  12997  rpdivcl  12999  rpgecl  13002  ledivge1le  13045  addlelt  13088  xralrple  13184  xlemul1  13269  infmrp1  13323  iccdil  13467  ltdifltdiv  13799  modcl  13838  mod0  13841  mulmod0  13842  modge0  13844  modlt  13845  modid0  13862  modabs  13869  modabs2  13870  modcyc  13871  modmuladd  13878  modmuladdnn0  13880  modltm1p1mod  13888  2txmodxeq0  13896  2submod  13897  moddi  13904  modsubdir  13905  modeqmodmin  13906  modirr  13907  rpexpmord  14133  expnlbnd  14196  rennim  15186  cnpart  15187  01sqrexlem1  15189  01sqrexlem2  15190  01sqrexlem4  15192  01sqrexlem5  15193  01sqrexlem6  15194  01sqrexlem7  15195  resqrex  15197  rpsqrtcl  15211  sqreulem  15306  eqsqrt2d  15315  2clim  15516  reccn2  15541  cn1lem  15542  climsqz  15585  climsqz2  15586  rlimsqzlem  15595  climsup  15616  climcau  15617  caucvgrlem2  15621  iseralt  15631  cvgcmp  15762  cvgcmpce  15764  divrcnv  15798  rprisefaccl  15967  efgt1  16059  ef01bndlem  16127  sinltx  16132  stdbdmet  24025  stdbdmopn  24027  met2ndci  24031  cfilucfil  24068  ngptgp  24145  reperflem  24334  iccntr  24337  reconnlem2  24343  opnreen  24347  metdseq0  24370  xlebnum  24481  cphsqrtcl3  24704  iscmet3lem3  24807  iscmet3lem1  24808  iscmet3lem2  24809  caubl  24825  lmcau  24830  bcthlem4  24844  minveclem3b  24945  minveclem3  24946  ivthlem2  24969  ivthlem3  24970  nulmbl2  25053  opnmbllem  25118  itg2const2  25259  itg2mulclem  25264  dveflem  25496  lhop  25533  dvcnvre  25536  aalioulem2  25846  aaliou  25851  aaliou3lem4  25859  ulmcaulem  25906  ulmcau  25907  ulmcn  25911  itgulm  25920  reeff1o  25959  pilem2  25964  logleb  26111  logcj  26114  argimgt0  26120  logdmnrp  26149  logcnlem3  26152  logcnlem4  26153  advlog  26162  efopnlem1  26164  cxple2  26205  cxplt2  26206  cxple3  26209  2irrexpq  26239  cxpcn3  26256  resqrtcn  26257  relogbf  26296  asinneg  26391  atanbndlem  26430  cxplim  26476  cxp2limlem  26480  cxp2lim  26481  cxploglim  26482  cxploglim2  26483  logdiflbnd  26499  harmoniclbnd  26513  harmonicbnd4  26515  chtrpcl  26679  ppiltx  26681  chtleppi  26713  logfacubnd  26724  logfaclbnd  26725  logfacbnd3  26726  logexprlim  26728  bposlem7  26793  bposlem8  26794  bposlem9  26795  chebbnd1  26975  chtppilim  26978  chto1ub  26979  chpo1ub  26983  vmadivsum  26985  rpvmasumlem  26990  dchrisumlem3  26994  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0  27023  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  mulog2sumlem2  27038  log2sumbnd  27047  selberglem2  27049  selberglem3  27050  selberg  27051  selberg2lem  27053  selberg2  27054  pntrf  27066  pntrmax  27067  pntrsumo1  27068  selbergr  27071  selbergs  27077  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntibndlem1  27092  pntlem3  27112  pntlemp  27113  pntleml  27114  pnt2  27116  padicabvcxp  27135  vacn  29947  nmcvcn  29948  smcnlem  29950  blocnilem  30057  chscllem2  30891  nmcexi  31279  nmcopexi  31280  nmcfnexi  31304  dp2ltsuc  32052  dpval3rp  32066  dplti  32071  dpgti  32072  dpexpp1  32074  dpadd2  32076  pnfinf  32329  sqsscirc1  32888  dya2icoseg2  33277  probfinmeasb  33427  probfinmeasbALTV  33428  signshf  33599  divsqrtid  33606  logdivsqrle  33662  hgt750lem2  33664  subfacval3  34180  opnrebl  35205  opnrebl2  35206  taupilem1  36202  opnmbllem0  36524  itg2addnclem  36539  itg2addnclem2  36540  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anc  36569  areacirclem1  36576  areacirclem4  36579  areacirc  36581  geomcau  36627  isbnd2  36651  ssbnd  36656  heiborlem7  36685  heiborlem8  36686  bfplem2  36691  rrncmslem  36700  rrnequiv  36703  dvrelog3  40930  aks4d1p1p6  40938  irrapxlem1  41560  irrapxlem2  41561  irrapxlem3  41562  irrapxlem5  41564  neglt  43994  2timesgt  43998  supxrge  44048  suplesup  44049  xrlexaddrp  44062  xralrple2  44064  infleinflem1  44080  xralrple4  44083  xralrple3  44084  xrralrecnnle  44093  climinf  44322  mullimc  44332  mullimcf  44339  limcrecl  44345  limcleqr  44360  addlimc  44364  0ellimcdiv  44365  limclner  44367  liminflimsupclim  44523  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem7  44723  fourierdlem73  44895  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  sge0iunmptlemre  45131  smflimlem4  45490  fldivexpfllog2  47251  blenre  47260  itscnhlc0yqe  47445  itscnhlc0xyqsol  47451  itschlc0xyqsol  47453  itsclc0xyqsolr  47455  itsclinecirc0in  47461  itsclquadb  47462  itscnhlinecirc02plem3  47470  itscnhlinecirc02p  47471  inlinecirc02plem  47472  inlinecirc02p  47473  amgmwlem  47849