Theorem rpre 12236

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

Syntax hints:   → wi 4   ∈ wcel 2079  ℝcr 10371  ℝ⁺crp 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rab 3112  df-in 3861  df-ss 3869  df-rp 12229

This theorem is referenced by:  rpxr  12237  rpcn  12238  rpge0  12241  rprege0  12243  rprene0  12245  rpaddcl  12250  rpmulcl  12251  rpdivcl  12253  rpgecl  12256  ledivge1le  12299  addlelt  12342  xralrple  12437  xlemul1  12522  infmrp1  12576  iccdil  12715  ltdifltdiv  13042  modcl  13079  mod0  13082  mulmod0  13083  modge0  13085  modlt  13086  modid0  13103  modabs  13110  modabs2  13111  modcyc  13112  modmuladd  13119  modmuladdnn0  13121  modltm1p1mod  13129  2txmodxeq0  13137  2submod  13138  moddi  13145  modsubdir  13146  modeqmodmin  13147  modirr  13148  rpexpmord  13370  expnlbnd  13432  rennim  14420  cnpart  14421  sqrlem1  14424  sqrlem2  14425  sqrlem4  14427  sqrlem5  14428  sqrlem6  14429  sqrlem7  14430  resqrex  14432  rpsqrtcl  14446  sqreulem  14541  eqsqrt2d  14550  2clim  14751  reccn2  14775  cn1lem  14776  climsqz  14819  climsqz2  14820  rlimsqzlem  14827  climsup  14848  climcau  14849  caucvgrlem2  14853  iseralt  14863  cvgcmp  14992  cvgcmpce  14994  divrcnv  15028  rprisefaccl  15198  efgt1  15290  ef01bndlem  15358  sinltx  15363  stdbdmet  22797  stdbdmopn  22799  met2ndci  22803  cfilucfil  22840  ngptgp  22916  reperflem  23097  iccntr  23100  reconnlem2  23106  opnreen  23110  metdseq0  23133  xlebnum  23240  cphsqrtcl3  23462  iscmet3lem3  23564  iscmet3lem1  23565  iscmet3lem2  23566  caubl  23582  lmcau  23587  bcthlem4  23601  minveclem3b  23702  minveclem3  23703  ivthlem2  23724  ivthlem3  23725  nulmbl2  23808  opnmbllem  23873  itg2const2  24013  itg2mulclem  24018  dveflem  24247  lhop  24284  dvcnvre  24287  aalioulem2  24593  aaliou  24598  aaliou3lem4  24606  ulmcaulem  24653  ulmcau  24654  ulmcn  24658  itgulm  24667  reeff1o  24706  pilem2  24711  logleb  24855  logcj  24858  argimgt0  24864  logdmnrp  24893  logcnlem3  24896  logcnlem4  24897  advlog  24906  efopnlem1  24908  cxple2  24949  cxplt2  24950  cxple3  24953  2irrexpq  24982  cxpcn3  24998  resqrtcn  24999  relogbf  25038  asinneg  25133  atanbndlem  25172  cxplim  25219  cxp2limlem  25223  cxp2lim  25224  cxploglim  25225  cxploglim2  25226  logdiflbnd  25242  harmoniclbnd  25256  harmonicbnd4  25258  chtrpcl  25422  ppiltx  25424  chtleppi  25456  logfacubnd  25467  logfaclbnd  25468  logfacbnd3  25469  logexprlim  25471  bposlem7  25536  bposlem8  25537  bposlem9  25538  chebbnd1  25718  chtppilim  25721  chto1ub  25722  chpo1ub  25726  vmadivsum  25728  rpvmasumlem  25733  dchrisumlem3  25737  dchrvmasumlem2  25744  dchrvmasumiflem1  25747  dchrisum0  25766  mudivsum  25776  mulogsumlem  25777  mulogsum  25778  mulog2sumlem2  25781  log2sumbnd  25790  selberglem2  25792  selberglem3  25793  selberg  25794  selberg2lem  25796  selberg2  25797  pntrf  25809  pntrmax  25810  pntrsumo1  25811  selbergr  25814  selbergs  25820  pntrlog2bndlem4  25826  pntrlog2bndlem5  25827  pntibndlem1  25835  pntlem3  25855  pntlemp  25856  pntleml  25857  pnt2  25859  padicabvcxp  25878  vacn  28150  nmcvcn  28151  smcnlem  28153  blocnilem  28260  chscllem2  29094  nmcexi  29482  nmcopexi  29483  nmcfnexi  29507  dp2ltsuc  30217  dpval3rp  30231  dplti  30236  dpgti  30237  dpexpp1  30239  dpadd2  30241  pnfinf  30408  sqsscirc1  30724  dya2icoseg2  31109  probfinmeasb  31259  probfinmeasbALTV  31260  divsqrtid  31438  logdivsqrle  31494  hgt750lem2  31496  subfacval3  32000  opnrebl  33222  opnrebl2  33223  taupilem1  34079  opnmbllem0  34405  itg2addnclem  34420  itg2addnclem2  34421  itg2addnclem3  34422  itg2addnc  34423  itg2gt0cn  34424  ftc1anclem5  34448  ftc1anclem7  34450  ftc1anc  34452  areacirclem1  34459  areacirclem4  34462  areacirc  34464  geomcau  34512  isbnd2  34539  ssbnd  34544  heiborlem7  34573  heiborlem8  34574  bfplem2  34579  rrncmslem  34588  rrnequiv  34591  irrapxlem1  38855  irrapxlem2  38856  irrapxlem3  38857  irrapxlem5  38859  neglt  41044  2timesgt  41048  supxrge  41100  suplesup  41101  xrlexaddrp  41114  xralrple2  41116  infleinflem1  41132  xralrple4  41135  xralrple3  41136  xrralrecnnle  41148  climinf  41383  mullimc  41393  mullimcf  41400  limcrecl  41406  limcleqr  41421  addlimc  41425  0ellimcdiv  41426  limclner  41428  liminflimsupclim  41584  ioodvbdlimc1lem1  41711  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  stoweidlem7  41788  fourierdlem73  41960  fourierdlem87  41974  fourierdlem103  41990  fourierdlem104  41991  sge0iunmptlemre  42193  smflimlem4  42546  fldivexpfllog2  44060  blenre  44069  itscnhlc0yqe  44181  itscnhlc0xyqsol  44187  itschlc0xyqsol  44189  itsclc0xyqsolr  44191  itsclinecirc0in  44197  itsclquadb  44198  itscnhlinecirc02plem3  44206  itscnhlinecirc02p  44207  inlinecirc02plem  44208  inlinecirc02p  44209  amgmwlem  44337