Theorem rpre 13002

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℝcr 11072  ℝ⁺crp 12993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3921  df-rp 12994

This theorem is referenced by:  rpxr  13003  rpcn  13004  rpge0  13007  rprege0  13009  rprene0  13011  neglt  13013  rpaddcl  13017  rpmulcl  13018  rpdivcl  13020  rpgecl  13023  ledivge1le  13066  addlelt  13109  xralrple  13208  xlemul1  13293  infmrp1  13348  iccdil  13494  ltdifltdiv  13844  modcl  13883  mod0  13886  mulmod0  13887  modge0  13889  modlt  13890  modid0  13907  modabs  13914  modabs2  13915  modcyc  13916  muladdmod  13925  modmuladd  13926  modmuladdnn0  13928  modltm1p1mod  13936  2txmodxeq0  13944  2submod  13945  moddi  13952  modsubdir  13953  modeqmodmin  13954  modirr  13955  rpexpmord  14181  expnlbnd  14246  rennim  15266  cnpart  15267  01sqrexlem1  15269  01sqrexlem2  15270  01sqrexlem4  15272  01sqrexlem5  15273  01sqrexlem6  15274  01sqrexlem7  15275  resqrex  15277  rpsqrtcl  15291  sqreulem  15387  eqsqrt2d  15396  2clim  15599  reccn2  15624  cn1lem  15625  climsqz  15668  climsqz2  15669  rlimsqzlem  15676  climsup  15697  climcau  15698  caucvgrlem2  15702  iseralt  15712  cvgcmp  15844  cvgcmpce  15846  divrcnv  15882  rprisefaccl  16053  efgt1  16148  ef01bndlem  16216  sinltx  16221  stdbdmet  24573  stdbdmopn  24575  met2ndci  24579  cfilucfil  24616  ngptgp  24693  reperflem  24876  iccntr  24879  reconnlem2  24885  opnreen  24889  metdseq0  24912  xlebnum  25024  cphsqrtcl3  25246  iscmet3lem3  25349  iscmet3lem1  25350  iscmet3lem2  25351  caubl  25367  lmcau  25372  bcthlem4  25386  minveclem3b  25487  minveclem3  25488  ivthlem2  25511  ivthlem3  25512  nulmbl2  25595  opnmbllem  25660  itg2const2  25800  itg2mulclem  25805  dveflem  26038  lhop  26075  dvcnvre  26078  aalioulem2  26394  aaliou  26399  aaliou3lem4  26407  ulmcaulem  26454  ulmcau  26455  ulmcn  26459  itgulm  26468  reeff1o  26507  pilem2  26512  logleb  26665  logcj  26668  argimgt0  26674  logdmnrp  26703  logcnlem3  26706  logcnlem4  26707  advlog  26716  efopnlem1  26718  cxple2  26759  cxplt2  26760  cxple3  26763  2irrexpq  26793  cxpcn3  26810  resqrtcn  26811  relogbf  26853  asinneg  26948  atanbndlem  26987  cxplim  27033  cxp2limlem  27037  cxp2lim  27038  cxploglim  27039  cxploglim2  27040  logdiflbnd  27056  harmoniclbnd  27070  harmonicbnd4  27072  chtrpcl  27236  ppiltx  27238  chtleppi  27271  logfacubnd  27282  logfaclbnd  27283  logfacbnd3  27284  logexprlim  27286  bposlem7  27351  bposlem8  27352  bposlem9  27353  chebbnd1  27533  chtppilim  27536  chto1ub  27537  chpo1ub  27541  vmadivsum  27543  rpvmasumlem  27548  dchrisumlem3  27552  dchrvmasumlem2  27559  dchrvmasumiflem1  27562  dchrisum0  27581  mudivsum  27591  mulogsumlem  27592  mulogsum  27593  mulog2sumlem2  27596  log2sumbnd  27605  selberglem2  27607  selberglem3  27608  selberg  27609  selberg2lem  27611  selberg2  27612  pntrf  27624  pntrmax  27625  pntrsumo1  27626  selbergr  27629  selbergs  27635  pntrlog2bndlem4  27641  pntrlog2bndlem5  27642  pntibndlem1  27650  pntlem3  27670  pntlemp  27671  pntleml  27672  pnt2  27674  padicabvcxp  27693  vacn  30894  nmcvcn  30895  smcnlem  30897  blocnilem  31004  chscllem2  31838  nmcexi  32226  nmcopexi  32227  nmcfnexi  32251  dp2ltsuc  33060  dpval3rp  33074  dplti  33079  dpgti  33080  dpexpp1  33082  dpadd2  33084  pnfinf  33360  sqsscirc1  34202  dya2icoseg2  34572  probfinmeasb  34722  probfinmeasbALTV  34723  signshf  34879  divsqrtid  34885  logdivsqrle  34941  hgt750lem2  34943  subfacval3  35536  opnrebl  36677  opnrebl2  36678  taupilem1  37810  opnmbllem0  38152  itg2addnclem  38167  itg2addnclem2  38168  itg2addnclem3  38169  itg2addnc  38170  itg2gt0cn  38171  ftc1anclem5  38193  ftc1anclem7  38195  ftc1anc  38197  areacirclem1  38204  areacirclem4  38207  areacirc  38209  geomcau  38255  isbnd2  38279  ssbnd  38284  heiborlem7  38313  heiborlem8  38314  bfplem2  38319  rrncmslem  38328  rrnequiv  38331  dvrelog3  42679  aks4d1p1p6  42687  rpabsid  42927  irrapxlem1  43396  irrapxlem2  43397  irrapxlem3  43398  irrapxlem5  43400  2timesgt  45864  supxrge  45911  suplesup  45912  xrlexaddrp  45925  xralrple2  45927  infleinflem1  45942  xralrple4  45945  xralrple3  45946  xrralrecnnle  45955  climinf  46179  mullimc  46189  mullimcf  46196  limcrecl  46202  limcleqr  46215  addlimc  46219  0ellimcdiv  46220  limclner  46222  liminflimsupclim  46378  ioodvbdlimc1lem1  46502  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  stoweidlem7  46578  fourierdlem73  46750  fourierdlem87  46764  fourierdlem103  46780  fourierdlem104  46781  sge0iunmptlemre  46986  smflimlem4  47345  fldivexpfllog2  49184  blenre  49193  itscnhlc0yqe  49378  itscnhlc0xyqsol  49384  itschlc0xyqsol  49386  itsclc0xyqsolr  49388  itsclinecirc0in  49394  itsclquadb  49395  itscnhlinecirc02plem3  49403  itscnhlinecirc02p  49404  inlinecirc02plem  49405  inlinecirc02p  49406  amgmwlem  50420