Theorem rpre 12073

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 12067	. . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2		ssrab2 3895	. . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
3	1, 2	eqsstri 3843	. 2 ⊢ ℝ+ ⊆ ℝ
4	3	sseli 3805	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2157  {crab 3111   class class class wbr 4855  ℝcr 10230  0cc0 10231   < clt 10369  ℝ⁺crp 12066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-in 3787  df-ss 3794  df-rp 12067

This theorem is referenced by:  rpxr  12074  rpcn  12075  rpssre  12077  rpge0  12079  rprege0  12081  rprene0  12083  rpaddcl  12088  rpmulcl  12089  rpdivcl  12090  rpgecl  12093  ledivge1le  12135  addlelt  12178  xralrple  12274  xlemul1  12358  infmrp1  12412  iccdil  12553  ltdifltdiv  12879  modcl  12916  mod0  12919  mulmod0  12920  modge0  12922  modlt  12923  modid0  12940  modabs  12947  modabs2  12948  modcyc  12949  modmuladd  12956  modmuladdnn0  12958  modltm1p1mod  12966  2txmodxeq0  12974  2submod  12975  moddi  12982  modsubdir  12983  modeqmodmin  12984  modirr  12985  expnlbnd  13237  rennim  14222  cnpart  14223  sqrlem1  14226  sqrlem2  14227  sqrlem4  14229  sqrlem5  14230  sqrlem6  14231  sqrlem7  14232  resqrex  14234  rpsqrtcl  14248  sqreulem  14342  eqsqrt2d  14351  2clim  14546  reccn2  14570  cn1lem  14571  climsqz  14614  climsqz2  14615  rlimsqzlem  14622  climsup  14643  climcau  14644  caucvgrlem2  14648  iseralt  14658  cvgcmp  14790  cvgcmpce  14792  divrcnv  14826  rprisefaccl  14994  efgt1  15086  ef01bndlem  15154  sinltx  15159  stdbdmet  22555  stdbdmopn  22557  met2ndci  22561  cfilucfil  22598  ngptgp  22674  reperflem  22855  iccntr  22858  reconnlem2  22864  opnreen  22868  metdseq0  22891  xlebnum  22998  cphsqrtcl3  23220  iscmet3lem3  23322  iscmet3lem1  23323  iscmet3lem2  23324  caubl  23340  lmcau  23345  bcthlem4  23358  minveclem3b  23434  minveclem3  23435  ivthlem2  23456  ivthlem3  23457  nulmbl2  23540  opnmbllem  23605  itg2const2  23745  itg2mulclem  23750  dveflem  23979  lhop  24016  dvcnvre  24019  aalioulem2  24325  aaliou  24330  aaliou3lem4  24338  ulmcaulem  24385  ulmcau  24386  ulmcn  24390  itgulm  24399  reeff1o  24438  pilem2  24443  logleb  24586  logcj  24589  argimgt0  24595  logdmnrp  24624  logcnlem3  24627  logcnlem4  24628  advlog  24637  efopnlem1  24639  cxple2  24680  cxplt2  24681  cxple3  24684  cxpcn3  24726  resqrtcn  24727  relogbf  24766  asinneg  24850  atanbndlem  24889  cxplim  24935  cxp2limlem  24939  cxp2lim  24940  cxploglim  24941  cxploglim2  24942  logdiflbnd  24958  harmoniclbnd  24972  harmonicbnd4  24974  chtrpcl  25138  ppiltx  25140  chtleppi  25172  logfacubnd  25183  logfaclbnd  25184  logfacbnd3  25185  logexprlim  25187  bposlem7  25252  bposlem8  25253  bposlem9  25254  chebbnd1  25398  chtppilim  25401  chto1ub  25402  chpo1ub  25406  vmadivsum  25408  rpvmasumlem  25413  dchrisumlem3  25417  dchrvmasumlem2  25424  dchrvmasumiflem1  25427  dchrisum0  25446  mudivsum  25456  mulogsumlem  25457  mulogsum  25458  mulog2sumlem2  25461  log2sumbnd  25470  selberglem2  25472  selberglem3  25473  selberg  25474  selberg2lem  25476  selberg2  25477  pntrf  25489  pntrmax  25490  pntrsumo1  25491  selbergr  25494  selbergs  25500  pntrlog2bndlem4  25506  pntrlog2bndlem5  25507  pntibndlem1  25515  pntlem3  25535  pntlemp  25536  pntleml  25537  pnt2  25539  padicabvcxp  25558  vacn  27900  nmcvcn  27901  smcnlem  27903  blocnilem  28010  chscllem2  28848  nmcexi  29236  nmcopexi  29237  nmcfnexi  29261  dp2ltsuc  29942  dpval3rp  29956  dplti  29961  dpgti  29962  dpexpp1  29964  dpadd2  29966  pnfinf  30085  sqsscirc1  30302  dya2icoseg2  30688  probfinmeasbOLD  30838  probfinmeasb  30839  divsqrtid  31020  logdivsqrle  31076  hgt750lem2  31078  subfacval3  31516  opnrebl  32658  opnrebl2  32659  taupilem1  33503  opnmbllem0  33777  itg2addnclem  33792  itg2addnclem2  33793  itg2addnclem3  33794  itg2addnc  33795  itg2gt0cn  33796  ftc1anclem5  33820  ftc1anclem7  33822  ftc1anc  33824  areacirclem1  33831  areacirclem4  33834  areacirc  33836  geomcau  33885  isbnd2  33912  ssbnd  33917  heiborlem7  33946  heiborlem8  33947  bfplem2  33952  rrncmslem  33961  rrnequiv  33964  irrapxlem1  37906  irrapxlem2  37907  irrapxlem3  37908  irrapxlem5  37910  rpexpmord  38032  neglt  39996  2timesgt  40000  supxrge  40052  suplesup  40053  xrlexaddrp  40066  xralrple2  40068  infleinflem1  40084  xralrple4  40087  xralrple3  40088  xrralrecnnle  40100  climinf  40336  mullimc  40346  mullimcf  40353  limcrecl  40359  limcleqr  40374  addlimc  40378  0ellimcdiv  40379  limclner  40381  liminflimsupclim  40537  ioodvbdlimc1lem1  40644  ioodvbdlimc1lem2  40645  ioodvbdlimc2lem  40647  stoweidlem7  40721  fourierdlem73  40893  fourierdlem87  40907  fourierdlem103  40923  fourierdlem104  40924  sge0iunmptlemre  41129  smflimlem4  41482  fldivexpfllog2  42945  blenre  42954  amgmwlem  43137