Theorem rpre 12936

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11043  ℝ⁺crp 12927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-ss 3928  df-rp 12928

This theorem is referenced by:  rpxr  12937  rpcn  12938  rpge0  12941  rprege0  12943  rprene0  12945  neglt  12947  rpaddcl  12951  rpmulcl  12952  rpdivcl  12954  rpgecl  12957  ledivge1le  13000  addlelt  13043  xralrple  13141  xlemul1  13226  infmrp1  13281  iccdil  13427  ltdifltdiv  13772  modcl  13811  mod0  13814  mulmod0  13815  modge0  13817  modlt  13818  modid0  13835  modabs  13842  modabs2  13843  modcyc  13844  muladdmod  13853  modmuladd  13854  modmuladdnn0  13856  modltm1p1mod  13864  2txmodxeq0  13872  2submod  13873  moddi  13880  modsubdir  13881  modeqmodmin  13882  modirr  13883  rpexpmord  14109  expnlbnd  14174  rennim  15181  cnpart  15182  01sqrexlem1  15184  01sqrexlem2  15185  01sqrexlem4  15187  01sqrexlem5  15188  01sqrexlem6  15189  01sqrexlem7  15190  resqrex  15192  rpsqrtcl  15206  sqreulem  15302  eqsqrt2d  15311  2clim  15514  reccn2  15539  cn1lem  15540  climsqz  15583  climsqz2  15584  rlimsqzlem  15591  climsup  15612  climcau  15613  caucvgrlem2  15617  iseralt  15627  cvgcmp  15758  cvgcmpce  15760  divrcnv  15794  rprisefaccl  15965  efgt1  16060  ef01bndlem  16128  sinltx  16133  stdbdmet  24437  stdbdmopn  24439  met2ndci  24443  cfilucfil  24480  ngptgp  24557  reperflem  24740  iccntr  24743  reconnlem2  24749  opnreen  24753  metdseq0  24776  xlebnum  24897  cphsqrtcl3  25120  iscmet3lem3  25223  iscmet3lem1  25224  iscmet3lem2  25225  caubl  25241  lmcau  25246  bcthlem4  25260  minveclem3b  25361  minveclem3  25362  ivthlem2  25386  ivthlem3  25387  nulmbl2  25470  opnmbllem  25535  itg2const2  25675  itg2mulclem  25680  dveflem  25916  lhop  25954  dvcnvre  25957  aalioulem2  26274  aaliou  26279  aaliou3lem4  26287  ulmcaulem  26336  ulmcau  26337  ulmcn  26341  itgulm  26350  reeff1o  26390  pilem2  26395  logleb  26545  logcj  26548  argimgt0  26554  logdmnrp  26583  logcnlem3  26586  logcnlem4  26587  advlog  26596  efopnlem1  26598  cxple2  26639  cxplt2  26640  cxple3  26643  2irrexpq  26673  cxpcn3  26691  resqrtcn  26692  relogbf  26734  asinneg  26829  atanbndlem  26868  cxplim  26915  cxp2limlem  26919  cxp2lim  26920  cxploglim  26921  cxploglim2  26922  logdiflbnd  26938  harmoniclbnd  26952  harmonicbnd4  26954  chtrpcl  27118  ppiltx  27120  chtleppi  27154  logfacubnd  27165  logfaclbnd  27166  logfacbnd3  27167  logexprlim  27169  bposlem7  27234  bposlem8  27235  bposlem9  27236  chebbnd1  27416  chtppilim  27419  chto1ub  27420  chpo1ub  27424  vmadivsum  27426  rpvmasumlem  27431  dchrisumlem3  27435  dchrvmasumlem2  27442  dchrvmasumiflem1  27445  dchrisum0  27464  mudivsum  27474  mulogsumlem  27475  mulogsum  27476  mulog2sumlem2  27479  log2sumbnd  27488  selberglem2  27490  selberglem3  27491  selberg  27492  selberg2lem  27494  selberg2  27495  pntrf  27507  pntrmax  27508  pntrsumo1  27509  selbergr  27512  selbergs  27518  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntibndlem1  27533  pntlem3  27553  pntlemp  27554  pntleml  27555  pnt2  27557  padicabvcxp  27576  vacn  30673  nmcvcn  30674  smcnlem  30676  blocnilem  30783  chscllem2  31617  nmcexi  32005  nmcopexi  32006  nmcfnexi  32030  dp2ltsuc  32856  dpval3rp  32870  dplti  32875  dpgti  32876  dpexpp1  32878  dpadd2  32880  pnfinf  33152  sqsscirc1  33891  dya2icoseg2  34262  probfinmeasb  34412  probfinmeasbALTV  34413  signshf  34572  divsqrtid  34578  logdivsqrle  34634  hgt750lem2  34636  subfacval3  35169  opnrebl  36301  opnrebl2  36302  taupilem1  37302  opnmbllem0  37643  itg2addnclem  37658  itg2addnclem2  37659  itg2addnclem3  37660  itg2addnc  37661  itg2gt0cn  37662  ftc1anclem5  37684  ftc1anclem7  37686  ftc1anc  37688  areacirclem1  37695  areacirclem4  37698  areacirc  37700  geomcau  37746  isbnd2  37770  ssbnd  37775  heiborlem7  37804  heiborlem8  37805  bfplem2  37810  rrncmslem  37819  rrnequiv  37822  dvrelog3  42046  aks4d1p1p6  42054  rpabsid  42302  irrapxlem1  42803  irrapxlem2  42804  irrapxlem3  42805  irrapxlem5  42807  2timesgt  45279  supxrge  45327  suplesup  45328  xrlexaddrp  45341  xralrple2  45343  infleinflem1  45359  xralrple4  45362  xralrple3  45363  xrralrecnnle  45372  climinf  45597  mullimc  45607  mullimcf  45614  limcrecl  45620  limcleqr  45635  addlimc  45639  0ellimcdiv  45640  limclner  45642  liminflimsupclim  45798  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem7  45998  fourierdlem73  46170  fourierdlem87  46184  fourierdlem103  46200  fourierdlem104  46201  sge0iunmptlemre  46406  smflimlem4  46765  fldivexpfllog2  48547  blenre  48556  itscnhlc0yqe  48741  itscnhlc0xyqsol  48747  itschlc0xyqsol  48749  itsclc0xyqsolr  48751  itsclinecirc0in  48757  itsclquadb  48758  itscnhlinecirc02plem3  48766  itscnhlinecirc02p  48767  inlinecirc02plem  48768  inlinecirc02p  48769  amgmwlem  49784