Theorem rpre 11254

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 11249	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3484	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3432	. 2 |- RR+ C_ RR
4	3	sseli 3398	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1872   {crab 2713   class class class wbr 4361   RRcr 9484   0cc0 9485   < clt 9621   RR+crp 11248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rab 2718  df-in 3381  df-ss 3388  df-rp 11249

This theorem is referenced by:  rpxr  11255  rpcn  11256  rpssre  11258  rpge0  11260  rprege0  11262  rprene0  11264  rpaddcl  11269  rpmulcl  11270  rpdivcl  11271  rpgecl  11274  xralrple  11444  xlemul1  11522  infmrp1  11580  iccdil  11716  ltdifltdiv  12011  modcl  12045  mod0  12048  mulmod0  12049  modge0  12051  modlt  12052  modid0  12067  modabs  12075  modabs2  12076  modcyc  12077  modltm1p1mod  12087  2txmodxeq0  12095  2submod  12096  moddi  12102  modsubdir  12103  modeqmodmin  12104  modirr  12105  expnlbnd  12347  rennim  13241  cnpart  13242  sqrlem1  13245  sqrlem2  13246  sqrlem4  13248  sqrlem5  13249  sqrlem6  13250  sqrlem7  13251  resqrex  13253  rpsqrtcl  13267  sqreulem  13361  eqsqrt2d  13370  2clim  13574  reccn2  13598  cn1lem  13599  climsqz  13642  climsqz2  13643  rlimsqzlem  13650  climsup  13671  climcau  13672  caucvgrlem2  13678  iseralt  13689  cvgcmp  13814  cvgcmpce  13816  divrcnv  13848  rprisefaccl  14014  efgt1  14108  ef01bndlem  14176  sinltx  14181  stdbdmet  21468  stdbdmopn  21470  met2ndci  21474  cfilucfil  21511  ngptgp  21581  reperflem  21773  iccntr  21776  reconnlem2  21782  opnreen  21786  metdseq0  21808  metdseq0OLD  21823  xlebnum  21933  cphsqrtcl3  22102  iscmet3lem3  22197  iscmet3lem1  22198  iscmet3lem2  22199  caubl  22214  lmcau  22219  bcthlem4  22232  minveclem3b  22307  minveclem3  22308  minveclem3bOLD  22319  minveclem3OLD  22320  ivthlem2  22340  ivthlem3  22341  nulmbl2  22427  opnmbllem  22496  itg2const2  22636  itg2mulclem  22641  dveflem  22868  lhop  22905  dvcnvre  22908  aalioulem2  23226  aaliou  23231  aaliou3lem4  23239  ulmcaulem  23286  ulmcau  23287  ulmcn  23291  itgulm  23300  reeff1o  23339  pilem2  23344  pilem2OLD  23345  logleb  23489  logcj  23492  argimgt0  23498  logdmnrp  23523  logcnlem3  23526  logcnlem4  23527  advlog  23536  efopnlem1  23538  cxple2  23579  cxplt2  23580  cxple3  23583  cxpcn3  23625  resqrtcn  23626  relogbf  23665  asinneg  23749  atanbndlem  23788  cxplim  23834  cxp2limlem  23838  cxp2lim  23839  cxploglim  23840  cxploglim2  23841  logdiflbnd  23857  harmoniclbnd  23871  harmonicbnd4  23873  chtrpcl  24039  ppiltx  24041  chtleppi  24075  logfacubnd  24086  logfaclbnd  24087  logfacbnd3  24088  logexprlim  24090  bposlem7  24155  bposlem8  24156  bposlem9  24157  chebbnd1  24247  chtppilim  24250  chto1ub  24251  chpo1ub  24255  vmadivsum  24257  rpvmasumlem  24262  dchrisumlem3  24266  dchrvmasumlem2  24273  dchrvmasumiflem1  24276  dchrisum0  24295  mudivsum  24305  mulogsumlem  24306  mulogsum  24307  mulog2sumlem2  24310  log2sumbnd  24319  selberglem2  24321  selberglem3  24322  selberg  24323  selberg2lem  24325  selberg2  24326  pntrf  24338  pntrmax  24339  pntrsumo1  24340  selbergr  24343  selbergs  24349  pntrlog2bndlem4  24355  pntrlog2bndlem5  24356  pntibndlem1  24364  pntlem3  24384  pntlemp  24385  pntleml  24386  pnt2  24388  padicabvcxp  24407  vacn  26267  nmcvcn  26268  smcnlem  26270  blocnilem  26382  chscllem2  27228  nmcexi  27616  nmcopexi  27617  nmcfnexi  27641  pnfinf  28446  sqsscirc1  28661  dya2icoseg2  29047  probfinmeasbOLD  29208  probfinmeasb  29209  subfacval3  29859  opnrebl  30920  opnrebl2  30921  taupilem1  31629  opnmbllem0  31883  itg2addnclem  31900  itg2addnclem2  31901  itg2addnclem3  31902  itg2addnc  31903  itg2gt0cn  31904  ftc1anclem5  31928  ftc1anclem7  31930  ftc1anc  31932  areacirclem1  31939  areacirclem4  31942  areacirc  31944  geomcau  31995  isbnd2  32022  ssbnd  32027  heiborlem7  32056  heiborlem8  32057  bfplem2  32062  rrncmslem  32071  rrnequiv  32074  irrapxlem1  35579  irrapxlem2  35580  irrapxlem3  35581  irrapxlem5  35583  rpexpmord  35709  neglt  37391  2timesgt  37398  supxrge  37458  suplesup  37459  xrlexaddrp  37472  xralrple2  37474  climinf  37567  climinfOLD  37568  mullimc  37579  mullimcf  37586  limcrecl  37592  limcleqr  37608  addlimc  37612  0ellimcdiv  37613  limclner  37615  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  stoweidlem7  37750  fourierdlem73  37926  fourierdlem87  37940  fourierdlem103  37956  fourierdlem104  37957  sge0iunmptlemre  38108  fldivexpfllog2  39969  blenre  39978