Theorem rpre 12899

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11005  ℝ⁺crp 12890

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-rp 12891

This theorem is referenced by:  rpxr  12900  rpcn  12901  rpge0  12904  rprege0  12906  rprene0  12908  neglt  12910  rpaddcl  12914  rpmulcl  12915  rpdivcl  12917  rpgecl  12920  ledivge1le  12963  addlelt  13006  xralrple  13104  xlemul1  13189  infmrp1  13244  iccdil  13390  ltdifltdiv  13738  modcl  13777  mod0  13780  mulmod0  13781  modge0  13783  modlt  13784  modid0  13801  modabs  13808  modabs2  13809  modcyc  13810  muladdmod  13819  modmuladd  13820  modmuladdnn0  13822  modltm1p1mod  13830  2txmodxeq0  13838  2submod  13839  moddi  13846  modsubdir  13847  modeqmodmin  13848  modirr  13849  rpexpmord  14075  expnlbnd  14140  rennim  15146  cnpart  15147  01sqrexlem1  15149  01sqrexlem2  15150  01sqrexlem4  15152  01sqrexlem5  15153  01sqrexlem6  15154  01sqrexlem7  15155  resqrex  15157  rpsqrtcl  15171  sqreulem  15267  eqsqrt2d  15276  2clim  15479  reccn2  15504  cn1lem  15505  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  climsup  15577  climcau  15578  caucvgrlem2  15582  iseralt  15592  cvgcmp  15723  cvgcmpce  15725  divrcnv  15759  rprisefaccl  15930  efgt1  16025  ef01bndlem  16093  sinltx  16098  stdbdmet  24431  stdbdmopn  24433  met2ndci  24437  cfilucfil  24474  ngptgp  24551  reperflem  24734  iccntr  24737  reconnlem2  24743  opnreen  24747  metdseq0  24770  xlebnum  24891  cphsqrtcl3  25114  iscmet3lem3  25217  iscmet3lem1  25218  iscmet3lem2  25219  caubl  25235  lmcau  25240  bcthlem4  25254  minveclem3b  25355  minveclem3  25356  ivthlem2  25380  ivthlem3  25381  nulmbl2  25464  opnmbllem  25529  itg2const2  25669  itg2mulclem  25674  dveflem  25910  lhop  25948  dvcnvre  25951  aalioulem2  26268  aaliou  26273  aaliou3lem4  26281  ulmcaulem  26330  ulmcau  26331  ulmcn  26335  itgulm  26344  reeff1o  26384  pilem2  26389  logleb  26539  logcj  26542  argimgt0  26548  logdmnrp  26577  logcnlem3  26580  logcnlem4  26581  advlog  26590  efopnlem1  26592  cxple2  26633  cxplt2  26634  cxple3  26637  2irrexpq  26667  cxpcn3  26685  resqrtcn  26686  relogbf  26728  asinneg  26823  atanbndlem  26862  cxplim  26909  cxp2limlem  26913  cxp2lim  26914  cxploglim  26915  cxploglim2  26916  logdiflbnd  26932  harmoniclbnd  26946  harmonicbnd4  26948  chtrpcl  27112  ppiltx  27114  chtleppi  27148  logfacubnd  27159  logfaclbnd  27160  logfacbnd3  27161  logexprlim  27163  bposlem7  27228  bposlem8  27229  bposlem9  27230  chebbnd1  27410  chtppilim  27413  chto1ub  27414  chpo1ub  27418  vmadivsum  27420  rpvmasumlem  27425  dchrisumlem3  27429  dchrvmasumlem2  27436  dchrvmasumiflem1  27439  dchrisum0  27458  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  mulog2sumlem2  27473  log2sumbnd  27482  selberglem2  27484  selberglem3  27485  selberg  27486  selberg2lem  27488  selberg2  27489  pntrf  27501  pntrmax  27502  pntrsumo1  27503  selbergr  27506  selbergs  27512  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntibndlem1  27527  pntlem3  27547  pntlemp  27548  pntleml  27549  pnt2  27551  padicabvcxp  27570  vacn  30674  nmcvcn  30675  smcnlem  30677  blocnilem  30784  chscllem2  31618  nmcexi  32006  nmcopexi  32007  nmcfnexi  32031  dp2ltsuc  32866  dpval3rp  32880  dplti  32885  dpgti  32886  dpexpp1  32888  dpadd2  32890  pnfinf  33152  sqsscirc1  33921  dya2icoseg2  34291  probfinmeasb  34441  probfinmeasbALTV  34442  signshf  34601  divsqrtid  34607  logdivsqrle  34663  hgt750lem2  34665  subfacval3  35233  opnrebl  36362  opnrebl2  36363  taupilem1  37363  opnmbllem0  37704  itg2addnclem  37719  itg2addnclem2  37720  itg2addnclem3  37721  itg2addnc  37722  itg2gt0cn  37723  ftc1anclem5  37745  ftc1anclem7  37747  ftc1anc  37749  areacirclem1  37756  areacirclem4  37759  areacirc  37761  geomcau  37807  isbnd2  37831  ssbnd  37836  heiborlem7  37865  heiborlem8  37866  bfplem2  37871  rrncmslem  37880  rrnequiv  37883  dvrelog3  42106  aks4d1p1p6  42114  rpabsid  42362  irrapxlem1  42863  irrapxlem2  42864  irrapxlem3  42865  irrapxlem5  42867  2timesgt  45337  supxrge  45385  suplesup  45386  xrlexaddrp  45399  xralrple2  45401  infleinflem1  45416  xralrple4  45419  xralrple3  45420  xrralrecnnle  45429  climinf  45654  mullimc  45664  mullimcf  45671  limcrecl  45677  limcleqr  45690  addlimc  45694  0ellimcdiv  45695  limclner  45697  liminflimsupclim  45853  ioodvbdlimc1lem1  45977  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  stoweidlem7  46053  fourierdlem73  46225  fourierdlem87  46239  fourierdlem103  46255  fourierdlem104  46256  sge0iunmptlemre  46461  smflimlem4  46820  fldivexpfllog2  48605  blenre  48614  itscnhlc0yqe  48799  itscnhlc0xyqsol  48805  itschlc0xyqsol  48807  itsclc0xyqsolr  48809  itsclinecirc0in  48815  itsclquadb  48816  itscnhlinecirc02plem3  48824  itscnhlinecirc02p  48825  inlinecirc02plem  48826  inlinecirc02p  48827  amgmwlem  49842