Theorem rpre 12951

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-rp 12943

This theorem is referenced by:  rpxr  12952  rpcn  12953  rpge0  12956  rprege0  12958  rprene0  12960  neglt  12962  rpaddcl  12966  rpmulcl  12967  rpdivcl  12969  rpgecl  12972  ledivge1le  13015  addlelt  13058  xralrple  13157  xlemul1  13242  infmrp1  13297  iccdil  13443  ltdifltdiv  13793  modcl  13832  mod0  13835  mulmod0  13836  modge0  13838  modlt  13839  modid0  13856  modabs  13863  modabs2  13864  modcyc  13865  muladdmod  13874  modmuladd  13875  modmuladdnn0  13877  modltm1p1mod  13885  2txmodxeq0  13893  2submod  13894  moddi  13901  modsubdir  13902  modeqmodmin  13903  modirr  13904  rpexpmord  14130  expnlbnd  14195  rennim  15201  cnpart  15202  01sqrexlem1  15204  01sqrexlem2  15205  01sqrexlem4  15207  01sqrexlem5  15208  01sqrexlem6  15209  01sqrexlem7  15210  resqrex  15212  rpsqrtcl  15226  sqreulem  15322  eqsqrt2d  15331  2clim  15534  reccn2  15559  cn1lem  15560  climsqz  15603  climsqz2  15604  rlimsqzlem  15611  climsup  15632  climcau  15633  caucvgrlem2  15637  iseralt  15647  cvgcmp  15779  cvgcmpce  15781  divrcnv  15817  rprisefaccl  15988  efgt1  16083  ef01bndlem  16151  sinltx  16156  stdbdmet  24481  stdbdmopn  24483  met2ndci  24487  cfilucfil  24524  ngptgp  24601  reperflem  24784  iccntr  24787  reconnlem2  24793  opnreen  24797  metdseq0  24820  xlebnum  24932  cphsqrtcl3  25154  iscmet3lem3  25257  iscmet3lem1  25258  iscmet3lem2  25259  caubl  25275  lmcau  25280  bcthlem4  25294  minveclem3b  25395  minveclem3  25396  ivthlem2  25419  ivthlem3  25420  nulmbl2  25503  opnmbllem  25568  itg2const2  25708  itg2mulclem  25713  dveflem  25946  lhop  25983  dvcnvre  25986  aalioulem2  26299  aaliou  26304  aaliou3lem4  26312  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  itgulm  26373  reeff1o  26412  pilem2  26417  logleb  26567  logcj  26570  argimgt0  26576  logdmnrp  26605  logcnlem3  26608  logcnlem4  26609  advlog  26618  efopnlem1  26620  cxple2  26661  cxplt2  26662  cxple3  26665  2irrexpq  26695  cxpcn3  26712  resqrtcn  26713  relogbf  26755  asinneg  26850  atanbndlem  26889  cxplim  26935  cxp2limlem  26939  cxp2lim  26940  cxploglim  26941  cxploglim2  26942  logdiflbnd  26958  harmoniclbnd  26972  harmonicbnd4  26974  chtrpcl  27138  ppiltx  27140  chtleppi  27173  logfacubnd  27184  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  bposlem7  27253  bposlem8  27254  bposlem9  27255  chebbnd1  27435  chtppilim  27438  chto1ub  27439  chpo1ub  27443  vmadivsum  27445  rpvmasumlem  27450  dchrisumlem3  27454  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0  27483  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem2  27498  log2sumbnd  27507  selberglem2  27509  selberglem3  27510  selberg  27511  selberg2lem  27513  selberg2  27514  pntrf  27526  pntrmax  27527  pntrsumo1  27528  selbergr  27531  selbergs  27537  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntibndlem1  27552  pntlem3  27572  pntlemp  27573  pntleml  27574  pnt2  27576  padicabvcxp  27595  vacn  30765  nmcvcn  30766  smcnlem  30768  blocnilem  30875  chscllem2  31709  nmcexi  32097  nmcopexi  32098  nmcfnexi  32122  dp2ltsuc  32945  dpval3rp  32959  dplti  32964  dpgti  32965  dpexpp1  32967  dpadd2  32969  pnfinf  33244  sqsscirc1  34052  dya2icoseg2  34422  probfinmeasb  34572  probfinmeasbALTV  34573  signshf  34732  divsqrtid  34738  logdivsqrle  34794  hgt750lem2  34796  subfacval3  35371  opnrebl  36502  opnrebl2  36503  taupilem1  37635  opnmbllem0  37977  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anc  38022  areacirclem1  38029  areacirclem4  38032  areacirc  38034  geomcau  38080  isbnd2  38104  ssbnd  38109  heiborlem7  38138  heiborlem8  38139  bfplem2  38144  rrncmslem  38153  rrnequiv  38156  dvrelog3  42504  aks4d1p1p6  42512  rpabsid  42753  irrapxlem1  43250  irrapxlem2  43251  irrapxlem3  43252  irrapxlem5  43254  2timesgt  45721  supxrge  45768  suplesup  45769  xrlexaddrp  45782  xralrple2  45784  infleinflem1  45799  xralrple4  45802  xralrple3  45803  xrralrecnnle  45812  climinf  46036  mullimc  46046  mullimcf  46053  limcrecl  46059  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  limclner  46079  liminflimsupclim  46235  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem7  46435  fourierdlem73  46607  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  sge0iunmptlemre  46843  smflimlem4  47202  fldivexpfllog2  49041  blenre  49050  itscnhlc0yqe  49235  itscnhlc0xyqsol  49241  itschlc0xyqsol  49243  itsclc0xyqsolr  49245  itsclinecirc0in  49251  itsclquadb  49252  itscnhlinecirc02plem3  49260  itscnhlinecirc02p  49261  inlinecirc02plem  49262  inlinecirc02p  49263  amgmwlem  50277