Theorem rpre 12902

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11008  ℝ⁺crp 12893

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-ss 3920  df-rp 12894

This theorem is referenced by:  rpxr  12903  rpcn  12904  rpge0  12907  rprege0  12909  rprene0  12911  neglt  12913  rpaddcl  12917  rpmulcl  12918  rpdivcl  12920  rpgecl  12923  ledivge1le  12966  addlelt  13009  xralrple  13107  xlemul1  13192  infmrp1  13247  iccdil  13393  ltdifltdiv  13738  modcl  13777  mod0  13780  mulmod0  13781  modge0  13783  modlt  13784  modid0  13801  modabs  13808  modabs2  13809  modcyc  13810  muladdmod  13819  modmuladd  13820  modmuladdnn0  13822  modltm1p1mod  13830  2txmodxeq0  13838  2submod  13839  moddi  13846  modsubdir  13847  modeqmodmin  13848  modirr  13849  rpexpmord  14075  expnlbnd  14140  rennim  15146  cnpart  15147  01sqrexlem1  15149  01sqrexlem2  15150  01sqrexlem4  15152  01sqrexlem5  15153  01sqrexlem6  15154  01sqrexlem7  15155  resqrex  15157  rpsqrtcl  15171  sqreulem  15267  eqsqrt2d  15276  2clim  15479  reccn2  15504  cn1lem  15505  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  climsup  15577  climcau  15578  caucvgrlem2  15582  iseralt  15592  cvgcmp  15723  cvgcmpce  15725  divrcnv  15759  rprisefaccl  15930  efgt1  16025  ef01bndlem  16093  sinltx  16098  stdbdmet  24402  stdbdmopn  24404  met2ndci  24408  cfilucfil  24445  ngptgp  24522  reperflem  24705  iccntr  24708  reconnlem2  24714  opnreen  24718  metdseq0  24741  xlebnum  24862  cphsqrtcl3  25085  iscmet3lem3  25188  iscmet3lem1  25189  iscmet3lem2  25190  caubl  25206  lmcau  25211  bcthlem4  25225  minveclem3b  25326  minveclem3  25327  ivthlem2  25351  ivthlem3  25352  nulmbl2  25435  opnmbllem  25500  itg2const2  25640  itg2mulclem  25645  dveflem  25881  lhop  25919  dvcnvre  25922  aalioulem2  26239  aaliou  26244  aaliou3lem4  26252  ulmcaulem  26301  ulmcau  26302  ulmcn  26306  itgulm  26315  reeff1o  26355  pilem2  26360  logleb  26510  logcj  26513  argimgt0  26519  logdmnrp  26548  logcnlem3  26551  logcnlem4  26552  advlog  26561  efopnlem1  26563  cxple2  26604  cxplt2  26605  cxple3  26608  2irrexpq  26638  cxpcn3  26656  resqrtcn  26657  relogbf  26699  asinneg  26794  atanbndlem  26833  cxplim  26880  cxp2limlem  26884  cxp2lim  26885  cxploglim  26886  cxploglim2  26887  logdiflbnd  26903  harmoniclbnd  26917  harmonicbnd4  26919  chtrpcl  27083  ppiltx  27085  chtleppi  27119  logfacubnd  27130  logfaclbnd  27131  logfacbnd3  27132  logexprlim  27134  bposlem7  27199  bposlem8  27200  bposlem9  27201  chebbnd1  27381  chtppilim  27384  chto1ub  27385  chpo1ub  27389  vmadivsum  27391  rpvmasumlem  27396  dchrisumlem3  27400  dchrvmasumlem2  27407  dchrvmasumiflem1  27410  dchrisum0  27429  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem2  27444  log2sumbnd  27453  selberglem2  27455  selberglem3  27456  selberg  27457  selberg2lem  27459  selberg2  27460  pntrf  27472  pntrmax  27473  pntrsumo1  27474  selbergr  27477  selbergs  27483  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntibndlem1  27498  pntlem3  27518  pntlemp  27519  pntleml  27520  pnt2  27522  padicabvcxp  27541  vacn  30638  nmcvcn  30639  smcnlem  30641  blocnilem  30748  chscllem2  31582  nmcexi  31970  nmcopexi  31971  nmcfnexi  31995  dp2ltsuc  32826  dpval3rp  32840  dplti  32845  dpgti  32846  dpexpp1  32848  dpadd2  32850  pnfinf  33125  sqsscirc1  33875  dya2icoseg2  34246  probfinmeasb  34396  probfinmeasbALTV  34397  signshf  34556  divsqrtid  34562  logdivsqrle  34618  hgt750lem2  34620  subfacval3  35162  opnrebl  36294  opnrebl2  36295  taupilem1  37295  opnmbllem0  37636  itg2addnclem  37651  itg2addnclem2  37652  itg2addnclem3  37653  itg2addnc  37654  itg2gt0cn  37655  ftc1anclem5  37677  ftc1anclem7  37679  ftc1anc  37681  areacirclem1  37688  areacirclem4  37691  areacirc  37693  geomcau  37739  isbnd2  37763  ssbnd  37768  heiborlem7  37797  heiborlem8  37798  bfplem2  37803  rrncmslem  37812  rrnequiv  37815  dvrelog3  42038  aks4d1p1p6  42046  rpabsid  42294  irrapxlem1  42795  irrapxlem2  42796  irrapxlem3  42797  irrapxlem5  42799  2timesgt  45270  supxrge  45318  suplesup  45319  xrlexaddrp  45332  xralrple2  45334  infleinflem1  45349  xralrple4  45352  xralrple3  45353  xrralrecnnle  45362  climinf  45587  mullimc  45597  mullimcf  45604  limcrecl  45610  limcleqr  45625  addlimc  45629  0ellimcdiv  45630  limclner  45632  liminflimsupclim  45788  ioodvbdlimc1lem1  45912  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  stoweidlem7  45988  fourierdlem73  46160  fourierdlem87  46174  fourierdlem103  46190  fourierdlem104  46191  sge0iunmptlemre  46396  smflimlem4  46755  fldivexpfllog2  48550  blenre  48559  itscnhlc0yqe  48744  itscnhlc0xyqsol  48750  itschlc0xyqsol  48752  itsclc0xyqsolr  48754  itsclinecirc0in  48760  itsclquadb  48761  itscnhlinecirc02plem3  48769  itscnhlinecirc02p  48770  inlinecirc02plem  48771  inlinecirc02p  48772  amgmwlem  49787