Theorem rpre 12914

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℝ⁺crp 12905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918  df-rp 12906

This theorem is referenced by:  rpxr  12915  rpcn  12916  rpge0  12919  rprege0  12921  rprene0  12923  neglt  12925  rpaddcl  12929  rpmulcl  12930  rpdivcl  12932  rpgecl  12935  ledivge1le  12978  addlelt  13021  xralrple  13120  xlemul1  13205  infmrp1  13260  iccdil  13406  ltdifltdiv  13754  modcl  13793  mod0  13796  mulmod0  13797  modge0  13799  modlt  13800  modid0  13817  modabs  13824  modabs2  13825  modcyc  13826  muladdmod  13835  modmuladd  13836  modmuladdnn0  13838  modltm1p1mod  13846  2txmodxeq0  13854  2submod  13855  moddi  13862  modsubdir  13863  modeqmodmin  13864  modirr  13865  rpexpmord  14091  expnlbnd  14156  rennim  15162  cnpart  15163  01sqrexlem1  15165  01sqrexlem2  15166  01sqrexlem4  15168  01sqrexlem5  15169  01sqrexlem6  15170  01sqrexlem7  15171  resqrex  15173  rpsqrtcl  15187  sqreulem  15283  eqsqrt2d  15292  2clim  15495  reccn2  15520  cn1lem  15521  climsqz  15564  climsqz2  15565  rlimsqzlem  15572  climsup  15593  climcau  15594  caucvgrlem2  15598  iseralt  15608  cvgcmp  15739  cvgcmpce  15741  divrcnv  15775  rprisefaccl  15946  efgt1  16041  ef01bndlem  16109  sinltx  16114  stdbdmet  24460  stdbdmopn  24462  met2ndci  24466  cfilucfil  24503  ngptgp  24580  reperflem  24763  iccntr  24766  reconnlem2  24772  opnreen  24776  metdseq0  24799  xlebnum  24920  cphsqrtcl3  25143  iscmet3lem3  25246  iscmet3lem1  25247  iscmet3lem2  25248  caubl  25264  lmcau  25269  bcthlem4  25283  minveclem3b  25384  minveclem3  25385  ivthlem2  25409  ivthlem3  25410  nulmbl2  25493  opnmbllem  25558  itg2const2  25698  itg2mulclem  25703  dveflem  25939  lhop  25977  dvcnvre  25980  aalioulem2  26297  aaliou  26302  aaliou3lem4  26310  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  itgulm  26373  reeff1o  26413  pilem2  26418  logleb  26568  logcj  26571  argimgt0  26577  logdmnrp  26606  logcnlem3  26609  logcnlem4  26610  advlog  26619  efopnlem1  26621  cxple2  26662  cxplt2  26663  cxple3  26666  2irrexpq  26696  cxpcn3  26714  resqrtcn  26715  relogbf  26757  asinneg  26852  atanbndlem  26891  cxplim  26938  cxp2limlem  26942  cxp2lim  26943  cxploglim  26944  cxploglim2  26945  logdiflbnd  26961  harmoniclbnd  26975  harmonicbnd4  26977  chtrpcl  27141  ppiltx  27143  chtleppi  27177  logfacubnd  27188  logfaclbnd  27189  logfacbnd3  27190  logexprlim  27192  bposlem7  27257  bposlem8  27258  bposlem9  27259  chebbnd1  27439  chtppilim  27442  chto1ub  27443  chpo1ub  27447  vmadivsum  27449  rpvmasumlem  27454  dchrisumlem3  27458  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0  27487  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem2  27502  log2sumbnd  27511  selberglem2  27513  selberglem3  27514  selberg  27515  selberg2lem  27517  selberg2  27518  pntrf  27530  pntrmax  27531  pntrsumo1  27532  selbergr  27535  selbergs  27541  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntibndlem1  27556  pntlem3  27576  pntlemp  27577  pntleml  27578  pnt2  27580  padicabvcxp  27599  vacn  30769  nmcvcn  30770  smcnlem  30772  blocnilem  30879  chscllem2  31713  nmcexi  32101  nmcopexi  32102  nmcfnexi  32126  dp2ltsuc  32967  dpval3rp  32981  dplti  32986  dpgti  32987  dpexpp1  32989  dpadd2  32991  pnfinf  33265  sqsscirc1  34065  dya2icoseg2  34435  probfinmeasb  34585  probfinmeasbALTV  34586  signshf  34745  divsqrtid  34751  logdivsqrle  34807  hgt750lem2  34809  subfacval3  35383  opnrebl  36514  opnrebl2  36515  taupilem1  37526  opnmbllem0  37857  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anc  37902  areacirclem1  37909  areacirclem4  37912  areacirc  37914  geomcau  37960  isbnd2  37984  ssbnd  37989  heiborlem7  38018  heiborlem8  38019  bfplem2  38024  rrncmslem  38033  rrnequiv  38036  dvrelog3  42319  aks4d1p1p6  42327  rpabsid  42576  irrapxlem1  43064  irrapxlem2  43065  irrapxlem3  43066  irrapxlem5  43068  2timesgt  45536  supxrge  45583  suplesup  45584  xrlexaddrp  45597  xralrple2  45599  infleinflem1  45614  xralrple4  45617  xralrple3  45618  xrralrecnnle  45627  climinf  45852  mullimc  45862  mullimcf  45869  limcrecl  45875  limcleqr  45888  addlimc  45892  0ellimcdiv  45893  limclner  45895  liminflimsupclim  46051  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  stoweidlem7  46251  fourierdlem73  46423  fourierdlem87  46437  fourierdlem103  46453  fourierdlem104  46454  sge0iunmptlemre  46659  smflimlem4  47018  fldivexpfllog2  48811  blenre  48820  itscnhlc0yqe  49005  itscnhlc0xyqsol  49011  itschlc0xyqsol  49013  itsclc0xyqsolr  49015  itsclinecirc0in  49021  itsclquadb  49022  itscnhlinecirc02plem3  49030  itscnhlinecirc02p  49031  inlinecirc02plem  49032  inlinecirc02p  49033  amgmwlem  50047