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  24380  stdbdmopn  24382  met2ndci  24386  cfilucfil  24423  ngptgp  24500  reperflem  24683  iccntr  24686  reconnlem2  24692  opnreen  24696  metdseq0  24719  xlebnum  24840  cphsqrtcl3  25063  iscmet3lem3  25166  iscmet3lem1  25167  iscmet3lem2  25168  caubl  25184  lmcau  25189  bcthlem4  25203  minveclem3b  25304  minveclem3  25305  ivthlem2  25329  ivthlem3  25330  nulmbl2  25413  opnmbllem  25478  itg2const2  25618  itg2mulclem  25623  dveflem  25859  lhop  25897  dvcnvre  25900  aalioulem2  26217  aaliou  26222  aaliou3lem4  26230  ulmcaulem  26279  ulmcau  26280  ulmcn  26284  itgulm  26293  reeff1o  26333  pilem2  26338  logleb  26488  logcj  26491  argimgt0  26497  logdmnrp  26526  logcnlem3  26529  logcnlem4  26530  advlog  26539  efopnlem1  26541  cxple2  26582  cxplt2  26583  cxple3  26586  2irrexpq  26616  cxpcn3  26634  resqrtcn  26635  relogbf  26677  asinneg  26772  atanbndlem  26811  cxplim  26858  cxp2limlem  26862  cxp2lim  26863  cxploglim  26864  cxploglim2  26865  logdiflbnd  26881  harmoniclbnd  26895  harmonicbnd4  26897  chtrpcl  27061  ppiltx  27063  chtleppi  27097  logfacubnd  27108  logfaclbnd  27109  logfacbnd3  27110  logexprlim  27112  bposlem7  27177  bposlem8  27178  bposlem9  27179  chebbnd1  27359  chtppilim  27362  chto1ub  27363  chpo1ub  27367  vmadivsum  27369  rpvmasumlem  27374  dchrisumlem3  27378  dchrvmasumlem2  27385  dchrvmasumiflem1  27388  dchrisum0  27407  mudivsum  27417  mulogsumlem  27418  mulogsum  27419  mulog2sumlem2  27422  log2sumbnd  27431  selberglem2  27433  selberglem3  27434  selberg  27435  selberg2lem  27437  selberg2  27438  pntrf  27450  pntrmax  27451  pntrsumo1  27452  selbergr  27455  selbergs  27461  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntibndlem1  27476  pntlem3  27496  pntlemp  27497  pntleml  27498  pnt2  27500  padicabvcxp  27519  vacn  30596  nmcvcn  30597  smcnlem  30599  blocnilem  30706  chscllem2  31540  nmcexi  31928  nmcopexi  31929  nmcfnexi  31953  dp2ltsuc  32779  dpval3rp  32793  dplti  32798  dpgti  32799  dpexpp1  32801  dpadd2  32803  pnfinf  33110  sqsscirc1  33871  dya2icoseg2  34242  probfinmeasb  34392  probfinmeasbALTV  34393  signshf  34552  divsqrtid  34558  logdivsqrle  34614  hgt750lem2  34616  subfacval3  35149  opnrebl  36281  opnrebl2  36282  taupilem1  37282  opnmbllem0  37623  itg2addnclem  37638  itg2addnclem2  37639  itg2addnclem3  37640  itg2addnc  37641  itg2gt0cn  37642  ftc1anclem5  37664  ftc1anclem7  37666  ftc1anc  37668  areacirclem1  37675  areacirclem4  37678  areacirc  37680  geomcau  37726  isbnd2  37750  ssbnd  37755  heiborlem7  37784  heiborlem8  37785  bfplem2  37790  rrncmslem  37799  rrnequiv  37802  dvrelog3  42026  aks4d1p1p6  42034  rpabsid  42282  irrapxlem1  42783  irrapxlem2  42784  irrapxlem3  42785  irrapxlem5  42787  2timesgt  45259  supxrge  45307  suplesup  45308  xrlexaddrp  45321  xralrple2  45323  infleinflem1  45339  xralrple4  45342  xralrple3  45343  xrralrecnnle  45352  climinf  45577  mullimc  45587  mullimcf  45594  limcrecl  45600  limcleqr  45615  addlimc  45619  0ellimcdiv  45620  limclner  45622  liminflimsupclim  45778  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem7  45978  fourierdlem73  46150  fourierdlem87  46164  fourierdlem103  46180  fourierdlem104  46181  sge0iunmptlemre  46386  smflimlem4  46745  fldivexpfllog2  48527  blenre  48536  itscnhlc0yqe  48721  itscnhlc0xyqsol  48727  itschlc0xyqsol  48729  itsclc0xyqsolr  48731  itsclinecirc0in  48737  itsclquadb  48738  itscnhlinecirc02plem3  48746  itscnhlinecirc02p  48747  inlinecirc02plem  48748  inlinecirc02p  48749  amgmwlem  49764