Theorem rpre 12559

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℝcr 10693  ℝ⁺crp 12551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-rp 12552

This theorem is referenced by:  rpxr  12560  rpcn  12561  rpge0  12564  rprege0  12566  rprene0  12568  rpaddcl  12573  rpmulcl  12574  rpdivcl  12576  rpgecl  12579  ledivge1le  12622  addlelt  12665  xralrple  12760  xlemul1  12845  infmrp1  12899  iccdil  13043  ltdifltdiv  13374  modcl  13411  mod0  13414  mulmod0  13415  modge0  13417  modlt  13418  modid0  13435  modabs  13442  modabs2  13443  modcyc  13444  modmuladd  13451  modmuladdnn0  13453  modltm1p1mod  13461  2txmodxeq0  13469  2submod  13470  moddi  13477  modsubdir  13478  modeqmodmin  13479  modirr  13480  rpexpmord  13703  expnlbnd  13765  rennim  14767  cnpart  14768  sqrlem1  14771  sqrlem2  14772  sqrlem4  14774  sqrlem5  14775  sqrlem6  14776  sqrlem7  14777  resqrex  14779  rpsqrtcl  14793  sqreulem  14888  eqsqrt2d  14897  2clim  15098  reccn2  15123  cn1lem  15124  climsqz  15167  climsqz2  15168  rlimsqzlem  15177  climsup  15198  climcau  15199  caucvgrlem2  15203  iseralt  15213  cvgcmp  15343  cvgcmpce  15345  divrcnv  15379  rprisefaccl  15548  efgt1  15640  ef01bndlem  15708  sinltx  15713  stdbdmet  23368  stdbdmopn  23370  met2ndci  23374  cfilucfil  23411  ngptgp  23488  reperflem  23669  iccntr  23672  reconnlem2  23678  opnreen  23682  metdseq0  23705  xlebnum  23816  cphsqrtcl3  24038  iscmet3lem3  24141  iscmet3lem1  24142  iscmet3lem2  24143  caubl  24159  lmcau  24164  bcthlem4  24178  minveclem3b  24279  minveclem3  24280  ivthlem2  24303  ivthlem3  24304  nulmbl2  24387  opnmbllem  24452  itg2const2  24593  itg2mulclem  24598  dveflem  24830  lhop  24867  dvcnvre  24870  aalioulem2  25180  aaliou  25185  aaliou3lem4  25193  ulmcaulem  25240  ulmcau  25241  ulmcn  25245  itgulm  25254  reeff1o  25293  pilem2  25298  logleb  25445  logcj  25448  argimgt0  25454  logdmnrp  25483  logcnlem3  25486  logcnlem4  25487  advlog  25496  efopnlem1  25498  cxple2  25539  cxplt2  25540  cxple3  25543  2irrexpq  25572  cxpcn3  25588  resqrtcn  25589  relogbf  25628  asinneg  25723  atanbndlem  25762  cxplim  25808  cxp2limlem  25812  cxp2lim  25813  cxploglim  25814  cxploglim2  25815  logdiflbnd  25831  harmoniclbnd  25845  harmonicbnd4  25847  chtrpcl  26011  ppiltx  26013  chtleppi  26045  logfacubnd  26056  logfaclbnd  26057  logfacbnd3  26058  logexprlim  26060  bposlem7  26125  bposlem8  26126  bposlem9  26127  chebbnd1  26307  chtppilim  26310  chto1ub  26311  chpo1ub  26315  vmadivsum  26317  rpvmasumlem  26322  dchrisumlem3  26326  dchrvmasumlem2  26333  dchrvmasumiflem1  26336  dchrisum0  26355  mudivsum  26365  mulogsumlem  26366  mulogsum  26367  mulog2sumlem2  26370  log2sumbnd  26379  selberglem2  26381  selberglem3  26382  selberg  26383  selberg2lem  26385  selberg2  26386  pntrf  26398  pntrmax  26399  pntrsumo1  26400  selbergr  26403  selbergs  26409  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntibndlem1  26424  pntlem3  26444  pntlemp  26445  pntleml  26446  pnt2  26448  padicabvcxp  26467  vacn  28729  nmcvcn  28730  smcnlem  28732  blocnilem  28839  chscllem2  29673  nmcexi  30061  nmcopexi  30062  nmcfnexi  30086  dp2ltsuc  30834  dpval3rp  30848  dplti  30853  dpgti  30854  dpexpp1  30856  dpadd2  30858  pnfinf  31110  sqsscirc1  31526  dya2icoseg2  31911  probfinmeasb  32061  probfinmeasbALTV  32062  signshf  32233  divsqrtid  32240  logdivsqrle  32296  hgt750lem2  32298  subfacval3  32818  opnrebl  34195  opnrebl2  34196  taupilem1  35175  opnmbllem0  35499  itg2addnclem  35514  itg2addnclem2  35515  itg2addnclem3  35516  itg2addnc  35517  itg2gt0cn  35518  ftc1anclem5  35540  ftc1anclem7  35542  ftc1anc  35544  areacirclem1  35551  areacirclem4  35554  areacirc  35556  geomcau  35603  isbnd2  35627  ssbnd  35632  heiborlem7  35661  heiborlem8  35662  bfplem2  35667  rrncmslem  35676  rrnequiv  35679  dvrelog3  39755  aks4d1p1p6  39763  irrapxlem1  40288  irrapxlem2  40289  irrapxlem3  40290  irrapxlem5  40292  neglt  42436  2timesgt  42440  supxrge  42491  suplesup  42492  xrlexaddrp  42505  xralrple2  42507  infleinflem1  42523  xralrple4  42526  xralrple3  42527  xrralrecnnle  42536  climinf  42765  mullimc  42775  mullimcf  42782  limcrecl  42788  limcleqr  42803  addlimc  42807  0ellimcdiv  42808  limclner  42810  liminflimsupclim  42966  ioodvbdlimc1lem1  43090  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  stoweidlem7  43166  fourierdlem73  43338  fourierdlem87  43352  fourierdlem103  43368  fourierdlem104  43369  sge0iunmptlemre  43571  smflimlem4  43924  fldivexpfllog2  45527  blenre  45536  itscnhlc0yqe  45721  itscnhlc0xyqsol  45727  itschlc0xyqsol  45729  itsclc0xyqsolr  45731  itsclinecirc0in  45737  itsclquadb  45738  itscnhlinecirc02plem3  45746  itscnhlinecirc02p  45747  inlinecirc02plem  45748  inlinecirc02p  45749  amgmwlem  46120