Theorem rpre 13041

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11114  ℝ⁺crp 13032

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-ss 3923  df-rp 13033

This theorem is used by:  rpxr  13042  rpcn  13043  rpge0  13046  rprege0  13048  rprene0  13050  neglt  13052  rpaddcl  13056  rpmulcl  13057  rpdivcl  13059  rpgecl  13062  ledivge1le  13105  addlelt  13148  xralrple  13247  xlemul1  13332  infmrp1  13387  iccdil  13533  ltdifltdiv  13885  modcl  13924  mod0  13927  mulmod0  13928  modge0  13930  modlt  13931  modid0  13948  modabs  13955  modabs2  13956  modcyc  13957  muladdmod  13966  modmuladd  13967  modmuladdnn0  13969  modltm1p1mod  13977  2txmodxeq0  13985  2submod  13986  moddi  13993  modsubdir  13994  modeqmodmin  13995  modirr  13996  rpexpmord  14222  expnlbnd  14287  rennim  15314  cnpart  15315  01sqrexlem1  15317  01sqrexlem2  15318  01sqrexlem4  15320  01sqrexlem5  15321  01sqrexlem6  15322  01sqrexlem7  15323  resqrex  15325  rpsqrtcl  15339  sqreulem  15435  eqsqrt2d  15444  2clim  15647  reccn2  15672  cn1lem  15673  climsqz  15716  climsqz2  15717  rlimsqzlem  15724  climsup  15745  climcau  15746  caucvgrlem2  15750  iseralt  15760  cvgcmp  15891  cvgcmpce  15893  divrcnv  15929  rprisefaccl  16100  efgt1  16194  ef01bndlem  16262  sinltx  16267  stdbdmet  24724  stdbdmopn  24726  met2ndci  24730  cfilucfil  24767  ngptgp  24844  reperflem  25027  iccntr  25030  reconnlem2  25036  opnreen  25040  metdseq0  25063  xlebnum  25175  cphsqrtcl3  25397  iscmet3lem3  25500  iscmet3lem1  25501  iscmet3lem2  25502  caubl  25518  lmcau  25523  bcthlem4  25537  minveclem3b  25638  minveclem3  25639  ivthlem2  25662  ivthlem3  25663  nulmbl2  25746  opnmbllem  25811  itg2const2  25951  itg2mulclem  25956  dveflem  26189  lhop  26226  dvcnvre  26229  aalioulem2  26547  aaliou  26552  aaliou3lem4  26560  ulmcaulem  26608  ulmcau  26609  ulmcn  26613  itgulm  26622  reeff1o  26661  pilem2  26666  logleb  26819  logcj  26822  argimgt0  26828  logdmnrp  26857  logcnlem3  26860  logcnlem4  26861  advlog  26870  efopnlem1  26872  cxple2  26913  cxplt2  26914  cxple3  26917  2irrexpq  26947  cxpcn3  26964  resqrtcn  26965  relogbf  27007  asinneg  27102  atanbndlem  27141  cxplim  27187  cxp2limlem  27191  cxp2lim  27192  cxploglim  27193  cxploglim2  27194  logdiflbnd  27210  harmoniclbnd  27224  harmonicbnd4  27226  chtrpcl  27390  ppiltx  27392  chtleppi  27425  logfacubnd  27436  logfaclbnd  27437  logfacbnd3  27438  logexprlim  27440  bposlem7  27505  bposlem8  27506  bposlem9  27507  chebbnd1  27687  chtppilim  27690  chto1ub  27691  chpo1ub  27695  vmadivsum  27697  rpvmasumlem  27702  dchrisumlem3  27706  dchrvmasumlem2  27713  dchrvmasumiflem1  27716  dchrisum0  27735  mudivsum  27745  mulogsumlem  27746  mulogsum  27747  mulog2sumlem2  27750  log2sumbnd  27759  selberglem2  27761  selberglem3  27762  selberg  27763  selberg2lem  27765  selberg2  27766  pntrf  27778  pntrmax  27779  pntrsumo1  27780  selbergr  27783  selbergs  27789  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntibndlem1  27804  pntlem3  27824  pntlemp  27825  pntleml  27826  pnt2  27828  padicabvcxp  27847  vacn  31117  nmcvcn  31118  smcnlem  31120  blocnilem  31227  chscllem2  32061  nmcexi  32449  nmcopexi  32450  nmcfnexi  32474  dp2ltsuc  33275  dpval3rp  33289  dplti  33294  dpgti  33295  dpexpp1  33297  dpadd2  33299  pnfinf  33567  sqsscirc1  34362  dya2icoseg2  34733  probfinmeasb  34883  probfinmeasbALTV  34884  signshf  35040  divsqrtid  35046  logdivsqrle  35102  hgt750lem2  35104  subfacval3  35718  opnrebl  36888  opnrebl2  36889  taupilem1  38022  opnmbllem0  38364  itg2addnclem  38379  itg2addnclem2  38380  itg2addnclem3  38381  itg2addnc  38382  itg2gt0cn  38383  ftc1anclem5  38405  ftc1anclem7  38407  ftc1anc  38409  areacirclem1  38416  areacirclem4  38419  areacirc  38421  geomcau  38468  isbnd2  38492  ssbnd  38497  heiborlem7  38526  heiborlem8  38527  bfplem2  38532  rrncmslem  38541  rrnequiv  38544  dvrelog3  42890  aks4d1p1p6  42898  rpabsid  43140  irrapxlem1  43607  irrapxlem2  43608  irrapxlem3  43609  irrapxlem5  43611  2timesgt  46065  supxrge  46112  suplesup  46113  xrlexaddrp  46126  xralrple2  46128  infleinflem1  46143  xralrple4  46146  xralrple3  46147  xrralrecnnle  46156  climinf  46380  mullimc  46390  mullimcf  46397  limcrecl  46403  limcleqr  46416  addlimc  46420  0ellimcdiv  46421  limclner  46423  liminflimsupclim  46579  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  stoweidlem7  46779  fourierdlem73  46951  fourierdlem87  46965  fourierdlem103  46981  fourierdlem104  46982  sge0iunmptlemre  47187  smflimlem4  47546  fldivexpfllog2  49402  blenre  49411  itscnhlc0yqe  49596  itscnhlc0xyqsol  49602  itschlc0xyqsol  49604  itsclc0xyqsolr  49606  itsclinecirc0in  49612  itsclquadb  49613  itscnhlinecirc02plem3  49621  itscnhlinecirc02p  49622  inlinecirc02plem  49623  inlinecirc02p  49624  amgmwlem  50707