Theorem rpre 13122

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11192  ℝ⁺crp 13113

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-rp 13114

This theorem is used by:  rpxr  13123  rpcn  13124  rpge0  13127  rprege0  13129  rprene0  13131  neglt  13133  rpaddcl  13137  rpmulcl  13138  rpdivcl  13140  rpgecl  13143  ledivge1le  13186  addlelt  13229  xralrple  13328  xlemul1  13413  infmrp1  13468  iccdil  13614  ltdifltdiv  13967  modcl  14006  mod0  14009  mulmod0  14010  modge0  14012  modlt  14013  modid0  14030  modabs  14037  modabs2  14038  modcyc  14039  muladdmod  14048  modmuladd  14049  modmuladdnn0  14051  modltm1p1mod  14059  2txmodxeq0  14067  2submod  14068  moddi  14075  modsubdir  14076  modeqmodmin  14077  modirr  14078  rpexpmord  14304  expnlbnd  14370  rennim  15399  cnpart  15400  01sqrexlem1  15402  01sqrexlem2  15403  01sqrexlem4  15405  01sqrexlem5  15406  01sqrexlem6  15407  01sqrexlem7  15408  resqrex  15410  rpsqrtcl  15424  sqreulem  15520  eqsqrt2d  15529  2clim  15732  reccn2  15757  cn1lem  15758  climsqz  15801  climsqz2  15802  rlimsqzlem  15809  climsup  15830  climcau  15831  caucvgrlem2  15835  iseralt  15845  cvgcmp  15976  cvgcmpce  15978  divrcnv  16014  rprisefaccl  16183  efgt1  16277  ef01bndlem  16345  sinltx  16350  stdbdmet  24828  stdbdmopn  24830  met2ndci  24834  cfilucfil  24871  ngptgp  24948  reperflem  25131  iccntr  25134  reconnlem2  25140  opnreen  25144  metdseq0  25167  xlebnum  25279  cphsqrtcl3  25501  iscmet3lem3  25604  iscmet3lem1  25605  iscmet3lem2  25606  caubl  25622  lmcau  25627  bcthlem4  25641  minveclem3b  25742  minveclem3  25743  ivthlem2  25766  ivthlem3  25767  nulmbl2  25850  opnmbllem  25915  itg2const2  26055  itg2mulclem  26060  dveflem  26292  lhop  26329  dvcnvre  26332  aalioulem2  26653  aaliou  26658  aaliou3lem4  26666  ulmcaulem  26714  ulmcau  26715  ulmcn  26719  itgulm  26728  reeff1o  26767  pilem2  26772  logleb  26924  logcj  26927  argimgt0  26933  logdmnrp  26962  logcnlem3  26965  logcnlem4  26966  advlog  26975  efopnlem1  26977  cxple2  27018  cxplt2  27019  cxple3  27022  2irrexpq  27052  cxpcn3  27069  resqrtcn  27070  relogbf  27112  asinneg  27207  atanbndlem  27246  cxplim  27292  cxp2limlem  27296  cxp2lim  27297  cxploglim  27298  cxploglim2  27299  logdiflbnd  27315  harmoniclbnd  27329  harmonicbnd4  27331  chtrpcl  27495  ppiltx  27497  chtleppi  27530  logfacubnd  27541  logfaclbnd  27542  logfacbnd3  27543  logexprlim  27545  bposlem7  27610  bposlem8  27611  bposlem9  27612  chebbnd1  27792  chtppilim  27795  chto1ub  27796  chpo1ub  27800  vmadivsum  27802  rpvmasumlem  27807  dchrisumlem3  27811  dchrvmasumlem2  27818  dchrvmasumiflem1  27821  dchrisum0  27840  mudivsum  27850  mulogsumlem  27851  mulogsum  27852  mulog2sumlem2  27855  log2sumbnd  27864  selberglem2  27866  selberglem3  27867  selberg  27868  selberg2lem  27870  selberg2  27871  pntrf  27883  pntrmax  27884  pntrsumo1  27885  selbergr  27888  selbergs  27894  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntibndlem1  27909  pntlem3  27929  pntlemp  27930  pntleml  27931  pnt2  27933  padicabvcxp  27952  vacn  31289  nmcvcn  31290  smcnlem  31292  blocnilem  31399  chscllem2  32233  nmcexi  32621  nmcopexi  32622  nmcfnexi  32646  dp2ltsuc  33445  dpval3rp  33459  dplti  33464  dpgti  33465  dpexpp1  33467  dpadd2  33469  pnfinf  33737  sqsscirc1  34533  dya2icoseg2  34903  probfinmeasb  35053  probfinmeasbALTV  35054  signshf  35210  divsqrtid  35216  logdivsqrle  35272  hgt750lem2  35274  subfacval3  35933  opnrebl  37088  opnrebl2  37089  taupilem1  38222  opnmbllem0  38554  itg2addnclem  38569  itg2addnclem2  38570  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  ftc1anclem5  38595  ftc1anclem7  38597  ftc1anc  38599  areacirclem1  38606  areacirclem4  38609  areacirc  38611  geomcau  38673  isbnd2  38697  ssbnd  38702  heiborlem7  38731  heiborlem8  38732  bfplem2  38737  rrncmslem  38746  rrnequiv  38749  dvrelog3  43095  aks4d1p1p6  43103  rpabsid  43358  irrapxlem1  43808  irrapxlem2  43809  irrapxlem3  43810  irrapxlem5  43812  2timesgt  46273  supxrge  46319  suplesup  46320  xrlexaddrp  46333  xralrple2  46335  infleinflem1  46350  xralrple4  46353  xralrple3  46354  xrralrecnnle  46363  climinf  46587  mullimc  46597  mullimcf  46604  limcrecl  46610  limcleqr  46623  addlimc  46627  0ellimcdiv  46628  limclner  46630  liminflimsupclim  46786  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweidlem7  46986  fourierdlem73  47158  fourierdlem87  47172  fourierdlem103  47188  fourierdlem104  47189  sge0iunmptlemre  47394  smflimlem4  47753  fldivexpfllog2  49646  blenre  49655  itscnhlc0yqe  49840  itscnhlc0xyqsol  49846  itschlc0xyqsol  49848  itsclc0xyqsolr  49850  itsclinecirc0in  49856  itsclquadb  49857  itscnhlinecirc02plem3  49865  itscnhlinecirc02p  49866  inlinecirc02plem  49867  inlinecirc02p  49868  amgmwlem  50956