Theorem rpre 12942

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11028  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-ss 3900  df-rp 12934

This theorem is referenced by:  rpxr  12943  rpcn  12944  rpge0  12947  rprege0  12949  rprene0  12951  neglt  12953  rpaddcl  12957  rpmulcl  12958  rpdivcl  12960  rpgecl  12963  ledivge1le  13006  addlelt  13049  xralrple  13148  xlemul1  13233  infmrp1  13288  iccdil  13434  ltdifltdiv  13784  modcl  13823  mod0  13826  mulmod0  13827  modge0  13829  modlt  13830  modid0  13847  modabs  13854  modabs2  13855  modcyc  13856  muladdmod  13865  modmuladd  13866  modmuladdnn0  13868  modltm1p1mod  13876  2txmodxeq0  13884  2submod  13885  moddi  13892  modsubdir  13893  modeqmodmin  13894  modirr  13895  rpexpmord  14121  expnlbnd  14186  rennim  15192  cnpart  15193  01sqrexlem1  15195  01sqrexlem2  15196  01sqrexlem4  15198  01sqrexlem5  15199  01sqrexlem6  15200  01sqrexlem7  15201  resqrex  15203  rpsqrtcl  15217  sqreulem  15313  eqsqrt2d  15322  2clim  15525  reccn2  15550  cn1lem  15551  climsqz  15594  climsqz2  15595  rlimsqzlem  15602  climsup  15623  climcau  15624  caucvgrlem2  15628  iseralt  15638  cvgcmp  15770  cvgcmpce  15772  divrcnv  15808  rprisefaccl  15979  efgt1  16074  ef01bndlem  16142  sinltx  16147  stdbdmet  24499  stdbdmopn  24501  met2ndci  24505  cfilucfil  24542  ngptgp  24619  reperflem  24802  iccntr  24805  reconnlem2  24811  opnreen  24815  metdseq0  24838  xlebnum  24950  cphsqrtcl3  25172  iscmet3lem3  25275  iscmet3lem1  25276  iscmet3lem2  25277  caubl  25293  lmcau  25298  bcthlem4  25312  minveclem3b  25413  minveclem3  25414  ivthlem2  25437  ivthlem3  25438  nulmbl2  25521  opnmbllem  25586  itg2const2  25726  itg2mulclem  25731  dveflem  25964  lhop  26001  dvcnvre  26004  aalioulem2  26317  aaliou  26322  aaliou3lem4  26330  ulmcaulem  26377  ulmcau  26378  ulmcn  26382  itgulm  26391  reeff1o  26430  pilem2  26435  logleb  26585  logcj  26588  argimgt0  26594  logdmnrp  26623  logcnlem3  26626  logcnlem4  26627  advlog  26636  efopnlem1  26638  cxple2  26679  cxplt2  26680  cxple3  26683  2irrexpq  26713  cxpcn3  26730  resqrtcn  26731  relogbf  26773  asinneg  26868  atanbndlem  26907  cxplim  26953  cxp2limlem  26957  cxp2lim  26958  cxploglim  26959  cxploglim2  26960  logdiflbnd  26976  harmoniclbnd  26990  harmonicbnd4  26992  chtrpcl  27156  ppiltx  27158  chtleppi  27191  logfacubnd  27202  logfaclbnd  27203  logfacbnd3  27204  logexprlim  27206  bposlem7  27271  bposlem8  27272  bposlem9  27273  chebbnd1  27453  chtppilim  27456  chto1ub  27457  chpo1ub  27461  vmadivsum  27463  rpvmasumlem  27468  dchrisumlem3  27472  dchrvmasumlem2  27479  dchrvmasumiflem1  27482  dchrisum0  27501  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  mulog2sumlem2  27516  log2sumbnd  27525  selberglem2  27527  selberglem3  27528  selberg  27529  selberg2lem  27531  selberg2  27532  pntrf  27544  pntrmax  27545  pntrsumo1  27546  selbergr  27549  selbergs  27555  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntibndlem1  27570  pntlem3  27590  pntlemp  27591  pntleml  27592  pnt2  27594  padicabvcxp  27613  vacn  30783  nmcvcn  30784  smcnlem  30786  blocnilem  30893  chscllem2  31727  nmcexi  32115  nmcopexi  32116  nmcfnexi  32140  dp2ltsuc  32964  dpval3rp  32978  dplti  32983  dpgti  32984  dpexpp1  32986  dpadd2  32988  pnfinf  33264  sqsscirc1  34092  dya2icoseg2  34462  probfinmeasb  34612  probfinmeasbALTV  34613  signshf  34772  divsqrtid  34778  logdivsqrle  34834  hgt750lem2  34836  subfacval3  35417  opnrebl  36548  opnrebl2  36549  taupilem1  37681  opnmbllem0  38023  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  ftc1anclem5  38064  ftc1anclem7  38066  ftc1anc  38068  areacirclem1  38075  areacirclem4  38078  areacirc  38080  geomcau  38126  isbnd2  38150  ssbnd  38155  heiborlem7  38184  heiborlem8  38185  bfplem2  38190  rrncmslem  38199  rrnequiv  38202  dvrelog3  42550  aks4d1p1p6  42558  rpabsid  42798  irrapxlem1  43267  irrapxlem2  43268  irrapxlem3  43269  irrapxlem5  43271  2timesgt  45736  supxrge  45783  suplesup  45784  xrlexaddrp  45797  xralrple2  45799  infleinflem1  45814  xralrple4  45817  xralrple3  45818  xrralrecnnle  45827  climinf  46051  mullimc  46061  mullimcf  46068  limcrecl  46074  limcleqr  46087  addlimc  46091  0ellimcdiv  46092  limclner  46094  liminflimsupclim  46250  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem7  46450  fourierdlem73  46622  fourierdlem87  46636  fourierdlem103  46652  fourierdlem104  46653  sge0iunmptlemre  46858  smflimlem4  47217  fldivexpfllog2  49056  blenre  49065  itscnhlc0yqe  49250  itscnhlc0xyqsol  49256  itschlc0xyqsol  49258  itsclc0xyqsolr  49260  itsclinecirc0in  49266  itsclquadb  49267  itscnhlinecirc02plem3  49275  itscnhlinecirc02p  49276  inlinecirc02plem  49277  inlinecirc02p  49278  amgmwlem  50292