Theorem rpre 12960

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-rp 12952

This theorem is referenced by:  rpxr  12961  rpcn  12962  rpge0  12965  rprege0  12967  rprene0  12969  neglt  12971  rpaddcl  12975  rpmulcl  12976  rpdivcl  12978  rpgecl  12981  ledivge1le  13024  addlelt  13067  xralrple  13165  xlemul1  13250  infmrp1  13305  iccdil  13451  ltdifltdiv  13796  modcl  13835  mod0  13838  mulmod0  13839  modge0  13841  modlt  13842  modid0  13859  modabs  13866  modabs2  13867  modcyc  13868  muladdmod  13877  modmuladd  13878  modmuladdnn0  13880  modltm1p1mod  13888  2txmodxeq0  13896  2submod  13897  moddi  13904  modsubdir  13905  modeqmodmin  13906  modirr  13907  rpexpmord  14133  expnlbnd  14198  rennim  15205  cnpart  15206  01sqrexlem1  15208  01sqrexlem2  15209  01sqrexlem4  15211  01sqrexlem5  15212  01sqrexlem6  15213  01sqrexlem7  15214  resqrex  15216  rpsqrtcl  15230  sqreulem  15326  eqsqrt2d  15335  2clim  15538  reccn2  15563  cn1lem  15564  climsqz  15607  climsqz2  15608  rlimsqzlem  15615  climsup  15636  climcau  15637  caucvgrlem2  15641  iseralt  15651  cvgcmp  15782  cvgcmpce  15784  divrcnv  15818  rprisefaccl  15989  efgt1  16084  ef01bndlem  16152  sinltx  16157  stdbdmet  24404  stdbdmopn  24406  met2ndci  24410  cfilucfil  24447  ngptgp  24524  reperflem  24707  iccntr  24710  reconnlem2  24716  opnreen  24720  metdseq0  24743  xlebnum  24864  cphsqrtcl3  25087  iscmet3lem3  25190  iscmet3lem1  25191  iscmet3lem2  25192  caubl  25208  lmcau  25213  bcthlem4  25227  minveclem3b  25328  minveclem3  25329  ivthlem2  25353  ivthlem3  25354  nulmbl2  25437  opnmbllem  25502  itg2const2  25642  itg2mulclem  25647  dveflem  25883  lhop  25921  dvcnvre  25924  aalioulem2  26241  aaliou  26246  aaliou3lem4  26254  ulmcaulem  26303  ulmcau  26304  ulmcn  26308  itgulm  26317  reeff1o  26357  pilem2  26362  logleb  26512  logcj  26515  argimgt0  26521  logdmnrp  26550  logcnlem3  26553  logcnlem4  26554  advlog  26563  efopnlem1  26565  cxple2  26606  cxplt2  26607  cxple3  26610  2irrexpq  26640  cxpcn3  26658  resqrtcn  26659  relogbf  26701  asinneg  26796  atanbndlem  26835  cxplim  26882  cxp2limlem  26886  cxp2lim  26887  cxploglim  26888  cxploglim2  26889  logdiflbnd  26905  harmoniclbnd  26919  harmonicbnd4  26921  chtrpcl  27085  ppiltx  27087  chtleppi  27121  logfacubnd  27132  logfaclbnd  27133  logfacbnd3  27134  logexprlim  27136  bposlem7  27201  bposlem8  27202  bposlem9  27203  chebbnd1  27383  chtppilim  27386  chto1ub  27387  chpo1ub  27391  vmadivsum  27393  rpvmasumlem  27398  dchrisumlem3  27402  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0  27431  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem2  27446  log2sumbnd  27455  selberglem2  27457  selberglem3  27458  selberg  27459  selberg2lem  27461  selberg2  27462  pntrf  27474  pntrmax  27475  pntrsumo1  27476  selbergr  27479  selbergs  27485  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntibndlem1  27500  pntlem3  27520  pntlemp  27521  pntleml  27522  pnt2  27524  padicabvcxp  27543  vacn  30623  nmcvcn  30624  smcnlem  30626  blocnilem  30733  chscllem2  31567  nmcexi  31955  nmcopexi  31956  nmcfnexi  31980  dp2ltsuc  32806  dpval3rp  32820  dplti  32825  dpgti  32826  dpexpp1  32828  dpadd2  32830  pnfinf  33137  sqsscirc1  33898  dya2icoseg2  34269  probfinmeasb  34419  probfinmeasbALTV  34420  signshf  34579  divsqrtid  34585  logdivsqrle  34641  hgt750lem2  34643  subfacval3  35176  opnrebl  36308  opnrebl2  36309  taupilem1  37309  opnmbllem0  37650  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anc  37695  areacirclem1  37702  areacirclem4  37705  areacirc  37707  geomcau  37753  isbnd2  37777  ssbnd  37782  heiborlem7  37811  heiborlem8  37812  bfplem2  37817  rrncmslem  37826  rrnequiv  37829  dvrelog3  42053  aks4d1p1p6  42061  rpabsid  42309  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  irrapxlem5  42814  2timesgt  45286  supxrge  45334  suplesup  45335  xrlexaddrp  45348  xralrple2  45350  infleinflem1  45366  xralrple4  45369  xralrple3  45370  xrralrecnnle  45379  climinf  45604  mullimc  45614  mullimcf  45621  limcrecl  45627  limcleqr  45642  addlimc  45646  0ellimcdiv  45647  limclner  45649  liminflimsupclim  45805  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem7  46005  fourierdlem73  46177  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  sge0iunmptlemre  46413  smflimlem4  46772  fldivexpfllog2  48554  blenre  48563  itscnhlc0yqe  48748  itscnhlc0xyqsol  48754  itschlc0xyqsol  48756  itsclc0xyqsolr  48758  itsclinecirc0in  48764  itsclquadb  48765  itscnhlinecirc02plem3  48773  itscnhlinecirc02p  48774  inlinecirc02plem  48775  inlinecirc02p  48776  amgmwlem  49791