Theorem rpre 12926

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-rp 12918

This theorem is referenced by:  rpxr  12927  rpcn  12928  rpge0  12931  rprege0  12933  rprene0  12935  neglt  12937  rpaddcl  12941  rpmulcl  12942  rpdivcl  12944  rpgecl  12947  ledivge1le  12990  addlelt  13033  xralrple  13132  xlemul1  13217  infmrp1  13272  iccdil  13418  ltdifltdiv  13766  modcl  13805  mod0  13808  mulmod0  13809  modge0  13811  modlt  13812  modid0  13829  modabs  13836  modabs2  13837  modcyc  13838  muladdmod  13847  modmuladd  13848  modmuladdnn0  13850  modltm1p1mod  13858  2txmodxeq0  13866  2submod  13867  moddi  13874  modsubdir  13875  modeqmodmin  13876  modirr  13877  rpexpmord  14103  expnlbnd  14168  rennim  15174  cnpart  15175  01sqrexlem1  15177  01sqrexlem2  15178  01sqrexlem4  15180  01sqrexlem5  15181  01sqrexlem6  15182  01sqrexlem7  15183  resqrex  15185  rpsqrtcl  15199  sqreulem  15295  eqsqrt2d  15304  2clim  15507  reccn2  15532  cn1lem  15533  climsqz  15576  climsqz2  15577  rlimsqzlem  15584  climsup  15605  climcau  15606  caucvgrlem2  15610  iseralt  15620  cvgcmp  15751  cvgcmpce  15753  divrcnv  15787  rprisefaccl  15958  efgt1  16053  ef01bndlem  16121  sinltx  16126  stdbdmet  24472  stdbdmopn  24474  met2ndci  24478  cfilucfil  24515  ngptgp  24592  reperflem  24775  iccntr  24778  reconnlem2  24784  opnreen  24788  metdseq0  24811  xlebnum  24932  cphsqrtcl3  25155  iscmet3lem3  25258  iscmet3lem1  25259  iscmet3lem2  25260  caubl  25276  lmcau  25281  bcthlem4  25295  minveclem3b  25396  minveclem3  25397  ivthlem2  25421  ivthlem3  25422  nulmbl2  25505  opnmbllem  25570  itg2const2  25710  itg2mulclem  25715  dveflem  25951  lhop  25989  dvcnvre  25992  aalioulem2  26309  aaliou  26314  aaliou3lem4  26322  ulmcaulem  26371  ulmcau  26372  ulmcn  26376  itgulm  26385  reeff1o  26425  pilem2  26430  logleb  26580  logcj  26583  argimgt0  26589  logdmnrp  26618  logcnlem3  26621  logcnlem4  26622  advlog  26631  efopnlem1  26633  cxple2  26674  cxplt2  26675  cxple3  26678  2irrexpq  26708  cxpcn3  26726  resqrtcn  26727  relogbf  26769  asinneg  26864  atanbndlem  26903  cxplim  26950  cxp2limlem  26954  cxp2lim  26955  cxploglim  26956  cxploglim2  26957  logdiflbnd  26973  harmoniclbnd  26987  harmonicbnd4  26989  chtrpcl  27153  ppiltx  27155  chtleppi  27189  logfacubnd  27200  logfaclbnd  27201  logfacbnd3  27202  logexprlim  27204  bposlem7  27269  bposlem8  27270  bposlem9  27271  chebbnd1  27451  chtppilim  27454  chto1ub  27455  chpo1ub  27459  vmadivsum  27461  rpvmasumlem  27466  dchrisumlem3  27470  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0  27499  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem2  27514  log2sumbnd  27523  selberglem2  27525  selberglem3  27526  selberg  27527  selberg2lem  27529  selberg2  27530  pntrf  27542  pntrmax  27543  pntrsumo1  27544  selbergr  27547  selbergs  27553  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntibndlem1  27568  pntlem3  27588  pntlemp  27589  pntleml  27590  pnt2  27592  padicabvcxp  27611  vacn  30782  nmcvcn  30783  smcnlem  30785  blocnilem  30892  chscllem2  31726  nmcexi  32114  nmcopexi  32115  nmcfnexi  32139  dp2ltsuc  32978  dpval3rp  32992  dplti  32997  dpgti  32998  dpexpp1  33000  dpadd2  33002  pnfinf  33277  sqsscirc1  34086  dya2icoseg2  34456  probfinmeasb  34606  probfinmeasbALTV  34607  signshf  34766  divsqrtid  34772  logdivsqrle  34828  hgt750lem2  34830  subfacval3  35405  opnrebl  36536  opnrebl2  36537  taupilem1  37576  opnmbllem0  37907  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  itg2addnc  37925  itg2gt0cn  37926  ftc1anclem5  37948  ftc1anclem7  37950  ftc1anc  37952  areacirclem1  37959  areacirclem4  37962  areacirc  37964  geomcau  38010  isbnd2  38034  ssbnd  38039  heiborlem7  38068  heiborlem8  38069  bfplem2  38074  rrncmslem  38083  rrnequiv  38086  dvrelog3  42435  aks4d1p1p6  42443  rpabsid  42691  irrapxlem1  43179  irrapxlem2  43180  irrapxlem3  43181  irrapxlem5  43183  2timesgt  45650  supxrge  45697  suplesup  45698  xrlexaddrp  45711  xralrple2  45713  infleinflem1  45728  xralrple4  45731  xralrple3  45732  xrralrecnnle  45741  climinf  45966  mullimc  45976  mullimcf  45983  limcrecl  45989  limcleqr  46002  addlimc  46006  0ellimcdiv  46007  limclner  46009  liminflimsupclim  46165  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  stoweidlem7  46365  fourierdlem73  46537  fourierdlem87  46551  fourierdlem103  46567  fourierdlem104  46568  sge0iunmptlemre  46773  smflimlem4  47132  fldivexpfllog2  48925  blenre  48934  itscnhlc0yqe  49119  itscnhlc0xyqsol  49125  itschlc0xyqsol  49127  itsclc0xyqsolr  49129  itsclinecirc0in  49135  itsclquadb  49136  itscnhlinecirc02plem3  49144  itscnhlinecirc02p  49145  inlinecirc02plem  49146  inlinecirc02p  49147  amgmwlem  50161