Theorem rpre 13040

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℝ⁺crp 13031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-ss 3979  df-rp 13032

This theorem is referenced by:  rpxr  13041  rpcn  13042  rpge0  13045  rprege0  13047  rprene0  13049  rpaddcl  13054  rpmulcl  13055  rpdivcl  13057  rpgecl  13060  ledivge1le  13103  addlelt  13146  xralrple  13243  xlemul1  13328  infmrp1  13382  iccdil  13526  ltdifltdiv  13870  modcl  13909  mod0  13912  mulmod0  13913  modge0  13915  modlt  13916  modid0  13933  modabs  13940  modabs2  13941  modcyc  13942  muladdmod  13949  modmuladd  13950  modmuladdnn0  13952  modltm1p1mod  13960  2txmodxeq0  13968  2submod  13969  moddi  13976  modsubdir  13977  modeqmodmin  13978  modirr  13979  rpexpmord  14204  expnlbnd  14268  rennim  15274  cnpart  15275  01sqrexlem1  15277  01sqrexlem2  15278  01sqrexlem4  15280  01sqrexlem5  15281  01sqrexlem6  15282  01sqrexlem7  15283  resqrex  15285  rpsqrtcl  15299  sqreulem  15394  eqsqrt2d  15403  2clim  15604  reccn2  15629  cn1lem  15630  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  climsup  15702  climcau  15703  caucvgrlem2  15707  iseralt  15717  cvgcmp  15848  cvgcmpce  15850  divrcnv  15884  rprisefaccl  16055  efgt1  16148  ef01bndlem  16216  sinltx  16221  stdbdmet  24544  stdbdmopn  24546  met2ndci  24550  cfilucfil  24587  ngptgp  24664  reperflem  24853  iccntr  24856  reconnlem2  24862  opnreen  24866  metdseq0  24889  xlebnum  25010  cphsqrtcl3  25234  iscmet3lem3  25337  iscmet3lem1  25338  iscmet3lem2  25339  caubl  25355  lmcau  25360  bcthlem4  25374  minveclem3b  25475  minveclem3  25476  ivthlem2  25500  ivthlem3  25501  nulmbl2  25584  opnmbllem  25649  itg2const2  25790  itg2mulclem  25795  dveflem  26031  lhop  26069  dvcnvre  26072  aalioulem2  26389  aaliou  26394  aaliou3lem4  26402  ulmcaulem  26451  ulmcau  26452  ulmcn  26456  itgulm  26465  reeff1o  26505  pilem2  26510  logleb  26659  logcj  26662  argimgt0  26668  logdmnrp  26697  logcnlem3  26700  logcnlem4  26701  advlog  26710  efopnlem1  26712  cxple2  26753  cxplt2  26754  cxple3  26757  2irrexpq  26787  cxpcn3  26805  resqrtcn  26806  relogbf  26848  asinneg  26943  atanbndlem  26982  cxplim  27029  cxp2limlem  27033  cxp2lim  27034  cxploglim  27035  cxploglim2  27036  logdiflbnd  27052  harmoniclbnd  27066  harmonicbnd4  27068  chtrpcl  27232  ppiltx  27234  chtleppi  27268  logfacubnd  27279  logfaclbnd  27280  logfacbnd3  27281  logexprlim  27283  bposlem7  27348  bposlem8  27349  bposlem9  27350  chebbnd1  27530  chtppilim  27533  chto1ub  27534  chpo1ub  27538  vmadivsum  27540  rpvmasumlem  27545  dchrisumlem3  27549  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0  27578  mudivsum  27588  mulogsumlem  27589  mulogsum  27590  mulog2sumlem2  27593  log2sumbnd  27602  selberglem2  27604  selberglem3  27605  selberg  27606  selberg2lem  27608  selberg2  27609  pntrf  27621  pntrmax  27622  pntrsumo1  27623  selbergr  27626  selbergs  27632  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntibndlem1  27647  pntlem3  27667  pntlemp  27668  pntleml  27669  pnt2  27671  padicabvcxp  27690  vacn  30722  nmcvcn  30723  smcnlem  30725  blocnilem  30832  chscllem2  31666  nmcexi  32054  nmcopexi  32055  nmcfnexi  32079  dp2ltsuc  32852  dpval3rp  32866  dplti  32871  dpgti  32872  dpexpp1  32874  dpadd2  32876  pnfinf  33172  sqsscirc1  33868  dya2icoseg2  34259  probfinmeasb  34409  probfinmeasbALTV  34410  signshf  34581  divsqrtid  34587  logdivsqrle  34643  hgt750lem2  34645  subfacval3  35173  opnrebl  36302  opnrebl2  36303  taupilem1  37303  opnmbllem0  37642  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anc  37687  areacirclem1  37694  areacirclem4  37697  areacirc  37699  geomcau  37745  isbnd2  37769  ssbnd  37774  heiborlem7  37803  heiborlem8  37804  bfplem2  37809  rrncmslem  37818  rrnequiv  37821  dvrelog3  42046  aks4d1p1p6  42054  rpabsid  42334  irrapxlem1  42809  irrapxlem2  42810  irrapxlem3  42811  irrapxlem5  42813  neglt  45234  2timesgt  45238  supxrge  45287  suplesup  45288  xrlexaddrp  45301  xralrple2  45303  infleinflem1  45319  xralrple4  45322  xralrple3  45323  xrralrecnnle  45332  climinf  45561  mullimc  45571  mullimcf  45578  limcrecl  45584  limcleqr  45599  addlimc  45603  0ellimcdiv  45604  limclner  45606  liminflimsupclim  45762  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem7  45962  fourierdlem73  46134  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  sge0iunmptlemre  46370  smflimlem4  46729  fldivexpfllog2  48414  blenre  48423  itscnhlc0yqe  48608  itscnhlc0xyqsol  48614  itschlc0xyqsol  48616  itsclc0xyqsolr  48618  itsclinecirc0in  48624  itsclquadb  48625  itscnhlinecirc02plem3  48633  itscnhlinecirc02p  48634  inlinecirc02plem  48635  inlinecirc02p  48636  amgmwlem  49032