Theorem rpre 13169

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11238  ℝ⁺crp 13160

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-rp 13161

This theorem is used by:  rpxr  13170  rpcn  13171  rpge0  13174  rprege0  13176  rprene0  13178  neglt  13180  rpaddcl  13184  rpmulcl  13185  rpdivcl  13187  rpgecl  13190  ledivge1le  13233  addlelt  13276  xralrple  13375  xlemul1  13460  infmrp1  13515  iccdil  13661  ltdifltdiv  14014  modcl  14053  mod0  14056  mulmod0  14057  modge0  14059  modlt  14060  modid0  14077  modabs  14084  modabs2  14085  modcyc  14086  muladdmod  14095  modmuladd  14096  modmuladdnn0  14098  modltm1p1mod  14106  2txmodxeq0  14114  2submod  14115  moddi  14122  modsubdir  14123  modeqmodmin  14124  modirr  14125  rpexpmord  14351  expnlbnd  14418  rennim  15449  cnpart  15450  01sqrexlem1  15452  01sqrexlem2  15453  01sqrexlem4  15455  01sqrexlem5  15456  01sqrexlem6  15457  01sqrexlem7  15458  resqrex  15460  rpsqrtcl  15474  sqreulem  15571  eqsqrt2d  15580  2clim  15783  reccn2  15808  cn1lem  15809  climsqz  15852  climsqz2  15853  rlimsqzlem  15860  climsup  15881  climcau  15882  caucvgrlem2  15886  iseralt  15896  cvgcmp  16027  cvgcmpce  16029  divrcnv  16065  rprisefaccl  16234  efgt1  16328  ef01bndlem  16396  sinltx  16401  stdbdmet  24890  stdbdmopn  24892  met2ndci  24896  cfilucfil  24933  ngptgp  25010  reperflem  25193  iccntr  25196  reconnlem2  25202  opnreen  25206  metdseq0  25229  xlebnum  25341  cphsqrtcl3  25563  iscmet3lem3  25666  iscmet3lem1  25667  iscmet3lem2  25668  caubl  25684  lmcau  25689  bcthlem4  25703  minveclem3b  25804  minveclem3  25805  ivthlem2  25828  ivthlem3  25829  nulmbl2  25912  opnmbllem  25977  itg2const2  26117  itg2mulclem  26122  dveflem  26354  lhop  26391  dvcnvre  26394  aalioulem2  26717  aaliou  26722  aaliou3lem4  26730  ulmcaulem  26778  ulmcau  26779  ulmcn  26783  itgulm  26792  reeff1o  26831  pilem2  26836  logleb  26988  logcj  26991  argimgt0  26997  logdmnrp  27026  logcnlem3  27029  logcnlem4  27030  advlog  27039  efopnlem1  27041  cxple2  27082  cxplt2  27083  cxple3  27086  2irrexpq  27116  cxpcn3  27133  resqrtcn  27134  relogbf  27176  asinneg  27271  atanbndlem  27310  cxplim  27356  cxp2limlem  27360  cxp2lim  27361  cxploglim  27362  cxploglim2  27363  logdiflbnd  27379  harmoniclbnd  27393  harmonicbnd4  27395  chtrpcl  27559  ppiltx  27561  chtleppi  27594  logfacubnd  27605  logfaclbnd  27606  logfacbnd3  27607  logexprlim  27609  bposlem7  27674  bposlem8  27675  bposlem9  27676  chebbnd1  27856  chtppilim  27859  chto1ub  27860  chpo1ub  27864  vmadivsum  27866  rpvmasumlem  27871  dchrisumlem3  27875  dchrvmasumlem2  27882  dchrvmasumiflem1  27885  dchrisum0  27904  mudivsum  27914  mulogsumlem  27915  mulogsum  27916  mulog2sumlem2  27919  log2sumbnd  27928  selberglem2  27930  selberglem3  27931  selberg  27932  selberg2lem  27934  selberg2  27935  pntrf  27947  pntrmax  27948  pntrsumo1  27949  selbergr  27952  selbergs  27958  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntibndlem1  27973  pntlem3  27993  pntlemp  27994  pntleml  27995  pnt2  27997  padicabvcxp  28016  vacn  31353  nmcvcn  31354  smcnlem  31356  blocnilem  31463  chscllem2  32297  nmcexi  32685  nmcopexi  32686  nmcfnexi  32710  dp2ltsuc  33548  dpval3rp  33562  dplti  33567  dpgti  33568  dpexpp1  33570  dpadd2  33572  pnfinf  33843  sqsscirc1  34651  dya2icoseg2  35021  probfinmeasb  35171  probfinmeasbALTV  35172  signshf  35328  divsqrtid  35334  logdivsqrle  35390  hgt750lem2  35392  subfacval3  36162  opnrebl  37323  opnrebl2  37324  taupilem1  38510  opnmbllem0  38842  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  itg2addnc  38860  itg2gt0cn  38861  ftc1anclem5  38883  ftc1anclem7  38885  ftc1anc  38887  areacirclem1  38894  areacirclem4  38897  areacirc  38899  geomcau  38959  isbnd2  38983  ssbnd  38988  heiborlem7  39017  heiborlem8  39018  bfplem2  39023  rrncmslem  39032  rrnequiv  39035  dvrelog3  43381  aks4d1p1p6  43389  rpabsid  43644  irrapxlem1  44095  irrapxlem2  44096  irrapxlem3  44097  irrapxlem5  44099  2timesgt  46577  supxrge  46623  suplesup  46624  xrlexaddrp  46637  xralrple2  46639  infleinflem1  46654  xralrple4  46657  xralrple3  46658  xrralrecnnle  46667  climinf  46891  mullimc  46901  mullimcf  46908  limcrecl  46914  limcleqr  46927  addlimc  46931  0ellimcdiv  46932  limclner  46934  liminflimsupclim  47090  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweidlem7  47290  fourierdlem73  47462  fourierdlem87  47476  fourierdlem103  47492  fourierdlem104  47493  sge0iunmptlemre  47698  smflimlem4  48057  fldivexpfllog2  50008  blenre  50017  itscnhlc0yqe  50202  itscnhlc0xyqsol  50208  itschlc0xyqsol  50210  itsclc0xyqsolr  50212  itsclinecirc0in  50218  itsclquadb  50219  itscnhlinecirc02plem3  50227  itscnhlinecirc02p  50228  inlinecirc02plem  50229  inlinecirc02p  50230  amgmwlem  51415