Theorem rpxrd 11370

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

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpxrd	|- ( ph -> A e. RR* )

Proof of Theorem rpxrd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 |- ( ph -> A e. RR+ )
2	1	rpred 11369	. 2 |- ( ph -> A e. RR )
3	2	rexrd 9715	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1897   RR*cxr 9699   RR+crp 11330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-un 3420  df-in 3422  df-ss 3429  df-xr 9704  df-rp 11331

This theorem is referenced by:  ssblex  21491  metequiv2  21573  metss2lem  21574  methaus  21583  met1stc  21584  met2ndci  21585  metcnp  21604  metcnpi3  21609  metustexhalf  21619  blval2  21625  metuel2  21628  nmoi2  21783  nmoi2OLD  21799  metdcnlem  21902  metdscnlem  21920  metnrmlem2  21925  metnrmlem3  21926  metdscnlemOLD  21935  metnrmlem2OLD  21940  metnrmlem3OLD  21941  cnheibor  22031  cnllycmp  22032  lebnumlem3  22039  lebnumlem3OLD  22042  nmoleub2lem  22176  nmhmcn  22182  iscfil2  22284  cfil3i  22287  iscfil3  22291  iscmet3lem2  22310  caubl  22325  caublcls  22326  relcmpcmet  22334  bcthlem2  22341  bcthlem4  22343  bcthlem5  22344  ellimc3  22882  ftc1a  23037  ulmdvlem1  23403  psercnlem2  23427  psercn  23429  pserdvlem2  23431  pserdv  23432  efopn  23651  logccv  23656  efrlim  23943  lgamucov  24011  ftalem3  24047  logexprlim  24201  pntpbnd1a  24471  pntleme  24494  pntlem3  24495  pntleml  24497  ubthlem1  26560  ubthlem2  26561  tpr2rico  28766  xrmulc1cn  28784  omssubadd  29176  omssubaddOLD  29180  sgnmulrp2  29462  ptrecube  31984  poimirlem29  32013  heicant  32019  ftc1anclem6  32066  ftc1anclem7  32067  sstotbnd2  32150  equivtotbnd  32154  totbndbnd  32165  cntotbnd  32172  heibor1lem  32185  heiborlem3  32189  heiborlem6  32192  heiborlem8  32194  supxrge  37598  infrpge  37611  stoweid  37962  qndenserrnbl  38201  sge0rpcpnf  38300  sge0xaddlem1  38312