Theorem rpre 12400

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 10539  ℝ⁺crp 12392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-in 3946  df-ss 3955  df-rp 12393

This theorem is referenced by:  rpxr  12401  rpcn  12402  rpge0  12405  rprege0  12407  rprene0  12409  rpaddcl  12414  rpmulcl  12415  rpdivcl  12417  rpgecl  12420  ledivge1le  12463  addlelt  12506  xralrple  12601  xlemul1  12686  infmrp1  12740  iccdil  12879  ltdifltdiv  13207  modcl  13244  mod0  13247  mulmod0  13248  modge0  13250  modlt  13251  modid0  13268  modabs  13275  modabs2  13276  modcyc  13277  modmuladd  13284  modmuladdnn0  13286  modltm1p1mod  13294  2txmodxeq0  13302  2submod  13303  moddi  13310  modsubdir  13311  modeqmodmin  13312  modirr  13313  rpexpmord  13535  expnlbnd  13597  rennim  14601  cnpart  14602  sqrlem1  14605  sqrlem2  14606  sqrlem4  14608  sqrlem5  14609  sqrlem6  14610  sqrlem7  14611  resqrex  14613  rpsqrtcl  14627  sqreulem  14722  eqsqrt2d  14731  2clim  14932  reccn2  14956  cn1lem  14957  climsqz  15000  climsqz2  15001  rlimsqzlem  15008  climsup  15029  climcau  15030  caucvgrlem2  15034  iseralt  15044  cvgcmp  15174  cvgcmpce  15176  divrcnv  15210  rprisefaccl  15380  efgt1  15472  ef01bndlem  15540  sinltx  15545  stdbdmet  23129  stdbdmopn  23131  met2ndci  23135  cfilucfil  23172  ngptgp  23248  reperflem  23429  iccntr  23432  reconnlem2  23438  opnreen  23442  metdseq0  23465  xlebnum  23572  cphsqrtcl3  23794  iscmet3lem3  23896  iscmet3lem1  23897  iscmet3lem2  23898  caubl  23914  lmcau  23919  bcthlem4  23933  minveclem3b  24034  minveclem3  24035  ivthlem2  24056  ivthlem3  24057  nulmbl2  24140  opnmbllem  24205  itg2const2  24345  itg2mulclem  24350  dveflem  24579  lhop  24616  dvcnvre  24619  aalioulem2  24925  aaliou  24930  aaliou3lem4  24938  ulmcaulem  24985  ulmcau  24986  ulmcn  24990  itgulm  24999  reeff1o  25038  pilem2  25043  logleb  25189  logcj  25192  argimgt0  25198  logdmnrp  25227  logcnlem3  25230  logcnlem4  25231  advlog  25240  efopnlem1  25242  cxple2  25283  cxplt2  25284  cxple3  25287  2irrexpq  25316  cxpcn3  25332  resqrtcn  25333  relogbf  25372  asinneg  25467  atanbndlem  25506  cxplim  25552  cxp2limlem  25556  cxp2lim  25557  cxploglim  25558  cxploglim2  25559  logdiflbnd  25575  harmoniclbnd  25589  harmonicbnd4  25591  chtrpcl  25755  ppiltx  25757  chtleppi  25789  logfacubnd  25800  logfaclbnd  25801  logfacbnd3  25802  logexprlim  25804  bposlem7  25869  bposlem8  25870  bposlem9  25871  chebbnd1  26051  chtppilim  26054  chto1ub  26055  chpo1ub  26059  vmadivsum  26061  rpvmasumlem  26066  dchrisumlem3  26070  dchrvmasumlem2  26077  dchrvmasumiflem1  26080  dchrisum0  26099  mudivsum  26109  mulogsumlem  26110  mulogsum  26111  mulog2sumlem2  26114  log2sumbnd  26123  selberglem2  26125  selberglem3  26126  selberg  26127  selberg2lem  26129  selberg2  26130  pntrf  26142  pntrmax  26143  pntrsumo1  26144  selbergr  26147  selbergs  26153  pntrlog2bndlem4  26159  pntrlog2bndlem5  26160  pntibndlem1  26168  pntlem3  26188  pntlemp  26189  pntleml  26190  pnt2  26192  padicabvcxp  26211  vacn  28474  nmcvcn  28475  smcnlem  28477  blocnilem  28584  chscllem2  29418  nmcexi  29806  nmcopexi  29807  nmcfnexi  29831  dp2ltsuc  30566  dpval3rp  30580  dplti  30585  dpgti  30586  dpexpp1  30588  dpadd2  30590  pnfinf  30816  sqsscirc1  31155  dya2icoseg2  31540  probfinmeasb  31690  probfinmeasbALTV  31691  signshf  31862  divsqrtid  31869  logdivsqrle  31925  hgt750lem2  31927  subfacval3  32440  opnrebl  33672  opnrebl2  33673  taupilem1  34606  opnmbllem0  34932  itg2addnclem  34947  itg2addnclem2  34948  itg2addnclem3  34949  itg2addnc  34950  itg2gt0cn  34951  ftc1anclem5  34975  ftc1anclem7  34977  ftc1anc  34979  areacirclem1  34986  areacirclem4  34989  areacirc  34991  geomcau  35038  isbnd2  35065  ssbnd  35070  heiborlem7  35099  heiborlem8  35100  bfplem2  35105  rrncmslem  35114  rrnequiv  35117  irrapxlem1  39425  irrapxlem2  39426  irrapxlem3  39427  irrapxlem5  39429  neglt  41556  2timesgt  41560  supxrge  41612  suplesup  41613  xrlexaddrp  41626  xralrple2  41628  infleinflem1  41644  xralrple4  41647  xralrple3  41648  xrralrecnnle  41659  climinf  41893  mullimc  41903  mullimcf  41910  limcrecl  41916  limcleqr  41931  addlimc  41935  0ellimcdiv  41936  limclner  41938  liminflimsupclim  42094  ioodvbdlimc1lem1  42222  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  stoweidlem7  42299  fourierdlem73  42471  fourierdlem87  42485  fourierdlem103  42501  fourierdlem104  42502  sge0iunmptlemre  42704  smflimlem4  43057  fldivexpfllog2  44632  blenre  44641  itscnhlc0yqe  44753  itscnhlc0xyqsol  44759  itschlc0xyqsol  44761  itsclc0xyqsolr  44763  itsclinecirc0in  44769  itsclquadb  44770  itscnhlinecirc02plem3  44778  itscnhlinecirc02p  44779  inlinecirc02plem  44780  inlinecirc02p  44781  amgmwlem  44910