Theorem rpre 12736

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 10868  ℝ⁺crp 12728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3433  df-in 3895  df-ss 3905  df-rp 12729

This theorem is referenced by:  rpxr  12737  rpcn  12738  rpge0  12741  rprege0  12743  rprene0  12745  rpaddcl  12750  rpmulcl  12751  rpdivcl  12753  rpgecl  12756  ledivge1le  12799  addlelt  12842  xralrple  12937  xlemul1  13022  infmrp1  13076  iccdil  13220  ltdifltdiv  13552  modcl  13591  mod0  13594  mulmod0  13595  modge0  13597  modlt  13598  modid0  13615  modabs  13622  modabs2  13623  modcyc  13624  modmuladd  13631  modmuladdnn0  13633  modltm1p1mod  13641  2txmodxeq0  13649  2submod  13650  moddi  13657  modsubdir  13658  modeqmodmin  13659  modirr  13660  rpexpmord  13884  expnlbnd  13946  rennim  14948  cnpart  14949  sqrlem1  14952  sqrlem2  14953  sqrlem4  14955  sqrlem5  14956  sqrlem6  14957  sqrlem7  14958  resqrex  14960  rpsqrtcl  14974  sqreulem  15069  eqsqrt2d  15078  2clim  15279  reccn2  15304  cn1lem  15305  climsqz  15348  climsqz2  15349  rlimsqzlem  15358  climsup  15379  climcau  15380  caucvgrlem2  15384  iseralt  15394  cvgcmp  15526  cvgcmpce  15528  divrcnv  15562  rprisefaccl  15731  efgt1  15823  ef01bndlem  15891  sinltx  15896  stdbdmet  23670  stdbdmopn  23672  met2ndci  23676  cfilucfil  23713  ngptgp  23790  reperflem  23979  iccntr  23982  reconnlem2  23988  opnreen  23992  metdseq0  24015  xlebnum  24126  cphsqrtcl3  24349  iscmet3lem3  24452  iscmet3lem1  24453  iscmet3lem2  24454  caubl  24470  lmcau  24475  bcthlem4  24489  minveclem3b  24590  minveclem3  24591  ivthlem2  24614  ivthlem3  24615  nulmbl2  24698  opnmbllem  24763  itg2const2  24904  itg2mulclem  24909  dveflem  25141  lhop  25178  dvcnvre  25181  aalioulem2  25491  aaliou  25496  aaliou3lem4  25504  ulmcaulem  25551  ulmcau  25552  ulmcn  25556  itgulm  25565  reeff1o  25604  pilem2  25609  logleb  25756  logcj  25759  argimgt0  25765  logdmnrp  25794  logcnlem3  25797  logcnlem4  25798  advlog  25807  efopnlem1  25809  cxple2  25850  cxplt2  25851  cxple3  25854  2irrexpq  25883  cxpcn3  25899  resqrtcn  25900  relogbf  25939  asinneg  26034  atanbndlem  26073  cxplim  26119  cxp2limlem  26123  cxp2lim  26124  cxploglim  26125  cxploglim2  26126  logdiflbnd  26142  harmoniclbnd  26156  harmonicbnd4  26158  chtrpcl  26322  ppiltx  26324  chtleppi  26356  logfacubnd  26367  logfaclbnd  26368  logfacbnd3  26369  logexprlim  26371  bposlem7  26436  bposlem8  26437  bposlem9  26438  chebbnd1  26618  chtppilim  26621  chto1ub  26622  chpo1ub  26626  vmadivsum  26628  rpvmasumlem  26633  dchrisumlem3  26637  dchrvmasumlem2  26644  dchrvmasumiflem1  26647  dchrisum0  26666  mudivsum  26676  mulogsumlem  26677  mulogsum  26678  mulog2sumlem2  26681  log2sumbnd  26690  selberglem2  26692  selberglem3  26693  selberg  26694  selberg2lem  26696  selberg2  26697  pntrf  26709  pntrmax  26710  pntrsumo1  26711  selbergr  26714  selbergs  26720  pntrlog2bndlem4  26726  pntrlog2bndlem5  26727  pntibndlem1  26735  pntlem3  26755  pntlemp  26756  pntleml  26757  pnt2  26759  padicabvcxp  26778  vacn  29053  nmcvcn  29054  smcnlem  29056  blocnilem  29163  chscllem2  29997  nmcexi  30385  nmcopexi  30386  nmcfnexi  30410  dp2ltsuc  31157  dpval3rp  31171  dplti  31176  dpgti  31177  dpexpp1  31179  dpadd2  31181  pnfinf  31434  sqsscirc1  31855  dya2icoseg2  32242  probfinmeasb  32392  probfinmeasbALTV  32393  signshf  32564  divsqrtid  32571  logdivsqrle  32627  hgt750lem2  32629  subfacval3  33148  opnrebl  34506  opnrebl2  34507  taupilem1  35489  opnmbllem0  35810  itg2addnclem  35825  itg2addnclem2  35826  itg2addnclem3  35827  itg2addnc  35828  itg2gt0cn  35829  ftc1anclem5  35851  ftc1anclem7  35853  ftc1anc  35855  areacirclem1  35862  areacirclem4  35865  areacirc  35867  geomcau  35914  isbnd2  35938  ssbnd  35943  heiborlem7  35972  heiborlem8  35973  bfplem2  35978  rrncmslem  35987  rrnequiv  35990  dvrelog3  40070  aks4d1p1p6  40078  irrapxlem1  40641  irrapxlem2  40642  irrapxlem3  40643  irrapxlem5  40645  neglt  42793  2timesgt  42797  supxrge  42847  suplesup  42848  xrlexaddrp  42861  xralrple2  42863  infleinflem1  42879  xralrple4  42882  xralrple3  42883  xrralrecnnle  42892  climinf  43117  mullimc  43127  mullimcf  43134  limcrecl  43140  limcleqr  43155  addlimc  43159  0ellimcdiv  43160  limclner  43162  liminflimsupclim  43318  ioodvbdlimc1lem1  43442  ioodvbdlimc1lem2  43443  ioodvbdlimc2lem  43445  stoweidlem7  43518  fourierdlem73  43690  fourierdlem87  43704  fourierdlem103  43720  fourierdlem104  43721  sge0iunmptlemre  43923  smflimlem4  44276  fldivexpfllog2  45878  blenre  45887  itscnhlc0yqe  46072  itscnhlc0xyqsol  46078  itschlc0xyqsol  46080  itsclc0xyqsolr  46082  itsclinecirc0in  46088  itsclquadb  46089  itscnhlinecirc02plem3  46097  itscnhlinecirc02p  46098  inlinecirc02plem  46099  inlinecirc02p  46100  amgmwlem  46473