Theorem rpxrd 13017

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝ^*cxr 11247  ℝ⁺crp 12974

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 3954  df-in 3956  df-ss 3966  df-xr 11252  df-rp 12975

This theorem is referenced by:  ssblex  23934  metequiv2  24019  metss2lem  24020  methaus  24029  met1stc  24030  met2ndci  24031  metcnp  24050  metcnpi3  24055  metustexhalf  24065  blval2  24071  metuel2  24074  nmoi2  24247  metdcnlem  24352  metdscnlem  24371  metnrmlem2  24376  metnrmlem3  24377  cnheibor  24471  cnllycmp  24472  lebnumlem3  24479  nmoleub2lem  24630  nmhmcn  24636  iscfil2  24783  cfil3i  24786  iscfil3  24790  cfilfcls  24791  iscmet3lem2  24809  caubl  24825  caublcls  24826  relcmpcmet  24835  bcthlem2  24842  bcthlem4  24844  bcthlem5  24845  ellimc3  25396  ftc1a  25554  ulmdvlem1  25912  psercnlem2  25936  psercn  25938  pserdvlem2  25940  pserdv  25941  efopn  26166  logccv  26171  efrlim  26474  lgamucov  26542  ftalem3  26579  logexprlim  26728  pntpbnd1a  27088  pntleme  27111  pntlem3  27112  pntleml  27114  ubthlem1  30123  ubthlem2  30124  tpr2rico  32892  xrmulc1cn  32910  omssubadd  33299  sgnmulrp2  33542  ptrecube  36488  poimirlem29  36517  heicant  36523  ftc1anclem6  36566  ftc1anclem7  36567  sstotbnd2  36642  equivtotbnd  36646  totbndbnd  36657  cntotbnd  36664  heibor1lem  36677  heiborlem3  36681  heiborlem6  36684  heiborlem8  36686  supxrge  44048  infrpge  44061  infleinflem1  44080  stoweid  44779  qndenserrnbl  45011  sge0rpcpnf  45137  sge0xaddlem1  45149