Theorem rpre 12912

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11023  ℝ⁺crp 12903

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-ss 3916  df-rp 12904

This theorem is referenced by:  rpxr  12913  rpcn  12914  rpge0  12917  rprege0  12919  rprene0  12921  neglt  12923  rpaddcl  12927  rpmulcl  12928  rpdivcl  12930  rpgecl  12933  ledivge1le  12976  addlelt  13019  xralrple  13118  xlemul1  13203  infmrp1  13258  iccdil  13404  ltdifltdiv  13752  modcl  13791  mod0  13794  mulmod0  13795  modge0  13797  modlt  13798  modid0  13815  modabs  13822  modabs2  13823  modcyc  13824  muladdmod  13833  modmuladd  13834  modmuladdnn0  13836  modltm1p1mod  13844  2txmodxeq0  13852  2submod  13853  moddi  13860  modsubdir  13861  modeqmodmin  13862  modirr  13863  rpexpmord  14089  expnlbnd  14154  rennim  15160  cnpart  15161  01sqrexlem1  15163  01sqrexlem2  15164  01sqrexlem4  15166  01sqrexlem5  15167  01sqrexlem6  15168  01sqrexlem7  15169  resqrex  15171  rpsqrtcl  15185  sqreulem  15281  eqsqrt2d  15290  2clim  15493  reccn2  15518  cn1lem  15519  climsqz  15562  climsqz2  15563  rlimsqzlem  15570  climsup  15591  climcau  15592  caucvgrlem2  15596  iseralt  15606  cvgcmp  15737  cvgcmpce  15739  divrcnv  15773  rprisefaccl  15944  efgt1  16039  ef01bndlem  16107  sinltx  16112  stdbdmet  24458  stdbdmopn  24460  met2ndci  24464  cfilucfil  24501  ngptgp  24578  reperflem  24761  iccntr  24764  reconnlem2  24770  opnreen  24774  metdseq0  24797  xlebnum  24918  cphsqrtcl3  25141  iscmet3lem3  25244  iscmet3lem1  25245  iscmet3lem2  25246  caubl  25262  lmcau  25267  bcthlem4  25281  minveclem3b  25382  minveclem3  25383  ivthlem2  25407  ivthlem3  25408  nulmbl2  25491  opnmbllem  25556  itg2const2  25696  itg2mulclem  25701  dveflem  25937  lhop  25975  dvcnvre  25978  aalioulem2  26295  aaliou  26300  aaliou3lem4  26308  ulmcaulem  26357  ulmcau  26358  ulmcn  26362  itgulm  26371  reeff1o  26411  pilem2  26416  logleb  26566  logcj  26569  argimgt0  26575  logdmnrp  26604  logcnlem3  26607  logcnlem4  26608  advlog  26617  efopnlem1  26619  cxple2  26660  cxplt2  26661  cxple3  26664  2irrexpq  26694  cxpcn3  26712  resqrtcn  26713  relogbf  26755  asinneg  26850  atanbndlem  26889  cxplim  26936  cxp2limlem  26940  cxp2lim  26941  cxploglim  26942  cxploglim2  26943  logdiflbnd  26959  harmoniclbnd  26973  harmonicbnd4  26975  chtrpcl  27139  ppiltx  27141  chtleppi  27175  logfacubnd  27186  logfaclbnd  27187  logfacbnd3  27188  logexprlim  27190  bposlem7  27255  bposlem8  27256  bposlem9  27257  chebbnd1  27437  chtppilim  27440  chto1ub  27441  chpo1ub  27445  vmadivsum  27447  rpvmasumlem  27452  dchrisumlem3  27456  dchrvmasumlem2  27463  dchrvmasumiflem1  27466  dchrisum0  27485  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  mulog2sumlem2  27500  log2sumbnd  27509  selberglem2  27511  selberglem3  27512  selberg  27513  selberg2lem  27515  selberg2  27516  pntrf  27528  pntrmax  27529  pntrsumo1  27530  selbergr  27533  selbergs  27539  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntibndlem1  27554  pntlem3  27574  pntlemp  27575  pntleml  27576  pnt2  27578  padicabvcxp  27597  vacn  30718  nmcvcn  30719  smcnlem  30721  blocnilem  30828  chscllem2  31662  nmcexi  32050  nmcopexi  32051  nmcfnexi  32075  dp2ltsuc  32916  dpval3rp  32930  dplti  32935  dpgti  32936  dpexpp1  32938  dpadd2  32940  pnfinf  33214  sqsscirc1  34014  dya2icoseg2  34384  probfinmeasb  34534  probfinmeasbALTV  34535  signshf  34694  divsqrtid  34700  logdivsqrle  34756  hgt750lem2  34758  subfacval3  35332  opnrebl  36463  opnrebl2  36464  taupilem1  37465  opnmbllem0  37796  itg2addnclem  37811  itg2addnclem2  37812  itg2addnclem3  37813  itg2addnc  37814  itg2gt0cn  37815  ftc1anclem5  37837  ftc1anclem7  37839  ftc1anc  37841  areacirclem1  37848  areacirclem4  37851  areacirc  37853  geomcau  37899  isbnd2  37923  ssbnd  37928  heiborlem7  37957  heiborlem8  37958  bfplem2  37963  rrncmslem  37972  rrnequiv  37975  dvrelog3  42258  aks4d1p1p6  42266  rpabsid  42518  irrapxlem1  43006  irrapxlem2  43007  irrapxlem3  43008  irrapxlem5  43010  2timesgt  45478  supxrge  45525  suplesup  45526  xrlexaddrp  45539  xralrple2  45541  infleinflem1  45556  xralrple4  45559  xralrple3  45560  xrralrecnnle  45569  climinf  45794  mullimc  45804  mullimcf  45811  limcrecl  45817  limcleqr  45830  addlimc  45834  0ellimcdiv  45835  limclner  45837  liminflimsupclim  45993  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  stoweidlem7  46193  fourierdlem73  46365  fourierdlem87  46379  fourierdlem103  46395  fourierdlem104  46396  sge0iunmptlemre  46601  smflimlem4  46960  fldivexpfllog2  48753  blenre  48762  itscnhlc0yqe  48947  itscnhlc0xyqsol  48953  itschlc0xyqsol  48955  itsclc0xyqsolr  48957  itsclinecirc0in  48963  itsclquadb  48964  itscnhlinecirc02plem3  48972  itscnhlinecirc02p  48973  inlinecirc02plem  48974  inlinecirc02p  48975  amgmwlem  49989