Theorem rpre 13043

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℝ⁺crp 13034

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-rp 13035

This theorem is referenced by:  rpxr  13044  rpcn  13045  rpge0  13048  rprege0  13050  rprene0  13052  rpaddcl  13057  rpmulcl  13058  rpdivcl  13060  rpgecl  13063  ledivge1le  13106  addlelt  13149  xralrple  13247  xlemul1  13332  infmrp1  13386  iccdil  13530  ltdifltdiv  13874  modcl  13913  mod0  13916  mulmod0  13917  modge0  13919  modlt  13920  modid0  13937  modabs  13944  modabs2  13945  modcyc  13946  muladdmod  13953  modmuladd  13954  modmuladdnn0  13956  modltm1p1mod  13964  2txmodxeq0  13972  2submod  13973  moddi  13980  modsubdir  13981  modeqmodmin  13982  modirr  13983  rpexpmord  14208  expnlbnd  14272  rennim  15278  cnpart  15279  01sqrexlem1  15281  01sqrexlem2  15282  01sqrexlem4  15284  01sqrexlem5  15285  01sqrexlem6  15286  01sqrexlem7  15287  resqrex  15289  rpsqrtcl  15303  sqreulem  15398  eqsqrt2d  15407  2clim  15608  reccn2  15633  cn1lem  15634  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  climsup  15706  climcau  15707  caucvgrlem2  15711  iseralt  15721  cvgcmp  15852  cvgcmpce  15854  divrcnv  15888  rprisefaccl  16059  efgt1  16152  ef01bndlem  16220  sinltx  16225  stdbdmet  24529  stdbdmopn  24531  met2ndci  24535  cfilucfil  24572  ngptgp  24649  reperflem  24840  iccntr  24843  reconnlem2  24849  opnreen  24853  metdseq0  24876  xlebnum  24997  cphsqrtcl3  25221  iscmet3lem3  25324  iscmet3lem1  25325  iscmet3lem2  25326  caubl  25342  lmcau  25347  bcthlem4  25361  minveclem3b  25462  minveclem3  25463  ivthlem2  25487  ivthlem3  25488  nulmbl2  25571  opnmbllem  25636  itg2const2  25776  itg2mulclem  25781  dveflem  26017  lhop  26055  dvcnvre  26058  aalioulem2  26375  aaliou  26380  aaliou3lem4  26388  ulmcaulem  26437  ulmcau  26438  ulmcn  26442  itgulm  26451  reeff1o  26491  pilem2  26496  logleb  26645  logcj  26648  argimgt0  26654  logdmnrp  26683  logcnlem3  26686  logcnlem4  26687  advlog  26696  efopnlem1  26698  cxple2  26739  cxplt2  26740  cxple3  26743  2irrexpq  26773  cxpcn3  26791  resqrtcn  26792  relogbf  26834  asinneg  26929  atanbndlem  26968  cxplim  27015  cxp2limlem  27019  cxp2lim  27020  cxploglim  27021  cxploglim2  27022  logdiflbnd  27038  harmoniclbnd  27052  harmonicbnd4  27054  chtrpcl  27218  ppiltx  27220  chtleppi  27254  logfacubnd  27265  logfaclbnd  27266  logfacbnd3  27267  logexprlim  27269  bposlem7  27334  bposlem8  27335  bposlem9  27336  chebbnd1  27516  chtppilim  27519  chto1ub  27520  chpo1ub  27524  vmadivsum  27526  rpvmasumlem  27531  dchrisumlem3  27535  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0  27564  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  mulog2sumlem2  27579  log2sumbnd  27588  selberglem2  27590  selberglem3  27591  selberg  27592  selberg2lem  27594  selberg2  27595  pntrf  27607  pntrmax  27608  pntrsumo1  27609  selbergr  27612  selbergs  27618  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntibndlem1  27633  pntlem3  27653  pntlemp  27654  pntleml  27655  pnt2  27657  padicabvcxp  27676  vacn  30713  nmcvcn  30714  smcnlem  30716  blocnilem  30823  chscllem2  31657  nmcexi  32045  nmcopexi  32046  nmcfnexi  32070  dp2ltsuc  32868  dpval3rp  32882  dplti  32887  dpgti  32888  dpexpp1  32890  dpadd2  32892  pnfinf  33190  sqsscirc1  33907  dya2icoseg2  34280  probfinmeasb  34430  probfinmeasbALTV  34431  signshf  34603  divsqrtid  34609  logdivsqrle  34665  hgt750lem2  34667  subfacval3  35194  opnrebl  36321  opnrebl2  36322  taupilem1  37322  opnmbllem0  37663  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anc  37708  areacirclem1  37715  areacirclem4  37718  areacirc  37720  geomcau  37766  isbnd2  37790  ssbnd  37795  heiborlem7  37824  heiborlem8  37825  bfplem2  37830  rrncmslem  37839  rrnequiv  37842  dvrelog3  42066  aks4d1p1p6  42074  rpabsid  42356  irrapxlem1  42833  irrapxlem2  42834  irrapxlem3  42835  irrapxlem5  42837  neglt  45296  2timesgt  45300  supxrge  45349  suplesup  45350  xrlexaddrp  45363  xralrple2  45365  infleinflem1  45381  xralrple4  45384  xralrple3  45385  xrralrecnnle  45394  climinf  45621  mullimc  45631  mullimcf  45638  limcrecl  45644  limcleqr  45659  addlimc  45663  0ellimcdiv  45664  limclner  45666  liminflimsupclim  45822  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem7  46022  fourierdlem73  46194  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  sge0iunmptlemre  46430  smflimlem4  46789  fldivexpfllog2  48486  blenre  48495  itscnhlc0yqe  48680  itscnhlc0xyqsol  48686  itschlc0xyqsol  48688  itsclc0xyqsolr  48690  itsclinecirc0in  48696  itsclquadb  48697  itscnhlinecirc02plem3  48705  itscnhlinecirc02p  48706  inlinecirc02plem  48707  inlinecirc02p  48708  amgmwlem  49321