Theorem rpxrd 12978

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝ^*cxr 11169  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-un 3888  df-ss 3900  df-xr 11174  df-rp 12934

This theorem is referenced by:  ssblex  24411  metequiv2  24493  metss2lem  24494  methaus  24503  met1stc  24504  met2ndci  24505  metcnp  24524  metcnpi3  24529  metustexhalf  24539  blval2  24545  metuel2  24548  nmoi2  24713  metdcnlem  24820  metdscnlem  24839  metnrmlem2  24844  metnrmlem3  24845  cnheibor  24940  cnllycmp  24941  lebnumlem3  24948  nmoleub2lem  25099  nmhmcn  25105  iscfil2  25251  cfil3i  25254  iscfil3  25258  cfilfcls  25259  iscmet3lem2  25277  caubl  25293  caublcls  25294  relcmpcmet  25303  bcthlem2  25310  bcthlem4  25312  bcthlem5  25313  ellimc3  25864  ftc1a  26022  ulmdvlem1  26383  psercnlem2  26407  psercn  26409  pserdvlem2  26411  pserdv  26412  efopn  26640  logccv  26645  efrlim  26951  lgamucov  27019  ftalem3  27056  logexprlim  27206  pntpbnd1a  27566  pntleme  27589  pntlem3  27590  pntleml  27592  ubthlem1  30959  ubthlem2  30960  sgnmulrp2  32928  tpr2rico  34096  xrmulc1cn  34114  omssubadd  34484  ptrecube  37987  poimirlem29  38016  heicant  38022  ftc1anclem6  38065  ftc1anclem7  38066  sstotbnd2  38141  equivtotbnd  38145  totbndbnd  38156  cntotbnd  38163  heibor1lem  38176  heiborlem3  38180  heiborlem6  38183  heiborlem8  38185  supxrge  45783  infrpge  45796  infleinflem1  45814  stoweid  46506  qndenserrnbl  46738  sge0rpcpnf  46864  sge0xaddlem1  46876