Theorem rpxrd 13014

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 13013	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	rexrd 11261	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2107  ℝ^*cxr 11244  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3953  df-in 3955  df-ss 3965  df-xr 11249  df-rp 12972

This theorem is referenced by:  ssblex  23926  metequiv2  24011  metss2lem  24012  methaus  24021  met1stc  24022  met2ndci  24023  metcnp  24042  metcnpi3  24047  metustexhalf  24057  blval2  24063  metuel2  24066  nmoi2  24239  metdcnlem  24344  metdscnlem  24363  metnrmlem2  24368  metnrmlem3  24369  cnheibor  24463  cnllycmp  24464  lebnumlem3  24471  nmoleub2lem  24622  nmhmcn  24628  iscfil2  24775  cfil3i  24778  iscfil3  24782  cfilfcls  24783  iscmet3lem2  24801  caubl  24817  caublcls  24818  relcmpcmet  24827  bcthlem2  24834  bcthlem4  24836  bcthlem5  24837  ellimc3  25388  ftc1a  25546  ulmdvlem1  25904  psercnlem2  25928  psercn  25930  pserdvlem2  25932  pserdv  25933  efopn  26158  logccv  26163  efrlim  26464  lgamucov  26532  ftalem3  26569  logexprlim  26718  pntpbnd1a  27078  pntleme  27101  pntlem3  27102  pntleml  27104  ubthlem1  30111  ubthlem2  30112  tpr2rico  32881  xrmulc1cn  32899  omssubadd  33288  sgnmulrp2  33531  ptrecube  36477  poimirlem29  36506  heicant  36512  ftc1anclem6  36555  ftc1anclem7  36556  sstotbnd2  36631  equivtotbnd  36635  totbndbnd  36646  cntotbnd  36653  heibor1lem  36666  heiborlem3  36670  heiborlem6  36673  heiborlem8  36675  supxrge  44035  infrpge  44048  infleinflem1  44067  stoweid  44766  qndenserrnbl  44998  sge0rpcpnf  45124  sge0xaddlem1  45136