Theorem rpre 13024

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℝcr 11098  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-ss 3930  df-rp 13016

This theorem is referenced by:  rpxr  13025  rpcn  13026  rpge0  13029  rprege0  13031  rprene0  13033  neglt  13035  rpaddcl  13039  rpmulcl  13040  rpdivcl  13042  rpgecl  13045  ledivge1le  13088  addlelt  13131  xralrple  13230  xlemul1  13315  infmrp1  13370  iccdil  13516  ltdifltdiv  13866  modcl  13905  mod0  13908  mulmod0  13909  modge0  13911  modlt  13912  modid0  13929  modabs  13936  modabs2  13937  modcyc  13938  muladdmod  13947  modmuladd  13948  modmuladdnn0  13950  modltm1p1mod  13958  2txmodxeq0  13966  2submod  13967  moddi  13974  modsubdir  13975  modeqmodmin  13976  modirr  13977  rpexpmord  14203  expnlbnd  14268  rennim  15289  cnpart  15290  01sqrexlem1  15292  01sqrexlem2  15293  01sqrexlem4  15295  01sqrexlem5  15296  01sqrexlem6  15297  01sqrexlem7  15298  resqrex  15300  rpsqrtcl  15314  sqreulem  15410  eqsqrt2d  15419  2clim  15622  reccn2  15647  cn1lem  15648  climsqz  15691  climsqz2  15692  rlimsqzlem  15699  climsup  15720  climcau  15721  caucvgrlem2  15725  iseralt  15735  cvgcmp  15867  cvgcmpce  15869  divrcnv  15905  rprisefaccl  16076  efgt1  16171  ef01bndlem  16239  sinltx  16244  stdbdmet  24641  stdbdmopn  24643  met2ndci  24647  cfilucfil  24684  ngptgp  24761  reperflem  24944  iccntr  24947  reconnlem2  24953  opnreen  24957  metdseq0  24980  xlebnum  25092  cphsqrtcl3  25314  iscmet3lem3  25417  iscmet3lem1  25418  iscmet3lem2  25419  caubl  25435  lmcau  25440  bcthlem4  25454  minveclem3b  25555  minveclem3  25556  ivthlem2  25579  ivthlem3  25580  nulmbl2  25663  opnmbllem  25728  itg2const2  25868  itg2mulclem  25873  dveflem  26106  lhop  26143  dvcnvre  26146  aalioulem2  26462  aaliou  26467  aaliou3lem4  26475  ulmcaulem  26522  ulmcau  26523  ulmcn  26527  itgulm  26536  reeff1o  26575  pilem2  26580  logleb  26733  logcj  26736  argimgt0  26742  logdmnrp  26771  logcnlem3  26774  logcnlem4  26775  advlog  26784  efopnlem1  26786  cxple2  26827  cxplt2  26828  cxple3  26831  2irrexpq  26861  cxpcn3  26878  resqrtcn  26879  relogbf  26921  asinneg  27016  atanbndlem  27055  cxplim  27101  cxp2limlem  27105  cxp2lim  27106  cxploglim  27107  cxploglim2  27108  logdiflbnd  27124  harmoniclbnd  27138  harmonicbnd4  27140  chtrpcl  27304  ppiltx  27306  chtleppi  27339  logfacubnd  27350  logfaclbnd  27351  logfacbnd3  27352  logexprlim  27354  bposlem7  27419  bposlem8  27420  bposlem9  27421  chebbnd1  27601  chtppilim  27604  chto1ub  27605  chpo1ub  27609  vmadivsum  27611  rpvmasumlem  27616  dchrisumlem3  27620  dchrvmasumlem2  27627  dchrvmasumiflem1  27630  dchrisum0  27649  mudivsum  27659  mulogsumlem  27660  mulogsum  27661  mulog2sumlem2  27664  log2sumbnd  27673  selberglem2  27675  selberglem3  27676  selberg  27677  selberg2lem  27679  selberg2  27680  pntrf  27692  pntrmax  27693  pntrsumo1  27694  selbergr  27697  selbergs  27703  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntibndlem1  27718  pntlem3  27738  pntlemp  27739  pntleml  27740  pnt2  27742  padicabvcxp  27761  vacn  30986  nmcvcn  30987  smcnlem  30989  blocnilem  31096  chscllem2  31930  nmcexi  32318  nmcopexi  32319  nmcfnexi  32343  dp2ltsuc  33145  dpval3rp  33159  dplti  33164  dpgti  33165  dpexpp1  33167  dpadd2  33169  pnfinf  33443  sqsscirc1  34242  dya2icoseg2  34612  probfinmeasb  34762  probfinmeasbALTV  34763  signshf  34919  divsqrtid  34925  logdivsqrle  34981  hgt750lem2  34983  subfacval3  35579  opnrebl  36719  opnrebl2  36720  taupilem1  37852  opnmbllem0  38194  itg2addnclem  38209  itg2addnclem2  38210  itg2addnclem3  38211  itg2addnc  38212  itg2gt0cn  38213  ftc1anclem5  38235  ftc1anclem7  38237  ftc1anc  38239  areacirclem1  38246  areacirclem4  38249  areacirc  38251  geomcau  38297  isbnd2  38321  ssbnd  38326  heiborlem7  38355  heiborlem8  38356  bfplem2  38361  rrncmslem  38370  rrnequiv  38373  dvrelog3  42721  aks4d1p1p6  42729  rpabsid  42971  irrapxlem1  43440  irrapxlem2  43441  irrapxlem3  43442  irrapxlem5  43444  2timesgt  45898  supxrge  45945  suplesup  45946  xrlexaddrp  45959  xralrple2  45961  infleinflem1  45976  xralrple4  45979  xralrple3  45980  xrralrecnnle  45989  climinf  46213  mullimc  46223  mullimcf  46230  limcrecl  46236  limcleqr  46249  addlimc  46253  0ellimcdiv  46254  limclner  46256  liminflimsupclim  46412  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  stoweidlem7  46612  fourierdlem73  46784  fourierdlem87  46798  fourierdlem103  46814  fourierdlem104  46815  sge0iunmptlemre  47020  smflimlem4  47379  fldivexpfllog2  49229  blenre  49238  itscnhlc0yqe  49423  itscnhlc0xyqsol  49429  itschlc0xyqsol  49431  itsclc0xyqsolr  49433  itsclinecirc0in  49439  itsclquadb  49440  itscnhlinecirc02plem3  49448  itscnhlinecirc02p  49449  inlinecirc02plem  49450  inlinecirc02p  49451  amgmwlem  50475