Theorem rpre 13017

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11128  ℝ⁺crp 13008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943  df-rp 13009

This theorem is referenced by:  rpxr  13018  rpcn  13019  rpge0  13022  rprege0  13024  rprene0  13026  rpaddcl  13031  rpmulcl  13032  rpdivcl  13034  rpgecl  13037  ledivge1le  13080  addlelt  13123  xralrple  13221  xlemul1  13306  infmrp1  13361  iccdil  13507  ltdifltdiv  13851  modcl  13890  mod0  13893  mulmod0  13894  modge0  13896  modlt  13897  modid0  13914  modabs  13921  modabs2  13922  modcyc  13923  muladdmod  13930  modmuladd  13931  modmuladdnn0  13933  modltm1p1mod  13941  2txmodxeq0  13949  2submod  13950  moddi  13957  modsubdir  13958  modeqmodmin  13959  modirr  13960  rpexpmord  14186  expnlbnd  14251  rennim  15258  cnpart  15259  01sqrexlem1  15261  01sqrexlem2  15262  01sqrexlem4  15264  01sqrexlem5  15265  01sqrexlem6  15266  01sqrexlem7  15267  resqrex  15269  rpsqrtcl  15283  sqreulem  15378  eqsqrt2d  15387  2clim  15588  reccn2  15613  cn1lem  15614  climsqz  15657  climsqz2  15658  rlimsqzlem  15665  climsup  15686  climcau  15687  caucvgrlem2  15691  iseralt  15701  cvgcmp  15832  cvgcmpce  15834  divrcnv  15868  rprisefaccl  16039  efgt1  16134  ef01bndlem  16202  sinltx  16207  stdbdmet  24455  stdbdmopn  24457  met2ndci  24461  cfilucfil  24498  ngptgp  24575  reperflem  24758  iccntr  24761  reconnlem2  24767  opnreen  24771  metdseq0  24794  xlebnum  24915  cphsqrtcl3  25139  iscmet3lem3  25242  iscmet3lem1  25243  iscmet3lem2  25244  caubl  25260  lmcau  25265  bcthlem4  25279  minveclem3b  25380  minveclem3  25381  ivthlem2  25405  ivthlem3  25406  nulmbl2  25489  opnmbllem  25554  itg2const2  25694  itg2mulclem  25699  dveflem  25935  lhop  25973  dvcnvre  25976  aalioulem2  26293  aaliou  26298  aaliou3lem4  26306  ulmcaulem  26355  ulmcau  26356  ulmcn  26360  itgulm  26369  reeff1o  26409  pilem2  26414  logleb  26564  logcj  26567  argimgt0  26573  logdmnrp  26602  logcnlem3  26605  logcnlem4  26606  advlog  26615  efopnlem1  26617  cxple2  26658  cxplt2  26659  cxple3  26662  2irrexpq  26692  cxpcn3  26710  resqrtcn  26711  relogbf  26753  asinneg  26848  atanbndlem  26887  cxplim  26934  cxp2limlem  26938  cxp2lim  26939  cxploglim  26940  cxploglim2  26941  logdiflbnd  26957  harmoniclbnd  26971  harmonicbnd4  26973  chtrpcl  27137  ppiltx  27139  chtleppi  27173  logfacubnd  27184  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  bposlem7  27253  bposlem8  27254  bposlem9  27255  chebbnd1  27435  chtppilim  27438  chto1ub  27439  chpo1ub  27443  vmadivsum  27445  rpvmasumlem  27450  dchrisumlem3  27454  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0  27483  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem2  27498  log2sumbnd  27507  selberglem2  27509  selberglem3  27510  selberg  27511  selberg2lem  27513  selberg2  27514  pntrf  27526  pntrmax  27527  pntrsumo1  27528  selbergr  27531  selbergs  27537  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntibndlem1  27552  pntlem3  27572  pntlemp  27573  pntleml  27574  pnt2  27576  padicabvcxp  27595  vacn  30675  nmcvcn  30676  smcnlem  30678  blocnilem  30785  chscllem2  31619  nmcexi  32007  nmcopexi  32008  nmcfnexi  32032  dp2ltsuc  32860  dpval3rp  32874  dplti  32879  dpgti  32880  dpexpp1  32882  dpadd2  32884  pnfinf  33181  sqsscirc1  33939  dya2icoseg2  34310  probfinmeasb  34460  probfinmeasbALTV  34461  signshf  34620  divsqrtid  34626  logdivsqrle  34682  hgt750lem2  34684  subfacval3  35211  opnrebl  36338  opnrebl2  36339  taupilem1  37339  opnmbllem0  37680  itg2addnclem  37695  itg2addnclem2  37696  itg2addnclem3  37697  itg2addnc  37698  itg2gt0cn  37699  ftc1anclem5  37721  ftc1anclem7  37723  ftc1anc  37725  areacirclem1  37732  areacirclem4  37735  areacirc  37737  geomcau  37783  isbnd2  37807  ssbnd  37812  heiborlem7  37841  heiborlem8  37842  bfplem2  37847  rrncmslem  37856  rrnequiv  37859  dvrelog3  42078  aks4d1p1p6  42086  rpabsid  42370  irrapxlem1  42845  irrapxlem2  42846  irrapxlem3  42847  irrapxlem5  42849  neglt  45313  2timesgt  45317  supxrge  45365  suplesup  45366  xrlexaddrp  45379  xralrple2  45381  infleinflem1  45397  xralrple4  45400  xralrple3  45401  xrralrecnnle  45410  climinf  45635  mullimc  45645  mullimcf  45652  limcrecl  45658  limcleqr  45673  addlimc  45677  0ellimcdiv  45678  limclner  45680  liminflimsupclim  45836  ioodvbdlimc1lem1  45960  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stoweidlem7  46036  fourierdlem73  46208  fourierdlem87  46222  fourierdlem103  46238  fourierdlem104  46239  sge0iunmptlemre  46444  smflimlem4  46803  fldivexpfllog2  48545  blenre  48554  itscnhlc0yqe  48739  itscnhlc0xyqsol  48745  itschlc0xyqsol  48747  itsclc0xyqsolr  48749  itsclinecirc0in  48755  itsclquadb  48756  itscnhlinecirc02plem3  48764  itscnhlinecirc02p  48765  inlinecirc02plem  48766  inlinecirc02p  48767  amgmwlem  49666