Theorem rpre 12979

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11106  ℝ⁺crp 12971

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3955  df-ss 3965  df-rp 12972

This theorem is referenced by:  rpxr  12980  rpcn  12981  rpge0  12984  rprege0  12986  rprene0  12988  rpaddcl  12993  rpmulcl  12994  rpdivcl  12996  rpgecl  12999  ledivge1le  13042  addlelt  13085  xralrple  13181  xlemul1  13266  infmrp1  13320  iccdil  13464  ltdifltdiv  13796  modcl  13835  mod0  13838  mulmod0  13839  modge0  13841  modlt  13842  modid0  13859  modabs  13866  modabs2  13867  modcyc  13868  modmuladd  13875  modmuladdnn0  13877  modltm1p1mod  13885  2txmodxeq0  13893  2submod  13894  moddi  13901  modsubdir  13902  modeqmodmin  13903  modirr  13904  rpexpmord  14130  expnlbnd  14193  rennim  15183  cnpart  15184  01sqrexlem1  15186  01sqrexlem2  15187  01sqrexlem4  15189  01sqrexlem5  15190  01sqrexlem6  15191  01sqrexlem7  15192  resqrex  15194  rpsqrtcl  15208  sqreulem  15303  eqsqrt2d  15312  2clim  15513  reccn2  15538  cn1lem  15539  climsqz  15582  climsqz2  15583  rlimsqzlem  15592  climsup  15613  climcau  15614  caucvgrlem2  15618  iseralt  15628  cvgcmp  15759  cvgcmpce  15761  divrcnv  15795  rprisefaccl  15964  efgt1  16056  ef01bndlem  16124  sinltx  16129  stdbdmet  24017  stdbdmopn  24019  met2ndci  24023  cfilucfil  24060  ngptgp  24137  reperflem  24326  iccntr  24329  reconnlem2  24335  opnreen  24339  metdseq0  24362  xlebnum  24473  cphsqrtcl3  24696  iscmet3lem3  24799  iscmet3lem1  24800  iscmet3lem2  24801  caubl  24817  lmcau  24822  bcthlem4  24836  minveclem3b  24937  minveclem3  24938  ivthlem2  24961  ivthlem3  24962  nulmbl2  25045  opnmbllem  25110  itg2const2  25251  itg2mulclem  25256  dveflem  25488  lhop  25525  dvcnvre  25528  aalioulem2  25838  aaliou  25843  aaliou3lem4  25851  ulmcaulem  25898  ulmcau  25899  ulmcn  25903  itgulm  25912  reeff1o  25951  pilem2  25956  logleb  26103  logcj  26106  argimgt0  26112  logdmnrp  26141  logcnlem3  26144  logcnlem4  26145  advlog  26154  efopnlem1  26156  cxple2  26197  cxplt2  26198  cxple3  26201  2irrexpq  26230  cxpcn3  26246  resqrtcn  26247  relogbf  26286  asinneg  26381  atanbndlem  26420  cxplim  26466  cxp2limlem  26470  cxp2lim  26471  cxploglim  26472  cxploglim2  26473  logdiflbnd  26489  harmoniclbnd  26503  harmonicbnd4  26505  chtrpcl  26669  ppiltx  26671  chtleppi  26703  logfacubnd  26714  logfaclbnd  26715  logfacbnd3  26716  logexprlim  26718  bposlem7  26783  bposlem8  26784  bposlem9  26785  chebbnd1  26965  chtppilim  26968  chto1ub  26969  chpo1ub  26973  vmadivsum  26975  rpvmasumlem  26980  dchrisumlem3  26984  dchrvmasumlem2  26991  dchrvmasumiflem1  26994  dchrisum0  27013  mudivsum  27023  mulogsumlem  27024  mulogsum  27025  mulog2sumlem2  27028  log2sumbnd  27037  selberglem2  27039  selberglem3  27040  selberg  27041  selberg2lem  27043  selberg2  27044  pntrf  27056  pntrmax  27057  pntrsumo1  27058  selbergr  27061  selbergs  27067  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntibndlem1  27082  pntlem3  27102  pntlemp  27103  pntleml  27104  pnt2  27106  padicabvcxp  27125  vacn  29935  nmcvcn  29936  smcnlem  29938  blocnilem  30045  chscllem2  30879  nmcexi  31267  nmcopexi  31268  nmcfnexi  31292  dp2ltsuc  32040  dpval3rp  32054  dplti  32059  dpgti  32060  dpexpp1  32062  dpadd2  32064  pnfinf  32317  sqsscirc1  32877  dya2icoseg2  33266  probfinmeasb  33416  probfinmeasbALTV  33417  signshf  33588  divsqrtid  33595  logdivsqrle  33651  hgt750lem2  33653  subfacval3  34169  opnrebl  35194  opnrebl2  35195  taupilem1  36191  opnmbllem0  36513  itg2addnclem  36528  itg2addnclem2  36529  itg2addnclem3  36530  itg2addnc  36531  itg2gt0cn  36532  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anc  36558  areacirclem1  36565  areacirclem4  36568  areacirc  36570  geomcau  36616  isbnd2  36640  ssbnd  36645  heiborlem7  36674  heiborlem8  36675  bfplem2  36680  rrncmslem  36689  rrnequiv  36692  dvrelog3  40919  aks4d1p1p6  40927  irrapxlem1  41546  irrapxlem2  41547  irrapxlem3  41548  irrapxlem5  41550  neglt  43981  2timesgt  43985  supxrge  44035  suplesup  44036  xrlexaddrp  44049  xralrple2  44051  infleinflem1  44067  xralrple4  44070  xralrple3  44071  xrralrecnnle  44080  climinf  44309  mullimc  44319  mullimcf  44326  limcrecl  44332  limcleqr  44347  addlimc  44351  0ellimcdiv  44352  limclner  44354  liminflimsupclim  44510  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  stoweidlem7  44710  fourierdlem73  44882  fourierdlem87  44896  fourierdlem103  44912  fourierdlem104  44913  sge0iunmptlemre  45118  smflimlem4  45477  fldivexpfllog2  47205  blenre  47214  itscnhlc0yqe  47399  itscnhlc0xyqsol  47405  itschlc0xyqsol  47407  itsclc0xyqsolr  47409  itsclinecirc0in  47415  itsclquadb  47416  itscnhlinecirc02plem3  47424  itscnhlinecirc02p  47425  inlinecirc02plem  47426  inlinecirc02p  47427  amgmwlem  47803