Theorem rpre 11715

Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
rpre	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		df-rp 11709	. . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2		ssrab2 3650	. . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
3	1, 2	eqsstri 3598	. 2 ⊢ ℝ+ ⊆ ℝ
4	3	sseli 3564	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1977  {crab 2900   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-rp 11709

This theorem is referenced by:  rpxr  11716  rpcn  11717  rpssre  11719  rpge0  11721  rprege0  11723  rprene0  11725  rpaddcl  11730  rpmulcl  11731  rpdivcl  11732  rpgecl  11735  ledivge1le  11777  addlelt  11818  xralrple  11910  xlemul1  11992  infmrp1  12045  iccdil  12181  ltdifltdiv  12497  modcl  12534  mod0  12537  mulmod0  12538  modge0  12540  modlt  12541  modid0  12558  modabs  12565  modabs2  12566  modcyc  12567  modmuladd  12574  modmuladdnn0  12576  modltm1p1mod  12584  2txmodxeq0  12592  2submod  12593  moddi  12600  modsubdir  12601  modeqmodmin  12602  modirr  12603  expnlbnd  12856  rennim  13827  cnpart  13828  sqrlem1  13831  sqrlem2  13832  sqrlem4  13834  sqrlem5  13835  sqrlem6  13836  sqrlem7  13837  resqrex  13839  rpsqrtcl  13853  sqreulem  13947  eqsqrt2d  13956  2clim  14151  reccn2  14175  cn1lem  14176  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  climsup  14248  climcau  14249  caucvgrlem2  14253  iseralt  14263  cvgcmp  14389  cvgcmpce  14391  divrcnv  14423  rprisefaccl  14593  efgt1  14685  ef01bndlem  14753  sinltx  14758  stdbdmet  22131  stdbdmopn  22133  met2ndci  22137  cfilucfil  22174  ngptgp  22250  reperflem  22429  iccntr  22432  reconnlem2  22438  opnreen  22442  metdseq0  22465  xlebnum  22572  cphsqrtcl3  22795  iscmet3lem3  22896  iscmet3lem1  22897  iscmet3lem2  22898  caubl  22914  lmcau  22919  bcthlem4  22932  minveclem3b  23007  minveclem3  23008  ivthlem2  23028  ivthlem3  23029  nulmbl2  23111  opnmbllem  23175  itg2const2  23314  itg2mulclem  23319  dveflem  23546  lhop  23583  dvcnvre  23586  aalioulem2  23892  aaliou  23897  aaliou3lem4  23905  ulmcaulem  23952  ulmcau  23953  ulmcn  23957  itgulm  23966  reeff1o  24005  pilem2  24010  logleb  24153  logcj  24156  argimgt0  24162  logdmnrp  24187  logcnlem3  24190  logcnlem4  24191  advlog  24200  efopnlem1  24202  cxple2  24243  cxplt2  24244  cxple3  24247  cxpcn3  24289  resqrtcn  24290  relogbf  24329  asinneg  24413  atanbndlem  24452  cxplim  24498  cxp2limlem  24502  cxp2lim  24503  cxploglim  24504  cxploglim2  24505  logdiflbnd  24521  harmoniclbnd  24535  harmonicbnd4  24537  chtrpcl  24701  ppiltx  24703  chtleppi  24735  logfacubnd  24746  logfaclbnd  24747  logfacbnd3  24748  logexprlim  24750  bposlem7  24815  bposlem8  24816  bposlem9  24817  chebbnd1  24961  chtppilim  24964  chto1ub  24965  chpo1ub  24969  vmadivsum  24971  rpvmasumlem  24976  dchrisumlem3  24980  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0  25009  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem2  25024  log2sumbnd  25033  selberglem2  25035  selberglem3  25036  selberg  25037  selberg2lem  25039  selberg2  25040  pntrf  25052  pntrmax  25053  pntrsumo1  25054  selbergr  25057  selbergs  25063  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntibndlem1  25078  pntlem3  25098  pntlemp  25099  pntleml  25100  pnt2  25102  padicabvcxp  25121  vacn  26933  nmcvcn  26934  smcnlem  26936  blocnilem  27043  chscllem2  27881  nmcexi  28269  nmcopexi  28270  nmcfnexi  28294  pnfinf  29068  sqsscirc1  29282  dya2icoseg2  29667  probfinmeasbOLD  29817  probfinmeasb  29818  subfacval3  30425  opnrebl  31485  opnrebl2  31486  taupilem1  32344  opnmbllem0  32615  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anc  32663  areacirclem1  32670  areacirclem4  32673  areacirc  32675  geomcau  32725  isbnd2  32752  ssbnd  32757  heiborlem7  32786  heiborlem8  32787  bfplem2  32792  rrncmslem  32801  rrnequiv  32804  irrapxlem1  36404  irrapxlem2  36405  irrapxlem3  36406  irrapxlem5  36408  rpexpmord  36531  neglt  38437  2timesgt  38441  supxrge  38495  suplesup  38496  xrlexaddrp  38509  xralrple2  38511  infleinflem1  38527  xralrple4  38530  xralrple3  38531  xrralrecnnle  38543  climinf  38673  mullimc  38683  mullimcf  38690  limcrecl  38696  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  limclner  38718  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem7  38900  fourierdlem73  39072  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  sge0iunmptlemre  39308  smflimlem4  39660  fldivexpfllog2  42157  blenre  42166  amgmwlem  42357