Theorem rpre 12747

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  ℝ⁺crp 12739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905  df-rp 12740

This theorem is referenced by:  rpxr  12748  rpcn  12749  rpge0  12752  rprege0  12754  rprene0  12756  rpaddcl  12761  rpmulcl  12762  rpdivcl  12764  rpgecl  12767  ledivge1le  12810  addlelt  12853  xralrple  12948  xlemul1  13033  infmrp1  13087  iccdil  13231  ltdifltdiv  13563  modcl  13602  mod0  13605  mulmod0  13606  modge0  13608  modlt  13609  modid0  13626  modabs  13633  modabs2  13634  modcyc  13635  modmuladd  13642  modmuladdnn0  13644  modltm1p1mod  13652  2txmodxeq0  13660  2submod  13661  moddi  13668  modsubdir  13669  modeqmodmin  13670  modirr  13671  rpexpmord  13895  expnlbnd  13957  rennim  14959  cnpart  14960  sqrlem1  14963  sqrlem2  14964  sqrlem4  14966  sqrlem5  14967  sqrlem6  14968  sqrlem7  14969  resqrex  14971  rpsqrtcl  14985  sqreulem  15080  eqsqrt2d  15089  2clim  15290  reccn2  15315  cn1lem  15316  climsqz  15359  climsqz2  15360  rlimsqzlem  15369  climsup  15390  climcau  15391  caucvgrlem2  15395  iseralt  15405  cvgcmp  15537  cvgcmpce  15539  divrcnv  15573  rprisefaccl  15742  efgt1  15834  ef01bndlem  15902  sinltx  15907  stdbdmet  23681  stdbdmopn  23683  met2ndci  23687  cfilucfil  23724  ngptgp  23801  reperflem  23990  iccntr  23993  reconnlem2  23999  opnreen  24003  metdseq0  24026  xlebnum  24137  cphsqrtcl3  24360  iscmet3lem3  24463  iscmet3lem1  24464  iscmet3lem2  24465  caubl  24481  lmcau  24486  bcthlem4  24500  minveclem3b  24601  minveclem3  24602  ivthlem2  24625  ivthlem3  24626  nulmbl2  24709  opnmbllem  24774  itg2const2  24915  itg2mulclem  24920  dveflem  25152  lhop  25189  dvcnvre  25192  aalioulem2  25502  aaliou  25507  aaliou3lem4  25515  ulmcaulem  25562  ulmcau  25563  ulmcn  25567  itgulm  25576  reeff1o  25615  pilem2  25620  logleb  25767  logcj  25770  argimgt0  25776  logdmnrp  25805  logcnlem3  25808  logcnlem4  25809  advlog  25818  efopnlem1  25820  cxple2  25861  cxplt2  25862  cxple3  25865  2irrexpq  25894  cxpcn3  25910  resqrtcn  25911  relogbf  25950  asinneg  26045  atanbndlem  26084  cxplim  26130  cxp2limlem  26134  cxp2lim  26135  cxploglim  26136  cxploglim2  26137  logdiflbnd  26153  harmoniclbnd  26167  harmonicbnd4  26169  chtrpcl  26333  ppiltx  26335  chtleppi  26367  logfacubnd  26378  logfaclbnd  26379  logfacbnd3  26380  logexprlim  26382  bposlem7  26447  bposlem8  26448  bposlem9  26449  chebbnd1  26629  chtppilim  26632  chto1ub  26633  chpo1ub  26637  vmadivsum  26639  rpvmasumlem  26644  dchrisumlem3  26648  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrisum0  26677  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  mulog2sumlem2  26692  log2sumbnd  26701  selberglem2  26703  selberglem3  26704  selberg  26705  selberg2lem  26707  selberg2  26708  pntrf  26720  pntrmax  26721  pntrsumo1  26722  selbergr  26725  selbergs  26731  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntibndlem1  26746  pntlem3  26766  pntlemp  26767  pntleml  26768  pnt2  26770  padicabvcxp  26789  vacn  29065  nmcvcn  29066  smcnlem  29068  blocnilem  29175  chscllem2  30009  nmcexi  30397  nmcopexi  30398  nmcfnexi  30422  dp2ltsuc  31169  dpval3rp  31183  dplti  31188  dpgti  31189  dpexpp1  31191  dpadd2  31193  pnfinf  31446  sqsscirc1  31867  dya2icoseg2  32254  probfinmeasb  32404  probfinmeasbALTV  32405  signshf  32576  divsqrtid  32583  logdivsqrle  32639  hgt750lem2  32641  subfacval3  33160  opnrebl  34518  opnrebl2  34519  taupilem1  35501  opnmbllem0  35822  itg2addnclem  35837  itg2addnclem2  35838  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anc  35867  areacirclem1  35874  areacirclem4  35877  areacirc  35879  geomcau  35926  isbnd2  35950  ssbnd  35955  heiborlem7  35984  heiborlem8  35985  bfplem2  35990  rrncmslem  35999  rrnequiv  36002  dvrelog3  40080  aks4d1p1p6  40088  irrapxlem1  40651  irrapxlem2  40652  irrapxlem3  40653  irrapxlem5  40655  neglt  42830  2timesgt  42834  supxrge  42884  suplesup  42885  xrlexaddrp  42898  xralrple2  42900  infleinflem1  42916  xralrple4  42919  xralrple3  42920  xrralrecnnle  42929  climinf  43154  mullimc  43164  mullimcf  43171  limcrecl  43177  limcleqr  43192  addlimc  43196  0ellimcdiv  43197  limclner  43199  liminflimsupclim  43355  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem7  43555  fourierdlem73  43727  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  sge0iunmptlemre  43960  smflimlem4  44319  fldivexpfllog2  45922  blenre  45931  itscnhlc0yqe  46116  itscnhlc0xyqsol  46122  itschlc0xyqsol  46124  itsclc0xyqsolr  46126  itsclinecirc0in  46132  itsclquadb  46133  itscnhlinecirc02plem3  46141  itscnhlinecirc02p  46142  inlinecirc02plem  46143  inlinecirc02p  46144  amgmwlem  46517