Theorem rpre 11271

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 11266	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3524	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3472	. 2 |- RR+ C_ RR
4	3	sseli 3438	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1842   {crab 2758   class class class wbr 4395   RRcr 9521   0cc0 9522   < clt 9658   RR+crp 11265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-in 3421  df-ss 3428  df-rp 11266

This theorem is referenced by:  rpxr  11272  rpcn  11273  rpssre  11275  rpge0  11277  rprege0  11279  rprene0  11281  rpaddcl  11286  rpmulcl  11287  rpdivcl  11288  rpgecl  11291  xralrple  11457  xlemul1  11535  iccdil  11712  ltdifltdiv  12004  modcl  12038  mod0  12041  mulmod0  12042  modge0  12044  modlt  12045  modid0  12060  modabs  12068  modabs2  12069  modcyc  12070  modltm1p1mod  12080  2txmodxeq0  12088  2submod  12089  moddi  12095  modsubdir  12096  modeqmodmin  12097  modirr  12098  expnlbnd  12340  rennim  13221  cnpart  13222  sqrlem1  13225  sqrlem2  13226  sqrlem4  13228  sqrlem5  13229  sqrlem6  13230  sqrlem7  13231  resqrex  13233  rpsqrtcl  13247  sqreulem  13341  eqsqrt2d  13350  2clim  13544  reccn2  13568  cn1lem  13569  climsqz  13612  climsqz2  13613  rlimsqzlem  13620  climsup  13641  climcau  13642  caucvgrlem2  13646  iseralt  13656  cvgcmp  13781  cvgcmpce  13783  divrcnv  13815  rprisefaccl  13968  efgt1  14060  ef01bndlem  14128  sinltx  14133  stdbdmet  21311  stdbdmopn  21313  met2ndci  21317  cfilucfilOLD  21364  cfilucfil  21365  ngptgp  21442  reperflem  21615  iccntr  21618  reconnlem2  21624  opnreen  21628  metdseq0  21650  xlebnum  21757  cphsqrtcl3  21926  iscmet3lem3  22021  iscmet3lem1  22022  iscmet3lem2  22023  caubl  22038  lmcau  22043  bcthlem4  22058  minveclem3b  22135  minveclem3  22136  ivthlem2  22156  ivthlem3  22157  nulmbl2  22239  opnmbllem  22302  itg2const2  22440  itg2mulclem  22445  dveflem  22672  lhop  22709  dvcnvre  22712  aalioulem2  23021  aaliou  23026  aaliou3lem4  23034  ulmcaulem  23081  ulmcau  23082  ulmcn  23086  itgulm  23095  reeff1o  23134  pilem2  23139  logleb  23282  logcj  23285  argimgt0  23291  logdmnrp  23316  logcnlem3  23319  logcnlem4  23320  advlog  23329  efopnlem1  23331  cxple2  23372  cxplt2  23373  cxple3  23376  cxpcn3  23418  resqrtcn  23419  relogbf  23458  asinneg  23542  atanbndlem  23581  cxplim  23627  cxp2limlem  23631  cxp2lim  23632  cxploglim  23633  cxploglim2  23634  logdiflbnd  23650  harmoniclbnd  23664  harmonicbnd4  23666  chtrpcl  23830  ppiltx  23832  chtleppi  23866  logfacubnd  23877  logfaclbnd  23878  logfacbnd3  23879  logexprlim  23881  bposlem7  23946  bposlem8  23947  bposlem9  23948  chebbnd1  24038  chtppilim  24041  chto1ub  24042  chpo1ub  24046  vmadivsum  24048  rpvmasumlem  24053  dchrisumlem3  24057  dchrvmasumlem2  24064  dchrvmasumiflem1  24067  dchrisum0  24086  mudivsum  24096  mulogsumlem  24097  mulogsum  24098  mulog2sumlem2  24101  log2sumbnd  24110  selberglem2  24112  selberglem3  24113  selberg  24114  selberg2lem  24116  selberg2  24117  pntrf  24129  pntrmax  24130  pntrsumo1  24131  selbergr  24134  selbergs  24140  pntrlog2bndlem4  24146  pntrlog2bndlem5  24147  pntibndlem1  24155  pntlem3  24175  pntlemp  24176  pntleml  24177  pnt2  24179  padicabvcxp  24198  vacn  26018  nmcvcn  26019  smcnlem  26021  blocnilem  26133  chscllem2  26970  nmcexi  27358  nmcopexi  27359  nmcfnexi  27383  pnfinf  28179  sqsscirc1  28343  dya2icoseg2  28726  probfinmeasbOLD  28873  probfinmeasb  28874  subfacval3  29486  opnrebl  30548  opnrebl2  30549  taupilem1  31247  opnmbllem0  31422  itg2addnclem  31439  itg2addnclem2  31440  itg2addnclem3  31441  itg2addnc  31442  itg2gt0cn  31443  ftc1anclem5  31467  ftc1anclem7  31469  ftc1anc  31471  areacirclem1  31478  areacirclem4  31481  areacirc  31483  geomcau  31534  isbnd2  31561  ssbnd  31566  heiborlem7  31595  heiborlem8  31596  bfplem2  31601  rrncmslem  31610  rrnequiv  31613  irrapxlem1  35119  irrapxlem2  35120  irrapxlem3  35121  irrapxlem5  35123  rpexpmord  35245  neglt  36841  2timesgt  36848  climinf  36980  mullimc  36990  mullimcf  36997  limcrecl  37003  limcleqr  37018  addlimc  37022  0ellimcdiv  37023  limclner  37025  ioodvbdlimc1lem1  37096  ioodvbdlimc1lem2  37097  ioodvbdlimc2lem  37099  stoweidlem7  37157  fourierdlem73  37330  fourierdlem87  37344  fourierdlem103  37360  fourierdlem104  37361  fldivexpfllog2  38696  blenre  38705