Theorem rpre 12891

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℝcr 10997  ℝ⁺crp 12882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-ss 3917  df-rp 12883

This theorem is referenced by:  rpxr  12892  rpcn  12893  rpge0  12896  rprege0  12898  rprene0  12900  neglt  12902  rpaddcl  12906  rpmulcl  12907  rpdivcl  12909  rpgecl  12912  ledivge1le  12955  addlelt  12998  xralrple  13096  xlemul1  13181  infmrp1  13236  iccdil  13382  ltdifltdiv  13730  modcl  13769  mod0  13772  mulmod0  13773  modge0  13775  modlt  13776  modid0  13793  modabs  13800  modabs2  13801  modcyc  13802  muladdmod  13811  modmuladd  13812  modmuladdnn0  13814  modltm1p1mod  13822  2txmodxeq0  13830  2submod  13831  moddi  13838  modsubdir  13839  modeqmodmin  13840  modirr  13841  rpexpmord  14067  expnlbnd  14132  rennim  15138  cnpart  15139  01sqrexlem1  15141  01sqrexlem2  15142  01sqrexlem4  15144  01sqrexlem5  15145  01sqrexlem6  15146  01sqrexlem7  15147  resqrex  15149  rpsqrtcl  15163  sqreulem  15259  eqsqrt2d  15268  2clim  15471  reccn2  15496  cn1lem  15497  climsqz  15540  climsqz2  15541  rlimsqzlem  15548  climsup  15569  climcau  15570  caucvgrlem2  15574  iseralt  15584  cvgcmp  15715  cvgcmpce  15717  divrcnv  15751  rprisefaccl  15922  efgt1  16017  ef01bndlem  16085  sinltx  16090  stdbdmet  24424  stdbdmopn  24426  met2ndci  24430  cfilucfil  24467  ngptgp  24544  reperflem  24727  iccntr  24730  reconnlem2  24736  opnreen  24740  metdseq0  24763  xlebnum  24884  cphsqrtcl3  25107  iscmet3lem3  25210  iscmet3lem1  25211  iscmet3lem2  25212  caubl  25228  lmcau  25233  bcthlem4  25247  minveclem3b  25348  minveclem3  25349  ivthlem2  25373  ivthlem3  25374  nulmbl2  25457  opnmbllem  25522  itg2const2  25662  itg2mulclem  25667  dveflem  25903  lhop  25941  dvcnvre  25944  aalioulem2  26261  aaliou  26266  aaliou3lem4  26274  ulmcaulem  26323  ulmcau  26324  ulmcn  26328  itgulm  26337  reeff1o  26377  pilem2  26382  logleb  26532  logcj  26535  argimgt0  26541  logdmnrp  26570  logcnlem3  26573  logcnlem4  26574  advlog  26583  efopnlem1  26585  cxple2  26626  cxplt2  26627  cxple3  26630  2irrexpq  26660  cxpcn3  26678  resqrtcn  26679  relogbf  26721  asinneg  26816  atanbndlem  26855  cxplim  26902  cxp2limlem  26906  cxp2lim  26907  cxploglim  26908  cxploglim2  26909  logdiflbnd  26925  harmoniclbnd  26939  harmonicbnd4  26941  chtrpcl  27105  ppiltx  27107  chtleppi  27141  logfacubnd  27152  logfaclbnd  27153  logfacbnd3  27154  logexprlim  27156  bposlem7  27221  bposlem8  27222  bposlem9  27223  chebbnd1  27403  chtppilim  27406  chto1ub  27407  chpo1ub  27411  vmadivsum  27413  rpvmasumlem  27418  dchrisumlem3  27422  dchrvmasumlem2  27429  dchrvmasumiflem1  27432  dchrisum0  27451  mudivsum  27461  mulogsumlem  27462  mulogsum  27463  mulog2sumlem2  27466  log2sumbnd  27475  selberglem2  27477  selberglem3  27478  selberg  27479  selberg2lem  27481  selberg2  27482  pntrf  27494  pntrmax  27495  pntrsumo1  27496  selbergr  27499  selbergs  27505  pntrlog2bndlem4  27511  pntrlog2bndlem5  27512  pntibndlem1  27520  pntlem3  27540  pntlemp  27541  pntleml  27542  pnt2  27544  padicabvcxp  27563  vacn  30664  nmcvcn  30665  smcnlem  30667  blocnilem  30774  chscllem2  31608  nmcexi  31996  nmcopexi  31997  nmcfnexi  32021  dp2ltsuc  32856  dpval3rp  32870  dplti  32875  dpgti  32876  dpexpp1  32878  dpadd2  32880  pnfinf  33142  sqsscirc1  33911  dya2icoseg2  34281  probfinmeasb  34431  probfinmeasbALTV  34432  signshf  34591  divsqrtid  34597  logdivsqrle  34653  hgt750lem2  34655  subfacval3  35201  opnrebl  36333  opnrebl2  36334  taupilem1  37334  opnmbllem0  37675  itg2addnclem  37690  itg2addnclem2  37691  itg2addnclem3  37692  itg2addnc  37693  itg2gt0cn  37694  ftc1anclem5  37716  ftc1anclem7  37718  ftc1anc  37720  areacirclem1  37727  areacirclem4  37730  areacirc  37732  geomcau  37778  isbnd2  37802  ssbnd  37807  heiborlem7  37836  heiborlem8  37837  bfplem2  37842  rrncmslem  37851  rrnequiv  37854  dvrelog3  42077  aks4d1p1p6  42085  rpabsid  42333  irrapxlem1  42834  irrapxlem2  42835  irrapxlem3  42836  irrapxlem5  42838  2timesgt  45308  supxrge  45356  suplesup  45357  xrlexaddrp  45370  xralrple2  45372  infleinflem1  45387  xralrple4  45390  xralrple3  45391  xrralrecnnle  45400  climinf  45625  mullimc  45635  mullimcf  45642  limcrecl  45648  limcleqr  45661  addlimc  45665  0ellimcdiv  45666  limclner  45668  liminflimsupclim  45824  ioodvbdlimc1lem1  45948  ioodvbdlimc1lem2  45949  ioodvbdlimc2lem  45951  stoweidlem7  46024  fourierdlem73  46196  fourierdlem87  46210  fourierdlem103  46226  fourierdlem104  46227  sge0iunmptlemre  46432  smflimlem4  46791  fldivexpfllog2  48576  blenre  48585  itscnhlc0yqe  48770  itscnhlc0xyqsol  48776  itschlc0xyqsol  48778  itsclc0xyqsolr  48780  itsclinecirc0in  48786  itsclquadb  48787  itscnhlinecirc02plem3  48795  itscnhlinecirc02p  48796  inlinecirc02plem  48797  inlinecirc02p  48798  amgmwlem  49813