Theorem rpre 13020

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11094  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3922  df-rp 13012

This theorem is referenced by:  rpxr  13021  rpcn  13022  rpge0  13025  rprege0  13027  rprene0  13029  neglt  13031  rpaddcl  13035  rpmulcl  13036  rpdivcl  13038  rpgecl  13041  ledivge1le  13084  addlelt  13127  xralrple  13226  xlemul1  13311  infmrp1  13366  iccdil  13512  ltdifltdiv  13863  modcl  13902  mod0  13905  mulmod0  13906  modge0  13908  modlt  13909  modid0  13926  modabs  13933  modabs2  13934  modcyc  13935  muladdmod  13944  modmuladd  13945  modmuladdnn0  13947  modltm1p1mod  13955  2txmodxeq0  13963  2submod  13964  moddi  13971  modsubdir  13972  modeqmodmin  13973  modirr  13974  rpexpmord  14200  expnlbnd  14265  rennim  15286  cnpart  15287  01sqrexlem1  15289  01sqrexlem2  15290  01sqrexlem4  15292  01sqrexlem5  15293  01sqrexlem6  15294  01sqrexlem7  15295  resqrex  15297  rpsqrtcl  15311  sqreulem  15407  eqsqrt2d  15416  2clim  15619  reccn2  15644  cn1lem  15645  climsqz  15688  climsqz2  15689  rlimsqzlem  15696  climsup  15717  climcau  15718  caucvgrlem2  15722  iseralt  15732  cvgcmp  15864  cvgcmpce  15866  divrcnv  15902  rprisefaccl  16073  efgt1  16167  ef01bndlem  16235  sinltx  16240  stdbdmet  24673  stdbdmopn  24675  met2ndci  24679  cfilucfil  24716  ngptgp  24793  reperflem  24976  iccntr  24979  reconnlem2  24985  opnreen  24989  metdseq0  25012  xlebnum  25124  cphsqrtcl3  25346  iscmet3lem3  25449  iscmet3lem1  25450  iscmet3lem2  25451  caubl  25467  lmcau  25472  bcthlem4  25486  minveclem3b  25587  minveclem3  25588  ivthlem2  25611  ivthlem3  25612  nulmbl2  25695  opnmbllem  25760  itg2const2  25900  itg2mulclem  25905  dveflem  26138  lhop  26175  dvcnvre  26178  aalioulem2  26496  aaliou  26501  aaliou3lem4  26509  ulmcaulem  26557  ulmcau  26558  ulmcn  26562  itgulm  26571  reeff1o  26610  pilem2  26615  logleb  26768  logcj  26771  argimgt0  26777  logdmnrp  26806  logcnlem3  26809  logcnlem4  26810  advlog  26819  efopnlem1  26821  cxple2  26862  cxplt2  26863  cxple3  26866  2irrexpq  26896  cxpcn3  26913  resqrtcn  26914  relogbf  26956  asinneg  27051  atanbndlem  27090  cxplim  27136  cxp2limlem  27140  cxp2lim  27141  cxploglim  27142  cxploglim2  27143  logdiflbnd  27159  harmoniclbnd  27173  harmonicbnd4  27175  chtrpcl  27339  ppiltx  27341  chtleppi  27374  logfacubnd  27385  logfaclbnd  27386  logfacbnd3  27387  logexprlim  27389  bposlem7  27454  bposlem8  27455  bposlem9  27456  chebbnd1  27636  chtppilim  27639  chto1ub  27640  chpo1ub  27644  vmadivsum  27646  rpvmasumlem  27651  dchrisumlem3  27655  dchrvmasumlem2  27662  dchrvmasumiflem1  27665  dchrisum0  27684  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  mulog2sumlem2  27699  log2sumbnd  27708  selberglem2  27710  selberglem3  27711  selberg  27712  selberg2lem  27714  selberg2  27715  pntrf  27727  pntrmax  27728  pntrsumo1  27729  selbergr  27732  selbergs  27738  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntibndlem1  27753  pntlem3  27773  pntlemp  27774  pntleml  27775  pnt2  27777  padicabvcxp  27796  vacn  31046  nmcvcn  31047  smcnlem  31049  blocnilem  31156  chscllem2  31990  nmcexi  32378  nmcopexi  32379  nmcfnexi  32403  dp2ltsuc  33205  dpval3rp  33219  dplti  33224  dpgti  33225  dpexpp1  33227  dpadd2  33229  pnfinf  33503  sqsscirc1  34298  dya2icoseg2  34668  probfinmeasb  34818  probfinmeasbALTV  34819  signshf  34975  divsqrtid  34981  logdivsqrle  35037  hgt750lem2  35039  subfacval3  35681  opnrebl  36831  opnrebl2  36832  taupilem1  37965  opnmbllem0  38307  itg2addnclem  38322  itg2addnclem2  38323  itg2addnclem3  38324  itg2addnc  38325  itg2gt0cn  38326  ftc1anclem5  38348  ftc1anclem7  38350  ftc1anc  38352  areacirclem1  38359  areacirclem4  38362  areacirc  38364  geomcau  38410  isbnd2  38434  ssbnd  38439  heiborlem7  38468  heiborlem8  38469  bfplem2  38474  rrncmslem  38483  rrnequiv  38486  dvrelog3  42832  aks4d1p1p6  42840  rpabsid  43082  irrapxlem1  43549  irrapxlem2  43550  irrapxlem3  43551  irrapxlem5  43553  2timesgt  46007  supxrge  46054  suplesup  46055  xrlexaddrp  46068  xralrple2  46070  infleinflem1  46085  xralrple4  46088  xralrple3  46089  xrralrecnnle  46098  climinf  46322  mullimc  46332  mullimcf  46339  limcrecl  46345  limcleqr  46358  addlimc  46362  0ellimcdiv  46363  limclner  46365  liminflimsupclim  46521  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  stoweidlem7  46721  fourierdlem73  46893  fourierdlem87  46907  fourierdlem103  46923  fourierdlem104  46924  sge0iunmptlemre  47129  smflimlem4  47488  fldivexpfllog2  49345  blenre  49354  itscnhlc0yqe  49539  itscnhlc0xyqsol  49545  itschlc0xyqsol  49547  itsclc0xyqsolr  49549  itsclinecirc0in  49555  itsclquadb  49556  itscnhlinecirc02plem3  49564  itscnhlinecirc02p  49565  inlinecirc02plem  49566  inlinecirc02p  49567  amgmwlem  50622