Theorem rpre 12667

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-rp 12660

This theorem is referenced by:  rpxr  12668  rpcn  12669  rpge0  12672  rprege0  12674  rprene0  12676  rpaddcl  12681  rpmulcl  12682  rpdivcl  12684  rpgecl  12687  ledivge1le  12730  addlelt  12773  xralrple  12868  xlemul1  12953  infmrp1  13007  iccdil  13151  ltdifltdiv  13482  modcl  13521  mod0  13524  mulmod0  13525  modge0  13527  modlt  13528  modid0  13545  modabs  13552  modabs2  13553  modcyc  13554  modmuladd  13561  modmuladdnn0  13563  modltm1p1mod  13571  2txmodxeq0  13579  2submod  13580  moddi  13587  modsubdir  13588  modeqmodmin  13589  modirr  13590  rpexpmord  13814  expnlbnd  13876  rennim  14878  cnpart  14879  sqrlem1  14882  sqrlem2  14883  sqrlem4  14885  sqrlem5  14886  sqrlem6  14887  sqrlem7  14888  resqrex  14890  rpsqrtcl  14904  sqreulem  14999  eqsqrt2d  15008  2clim  15209  reccn2  15234  cn1lem  15235  climsqz  15278  climsqz2  15279  rlimsqzlem  15288  climsup  15309  climcau  15310  caucvgrlem2  15314  iseralt  15324  cvgcmp  15456  cvgcmpce  15458  divrcnv  15492  rprisefaccl  15661  efgt1  15753  ef01bndlem  15821  sinltx  15826  stdbdmet  23578  stdbdmopn  23580  met2ndci  23584  cfilucfil  23621  ngptgp  23698  reperflem  23887  iccntr  23890  reconnlem2  23896  opnreen  23900  metdseq0  23923  xlebnum  24034  cphsqrtcl3  24256  iscmet3lem3  24359  iscmet3lem1  24360  iscmet3lem2  24361  caubl  24377  lmcau  24382  bcthlem4  24396  minveclem3b  24497  minveclem3  24498  ivthlem2  24521  ivthlem3  24522  nulmbl2  24605  opnmbllem  24670  itg2const2  24811  itg2mulclem  24816  dveflem  25048  lhop  25085  dvcnvre  25088  aalioulem2  25398  aaliou  25403  aaliou3lem4  25411  ulmcaulem  25458  ulmcau  25459  ulmcn  25463  itgulm  25472  reeff1o  25511  pilem2  25516  logleb  25663  logcj  25666  argimgt0  25672  logdmnrp  25701  logcnlem3  25704  logcnlem4  25705  advlog  25714  efopnlem1  25716  cxple2  25757  cxplt2  25758  cxple3  25761  2irrexpq  25790  cxpcn3  25806  resqrtcn  25807  relogbf  25846  asinneg  25941  atanbndlem  25980  cxplim  26026  cxp2limlem  26030  cxp2lim  26031  cxploglim  26032  cxploglim2  26033  logdiflbnd  26049  harmoniclbnd  26063  harmonicbnd4  26065  chtrpcl  26229  ppiltx  26231  chtleppi  26263  logfacubnd  26274  logfaclbnd  26275  logfacbnd3  26276  logexprlim  26278  bposlem7  26343  bposlem8  26344  bposlem9  26345  chebbnd1  26525  chtppilim  26528  chto1ub  26529  chpo1ub  26533  vmadivsum  26535  rpvmasumlem  26540  dchrisumlem3  26544  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0  26573  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem2  26588  log2sumbnd  26597  selberglem2  26599  selberglem3  26600  selberg  26601  selberg2lem  26603  selberg2  26604  pntrf  26616  pntrmax  26617  pntrsumo1  26618  selbergr  26621  selbergs  26627  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntibndlem1  26642  pntlem3  26662  pntlemp  26663  pntleml  26664  pnt2  26666  padicabvcxp  26685  vacn  28957  nmcvcn  28958  smcnlem  28960  blocnilem  29067  chscllem2  29901  nmcexi  30289  nmcopexi  30290  nmcfnexi  30314  dp2ltsuc  31062  dpval3rp  31076  dplti  31081  dpgti  31082  dpexpp1  31084  dpadd2  31086  pnfinf  31339  sqsscirc1  31760  dya2icoseg2  32145  probfinmeasb  32295  probfinmeasbALTV  32296  signshf  32467  divsqrtid  32474  logdivsqrle  32530  hgt750lem2  32532  subfacval3  33051  opnrebl  34436  opnrebl2  34437  taupilem1  35419  opnmbllem0  35740  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anc  35785  areacirclem1  35792  areacirclem4  35795  areacirc  35797  geomcau  35844  isbnd2  35868  ssbnd  35873  heiborlem7  35902  heiborlem8  35903  bfplem2  35908  rrncmslem  35917  rrnequiv  35920  dvrelog3  40001  aks4d1p1p6  40009  irrapxlem1  40560  irrapxlem2  40561  irrapxlem3  40562  irrapxlem5  40564  neglt  42712  2timesgt  42716  supxrge  42767  suplesup  42768  xrlexaddrp  42781  xralrple2  42783  infleinflem1  42799  xralrple4  42802  xralrple3  42803  xrralrecnnle  42812  climinf  43037  mullimc  43047  mullimcf  43054  limcrecl  43060  limcleqr  43075  addlimc  43079  0ellimcdiv  43080  limclner  43082  liminflimsupclim  43238  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem7  43438  fourierdlem73  43610  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  sge0iunmptlemre  43843  smflimlem4  44196  fldivexpfllog2  45799  blenre  45808  itscnhlc0yqe  45993  itscnhlc0xyqsol  45999  itschlc0xyqsol  46001  itsclc0xyqsolr  46003  itsclinecirc0in  46009  itsclquadb  46010  itscnhlinecirc02plem3  46018  itscnhlinecirc02p  46019  inlinecirc02plem  46020  inlinecirc02p  46021  amgmwlem  46392