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 3965	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10538  ℝ⁺crp 12392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-in 3945  df-ss 3954  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  14600  cnpart  14601  sqrlem1  14604  sqrlem2  14605  sqrlem4  14607  sqrlem5  14608  sqrlem6  14609  sqrlem7  14610  resqrex  14612  rpsqrtcl  14626  sqreulem  14721  eqsqrt2d  14730  2clim  14931  reccn2  14955  cn1lem  14956  climsqz  14999  climsqz2  15000  rlimsqzlem  15007  climsup  15028  climcau  15029  caucvgrlem2  15033  iseralt  15043  cvgcmp  15173  cvgcmpce  15175  divrcnv  15209  rprisefaccl  15379  efgt1  15471  ef01bndlem  15539  sinltx  15544  stdbdmet  23128  stdbdmopn  23130  met2ndci  23134  cfilucfil  23171  ngptgp  23247  reperflem  23428  iccntr  23431  reconnlem2  23437  opnreen  23441  metdseq0  23464  xlebnum  23571  cphsqrtcl3  23793  iscmet3lem3  23895  iscmet3lem1  23896  iscmet3lem2  23897  caubl  23913  lmcau  23918  bcthlem4  23932  minveclem3b  24033  minveclem3  24034  ivthlem2  24055  ivthlem3  24056  nulmbl2  24139  opnmbllem  24204  itg2const2  24344  itg2mulclem  24349  dveflem  24578  lhop  24615  dvcnvre  24618  aalioulem2  24924  aaliou  24929  aaliou3lem4  24937  ulmcaulem  24984  ulmcau  24985  ulmcn  24989  itgulm  24998  reeff1o  25037  pilem2  25042  logleb  25188  logcj  25191  argimgt0  25197  logdmnrp  25226  logcnlem3  25229  logcnlem4  25230  advlog  25239  efopnlem1  25241  cxple2  25282  cxplt2  25283  cxple3  25286  2irrexpq  25315  cxpcn3  25331  resqrtcn  25332  relogbf  25371  asinneg  25466  atanbndlem  25505  cxplim  25551  cxp2limlem  25555  cxp2lim  25556  cxploglim  25557  cxploglim2  25558  logdiflbnd  25574  harmoniclbnd  25588  harmonicbnd4  25590  chtrpcl  25754  ppiltx  25756  chtleppi  25788  logfacubnd  25799  logfaclbnd  25800  logfacbnd3  25801  logexprlim  25803  bposlem7  25868  bposlem8  25869  bposlem9  25870  chebbnd1  26050  chtppilim  26053  chto1ub  26054  chpo1ub  26058  vmadivsum  26060  rpvmasumlem  26065  dchrisumlem3  26069  dchrvmasumlem2  26076  dchrvmasumiflem1  26079  dchrisum0  26098  mudivsum  26108  mulogsumlem  26109  mulogsum  26110  mulog2sumlem2  26113  log2sumbnd  26122  selberglem2  26124  selberglem3  26125  selberg  26126  selberg2lem  26128  selberg2  26129  pntrf  26141  pntrmax  26142  pntrsumo1  26143  selbergr  26146  selbergs  26152  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  pntibndlem1  26167  pntlem3  26187  pntlemp  26188  pntleml  26189  pnt2  26191  padicabvcxp  26210  vacn  28473  nmcvcn  28474  smcnlem  28476  blocnilem  28583  chscllem2  29417  nmcexi  29805  nmcopexi  29806  nmcfnexi  29830  dp2ltsuc  30564  dpval3rp  30578  dplti  30583  dpgti  30584  dpexpp1  30586  dpadd2  30588  pnfinf  30814  sqsscirc1  31153  dya2icoseg2  31538  probfinmeasb  31688  probfinmeasbALTV  31689  signshf  31860  divsqrtid  31867  logdivsqrle  31923  hgt750lem2  31925  subfacval3  32438  opnrebl  33670  opnrebl2  33671  taupilem1  34604  opnmbllem0  34930  itg2addnclem  34945  itg2addnclem2  34946  itg2addnclem3  34947  itg2addnc  34948  itg2gt0cn  34949  ftc1anclem5  34973  ftc1anclem7  34975  ftc1anc  34977  areacirclem1  34984  areacirclem4  34987  areacirc  34989  geomcau  35036  isbnd2  35063  ssbnd  35068  heiborlem7  35097  heiborlem8  35098  bfplem2  35103  rrncmslem  35112  rrnequiv  35115  irrapxlem1  39426  irrapxlem2  39427  irrapxlem3  39428  irrapxlem5  39430  neglt  41557  2timesgt  41561  supxrge  41613  suplesup  41614  xrlexaddrp  41627  xralrple2  41629  infleinflem1  41645  xralrple4  41648  xralrple3  41649  xrralrecnnle  41660  climinf  41894  mullimc  41904  mullimcf  41911  limcrecl  41917  limcleqr  41932  addlimc  41936  0ellimcdiv  41937  limclner  41939  liminflimsupclim  42095  ioodvbdlimc1lem1  42223  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  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