Theorem rpre 11839

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

Assertion

Ref	Expression
rpre	|- ( A e. RR+ -> A e. RR )

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		df-rp 11833	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3687	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3635	. 2 |- RR+ C_ RR
4	3	sseli 3599	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1990   {crab 2916   class class class wbr 4653   RRcr 9935   0cc0 9936   < clt 10074   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-rp 11833

This theorem is referenced by:  rpxr  11840  rpcn  11841  rpssre  11843  rpge0  11845  rprege0  11847  rprene0  11849  rpaddcl  11854  rpmulcl  11855  rpdivcl  11856  rpgecl  11859  ledivge1le  11901  addlelt  11942  xralrple  12036  xlemul1  12120  infmrp1  12174  iccdil  12310  ltdifltdiv  12635  modcl  12672  mod0  12675  mulmod0  12676  modge0  12678  modlt  12679  modid0  12696  modabs  12703  modabs2  12704  modcyc  12705  modmuladd  12712  modmuladdnn0  12714  modltm1p1mod  12722  2txmodxeq0  12730  2submod  12731  moddi  12738  modsubdir  12739  modeqmodmin  12740  modirr  12741  expnlbnd  12994  rennim  13979  cnpart  13980  sqrlem1  13983  sqrlem2  13984  sqrlem4  13986  sqrlem5  13987  sqrlem6  13988  sqrlem7  13989  resqrex  13991  rpsqrtcl  14005  sqreulem  14099  eqsqrt2d  14108  2clim  14303  reccn2  14327  cn1lem  14328  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  climsup  14400  climcau  14401  caucvgrlem2  14405  iseralt  14415  cvgcmp  14548  cvgcmpce  14550  divrcnv  14584  rprisefaccl  14754  efgt1  14846  ef01bndlem  14914  sinltx  14919  stdbdmet  22321  stdbdmopn  22323  met2ndci  22327  cfilucfil  22364  ngptgp  22440  reperflem  22621  iccntr  22624  reconnlem2  22630  opnreen  22634  metdseq0  22657  xlebnum  22764  cphsqrtcl3  22987  iscmet3lem3  23088  iscmet3lem1  23089  iscmet3lem2  23090  caubl  23106  lmcau  23111  bcthlem4  23124  minveclem3b  23199  minveclem3  23200  ivthlem2  23221  ivthlem3  23222  nulmbl2  23304  opnmbllem  23369  itg2const2  23508  itg2mulclem  23513  dveflem  23742  lhop  23779  dvcnvre  23782  aalioulem2  24088  aaliou  24093  aaliou3lem4  24101  ulmcaulem  24148  ulmcau  24149  ulmcn  24153  itgulm  24162  reeff1o  24201  pilem2  24206  logleb  24349  logcj  24352  argimgt0  24358  logdmnrp  24387  logcnlem3  24390  logcnlem4  24391  advlog  24400  efopnlem1  24402  cxple2  24443  cxplt2  24444  cxple3  24447  cxpcn3  24489  resqrtcn  24490  relogbf  24529  asinneg  24613  atanbndlem  24652  cxplim  24698  cxp2limlem  24702  cxp2lim  24703  cxploglim  24704  cxploglim2  24705  logdiflbnd  24721  harmoniclbnd  24735  harmonicbnd4  24737  chtrpcl  24901  ppiltx  24903  chtleppi  24935  logfacubnd  24946  logfaclbnd  24947  logfacbnd3  24948  logexprlim  24950  bposlem7  25015  bposlem8  25016  bposlem9  25017  chebbnd1  25161  chtppilim  25164  chto1ub  25165  chpo1ub  25169  vmadivsum  25171  rpvmasumlem  25176  dchrisumlem3  25180  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0  25209  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem2  25224  log2sumbnd  25233  selberglem2  25235  selberglem3  25236  selberg  25237  selberg2lem  25239  selberg2  25240  pntrf  25252  pntrmax  25253  pntrsumo1  25254  selbergr  25257  selbergs  25263  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntibndlem1  25278  pntlem3  25298  pntlemp  25299  pntleml  25300  pnt2  25302  padicabvcxp  25321  vacn  27549  nmcvcn  27550  smcnlem  27552  blocnilem  27659  chscllem2  28497  nmcexi  28885  nmcopexi  28886  nmcfnexi  28910  dp2ltsuc  29593  dpval3rp  29608  dplti  29613  dpgti  29614  dpexpp1  29616  dpadd2  29618  pnfinf  29737  sqsscirc1  29954  dya2icoseg2  30340  probfinmeasbOLD  30490  probfinmeasb  30491  divsqrtid  30672  logdivsqrle  30728  hgt750lem2  30730  subfacval3  31171  opnrebl  32315  opnrebl2  32316  taupilem1  33167  opnmbllem0  33445  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anc  33493  areacirclem1  33500  areacirclem4  33503  areacirc  33505  geomcau  33555  isbnd2  33582  ssbnd  33587  heiborlem7  33616  heiborlem8  33617  bfplem2  33622  rrncmslem  33631  rrnequiv  33634  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  irrapxlem5  37390  rpexpmord  37513  neglt  39496  2timesgt  39500  supxrge  39554  suplesup  39555  xrlexaddrp  39568  xralrple2  39570  infleinflem1  39586  xralrple4  39589  xralrple3  39590  xrralrecnnle  39602  climinf  39838  mullimc  39848  mullimcf  39855  limcrecl  39861  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limclner  39883  liminflimsupclim  40039  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem7  40224  fourierdlem73  40396  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  sge0iunmptlemre  40632  smflimlem4  40982  fldivexpfllog2  42359  blenre  42368  amgmwlem  42548