Theorem rpre 12945

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11031  ℝ⁺crp 12936

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-rp 12937

This theorem is referenced by:  rpxr  12946  rpcn  12947  rpge0  12950  rprege0  12952  rprene0  12954  neglt  12956  rpaddcl  12960  rpmulcl  12961  rpdivcl  12963  rpgecl  12966  ledivge1le  13009  addlelt  13052  xralrple  13151  xlemul1  13236  infmrp1  13291  iccdil  13437  ltdifltdiv  13787  modcl  13826  mod0  13829  mulmod0  13830  modge0  13832  modlt  13833  modid0  13850  modabs  13857  modabs2  13858  modcyc  13859  muladdmod  13868  modmuladd  13869  modmuladdnn0  13871  modltm1p1mod  13879  2txmodxeq0  13887  2submod  13888  moddi  13895  modsubdir  13896  modeqmodmin  13897  modirr  13898  rpexpmord  14124  expnlbnd  14189  rennim  15195  cnpart  15196  01sqrexlem1  15198  01sqrexlem2  15199  01sqrexlem4  15201  01sqrexlem5  15202  01sqrexlem6  15203  01sqrexlem7  15204  resqrex  15206  rpsqrtcl  15220  sqreulem  15316  eqsqrt2d  15325  2clim  15528  reccn2  15553  cn1lem  15554  climsqz  15597  climsqz2  15598  rlimsqzlem  15605  climsup  15626  climcau  15627  caucvgrlem2  15631  iseralt  15641  cvgcmp  15773  cvgcmpce  15775  divrcnv  15811  rprisefaccl  15982  efgt1  16077  ef01bndlem  16145  sinltx  16150  stdbdmet  24494  stdbdmopn  24496  met2ndci  24500  cfilucfil  24537  ngptgp  24614  reperflem  24797  iccntr  24800  reconnlem2  24806  opnreen  24810  metdseq0  24833  xlebnum  24945  cphsqrtcl3  25167  iscmet3lem3  25270  iscmet3lem1  25271  iscmet3lem2  25272  caubl  25288  lmcau  25293  bcthlem4  25307  minveclem3b  25408  minveclem3  25409  ivthlem2  25432  ivthlem3  25433  nulmbl2  25516  opnmbllem  25581  itg2const2  25721  itg2mulclem  25726  dveflem  25959  lhop  25996  dvcnvre  25999  aalioulem2  26313  aaliou  26318  aaliou3lem4  26326  ulmcaulem  26375  ulmcau  26376  ulmcn  26380  itgulm  26389  reeff1o  26428  pilem2  26433  logleb  26583  logcj  26586  argimgt0  26592  logdmnrp  26621  logcnlem3  26624  logcnlem4  26625  advlog  26634  efopnlem1  26636  cxple2  26677  cxplt2  26678  cxple3  26681  2irrexpq  26711  cxpcn3  26728  resqrtcn  26729  relogbf  26771  asinneg  26866  atanbndlem  26905  cxplim  26952  cxp2limlem  26956  cxp2lim  26957  cxploglim  26958  cxploglim2  26959  logdiflbnd  26975  harmoniclbnd  26989  harmonicbnd4  26991  chtrpcl  27155  ppiltx  27157  chtleppi  27190  logfacubnd  27201  logfaclbnd  27202  logfacbnd3  27203  logexprlim  27205  bposlem7  27270  bposlem8  27271  bposlem9  27272  chebbnd1  27452  chtppilim  27455  chto1ub  27456  chpo1ub  27460  vmadivsum  27462  rpvmasumlem  27467  dchrisumlem3  27471  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0  27500  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem2  27515  log2sumbnd  27524  selberglem2  27526  selberglem3  27527  selberg  27528  selberg2lem  27530  selberg2  27531  pntrf  27543  pntrmax  27544  pntrsumo1  27545  selbergr  27548  selbergs  27554  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntibndlem1  27569  pntlem3  27589  pntlemp  27590  pntleml  27591  pnt2  27593  padicabvcxp  27612  vacn  30783  nmcvcn  30784  smcnlem  30786  blocnilem  30893  chscllem2  31727  nmcexi  32115  nmcopexi  32116  nmcfnexi  32140  dp2ltsuc  32963  dpval3rp  32977  dplti  32982  dpgti  32983  dpexpp1  32985  dpadd2  32987  pnfinf  33262  sqsscirc1  34071  dya2icoseg2  34441  probfinmeasb  34591  probfinmeasbALTV  34592  signshf  34751  divsqrtid  34757  logdivsqrle  34813  hgt750lem2  34815  subfacval3  35390  opnrebl  36521  opnrebl2  36522  taupilem1  37654  opnmbllem0  37994  itg2addnclem  38009  itg2addnclem2  38010  itg2addnclem3  38011  itg2addnc  38012  itg2gt0cn  38013  ftc1anclem5  38035  ftc1anclem7  38037  ftc1anc  38039  areacirclem1  38046  areacirclem4  38049  areacirc  38051  geomcau  38097  isbnd2  38121  ssbnd  38126  heiborlem7  38155  heiborlem8  38156  bfplem2  38161  rrncmslem  38170  rrnequiv  38173  dvrelog3  42521  aks4d1p1p6  42529  rpabsid  42770  irrapxlem1  43271  irrapxlem2  43272  irrapxlem3  43273  irrapxlem5  43275  2timesgt  45742  supxrge  45789  suplesup  45790  xrlexaddrp  45803  xralrple2  45805  infleinflem1  45820  xralrple4  45823  xralrple3  45824  xrralrecnnle  45833  climinf  46057  mullimc  46067  mullimcf  46074  limcrecl  46080  limcleqr  46093  addlimc  46097  0ellimcdiv  46098  limclner  46100  liminflimsupclim  46256  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  stoweidlem7  46456  fourierdlem73  46628  fourierdlem87  46642  fourierdlem103  46658  fourierdlem104  46659  sge0iunmptlemre  46864  smflimlem4  47223  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