Theorem rpxrd 11286

Description: A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1

Assertion

Ref	Expression
rpxrd

Proof of Theorem rpxrd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3
2	1	rpred 11285	. 2
3	2	rexrd 9664	1

Syntax hints:  ->wi 4  e.wcel 1818  cxr 9648  crp 11249

This theorem is referenced by:  ssblex  20931  metequiv2  21013  metss2lem  21014  methaus  21023  met1stc  21024  met2ndci  21025  metcnp  21044  metcnpi3  21049  metustexhalfOLD  21066  metustexhalf  21067  blval2  21078  metuel2  21082  nmoi2  21237  metdcnlem  21341  metdscnlem  21359  metnrmlem2  21364  metnrmlem3  21365  cnheibor  21455  cnllycmp  21456  lebnumlem3  21463  nmoleub2lem  21597  nmhmcn  21603  iscfil2  21705  cfil3i  21708  iscfil3  21712  iscmet3lem2  21731  caubl  21746  caublcls  21747  relcmpcmet  21755  bcthlem2  21764  bcthlem4  21766  bcthlem5  21767  ellimc3  22283  ftc1a  22438  ulmdvlem1  22795  psercnlem2  22819  psercn  22821  pserdvlem2  22823  pserdv  22824  efopn  23039  logccv  23044  efrlim  23299  ftalem3  23348  logexprlim  23500  pntpbnd1a  23770  pntleme  23793  pntlem3  23794  pntleml  23796  ubthlem1  25786  ubthlem2  25787  tpr2rico  27894  xrmulc1cn  27912  sgnmulrp2  28482  lgamucov  28580  heicant  30049  ftc1anclem6  30095  ftc1anclem7  30096  sstotbnd2  30270  equivtotbnd  30274  totbndbnd  30285  cntotbnd  30292  heibor1lem  30305  heiborlem3  30309  heiborlem6  30312  heiborlem8  30314  stoweid  31845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-xr 9653  df-rp 11250