Theorem rpre 13036

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℝcr 11157  ℝ⁺crp 13028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-ss 3964  df-rp 13029

This theorem is referenced by:  rpxr  13037  rpcn  13038  rpge0  13041  rprege0  13043  rprene0  13045  rpaddcl  13050  rpmulcl  13051  rpdivcl  13053  rpgecl  13056  ledivge1le  13099  addlelt  13142  xralrple  13238  xlemul1  13323  infmrp1  13377  iccdil  13521  ltdifltdiv  13854  modcl  13893  mod0  13896  mulmod0  13897  modge0  13899  modlt  13900  modid0  13917  modabs  13924  modabs2  13925  modcyc  13926  modmuladd  13933  modmuladdnn0  13935  modltm1p1mod  13943  2txmodxeq0  13951  2submod  13952  moddi  13959  modsubdir  13960  modeqmodmin  13961  modirr  13962  rpexpmord  14187  expnlbnd  14250  rennim  15244  cnpart  15245  01sqrexlem1  15247  01sqrexlem2  15248  01sqrexlem4  15250  01sqrexlem5  15251  01sqrexlem6  15252  01sqrexlem7  15253  resqrex  15255  rpsqrtcl  15269  sqreulem  15364  eqsqrt2d  15373  2clim  15574  reccn2  15599  cn1lem  15600  climsqz  15643  climsqz2  15644  rlimsqzlem  15653  climsup  15674  climcau  15675  caucvgrlem2  15679  iseralt  15689  cvgcmp  15820  cvgcmpce  15822  divrcnv  15856  rprisefaccl  16025  efgt1  16118  ef01bndlem  16186  sinltx  16191  stdbdmet  24516  stdbdmopn  24518  met2ndci  24522  cfilucfil  24559  ngptgp  24636  reperflem  24825  iccntr  24828  reconnlem2  24834  opnreen  24838  metdseq0  24861  xlebnum  24982  cphsqrtcl3  25206  iscmet3lem3  25309  iscmet3lem1  25310  iscmet3lem2  25311  caubl  25327  lmcau  25332  bcthlem4  25346  minveclem3b  25447  minveclem3  25448  ivthlem2  25472  ivthlem3  25473  nulmbl2  25556  opnmbllem  25621  itg2const2  25762  itg2mulclem  25767  dveflem  26002  lhop  26040  dvcnvre  26043  aalioulem2  26361  aaliou  26366  aaliou3lem4  26374  ulmcaulem  26423  ulmcau  26424  ulmcn  26428  itgulm  26437  reeff1o  26477  pilem2  26482  logleb  26630  logcj  26633  argimgt0  26639  logdmnrp  26668  logcnlem3  26671  logcnlem4  26672  advlog  26681  efopnlem1  26683  cxple2  26724  cxplt2  26725  cxple3  26728  2irrexpq  26758  cxpcn3  26776  resqrtcn  26777  relogbf  26819  asinneg  26914  atanbndlem  26953  cxplim  27000  cxp2limlem  27004  cxp2lim  27005  cxploglim  27006  cxploglim2  27007  logdiflbnd  27023  harmoniclbnd  27037  harmonicbnd4  27039  chtrpcl  27203  ppiltx  27205  chtleppi  27239  logfacubnd  27250  logfaclbnd  27251  logfacbnd3  27252  logexprlim  27254  bposlem7  27319  bposlem8  27320  bposlem9  27321  chebbnd1  27501  chtppilim  27504  chto1ub  27505  chpo1ub  27509  vmadivsum  27511  rpvmasumlem  27516  dchrisumlem3  27520  dchrvmasumlem2  27527  dchrvmasumiflem1  27530  dchrisum0  27549  mudivsum  27559  mulogsumlem  27560  mulogsum  27561  mulog2sumlem2  27564  log2sumbnd  27573  selberglem2  27575  selberglem3  27576  selberg  27577  selberg2lem  27579  selberg2  27580  pntrf  27592  pntrmax  27593  pntrsumo1  27594  selbergr  27597  selbergs  27603  pntrlog2bndlem4  27609  pntrlog2bndlem5  27610  pntibndlem1  27618  pntlem3  27638  pntlemp  27639  pntleml  27640  pnt2  27642  padicabvcxp  27661  vacn  30627  nmcvcn  30628  smcnlem  30630  blocnilem  30737  chscllem2  31571  nmcexi  31959  nmcopexi  31960  nmcfnexi  31984  dp2ltsuc  32747  dpval3rp  32761  dplti  32766  dpgti  32767  dpexpp1  32769  dpadd2  32771  pnfinf  33048  sqsscirc1  33723  dya2icoseg2  34112  probfinmeasb  34262  probfinmeasbALTV  34263  signshf  34434  divsqrtid  34440  logdivsqrle  34496  hgt750lem2  34498  subfacval3  35017  opnrebl  36032  opnrebl2  36033  taupilem1  37028  opnmbllem0  37357  itg2addnclem  37372  itg2addnclem2  37373  itg2addnclem3  37374  itg2addnc  37375  itg2gt0cn  37376  ftc1anclem5  37398  ftc1anclem7  37400  ftc1anc  37402  areacirclem1  37409  areacirclem4  37412  areacirc  37414  geomcau  37460  isbnd2  37484  ssbnd  37489  heiborlem7  37518  heiborlem8  37519  bfplem2  37524  rrncmslem  37533  rrnequiv  37536  dvrelog3  41764  aks4d1p1p6  41772  irrapxlem1  42479  irrapxlem2  42480  irrapxlem3  42481  irrapxlem5  42483  neglt  44899  2timesgt  44903  supxrge  44953  suplesup  44954  xrlexaddrp  44967  xralrple2  44969  infleinflem1  44985  xralrple4  44988  xralrple3  44989  xrralrecnnle  44998  climinf  45227  mullimc  45237  mullimcf  45244  limcrecl  45250  limcleqr  45265  addlimc  45269  0ellimcdiv  45270  limclner  45272  liminflimsupclim  45428  ioodvbdlimc1lem1  45552  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  stoweidlem7  45628  fourierdlem73  45800  fourierdlem87  45814  fourierdlem103  45830  fourierdlem104  45831  sge0iunmptlemre  46036  smflimlem4  46395  fldivexpfllog2  47953  blenre  47962  itscnhlc0yqe  48147  itscnhlc0xyqsol  48153  itschlc0xyqsol  48155  itsclc0xyqsolr  48157  itsclinecirc0in  48163  itsclquadb  48164  itscnhlinecirc02plem3  48172  itscnhlinecirc02p  48173  inlinecirc02plem  48174  inlinecirc02p  48175  amgmwlem  48550