Theorem rpxrd 13078

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝ^*cxr 11294  ℝ⁺crp 13034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-ss 3968  df-xr 11299  df-rp 13035

This theorem is referenced by:  ssblex  24438  metequiv2  24523  metss2lem  24524  methaus  24533  met1stc  24534  met2ndci  24535  metcnp  24554  metcnpi3  24559  metustexhalf  24569  blval2  24575  metuel2  24578  nmoi2  24751  metdcnlem  24858  metdscnlem  24877  metnrmlem2  24882  metnrmlem3  24883  cnheibor  24987  cnllycmp  24988  lebnumlem3  24995  nmoleub2lem  25147  nmhmcn  25153  iscfil2  25300  cfil3i  25303  iscfil3  25307  cfilfcls  25308  iscmet3lem2  25326  caubl  25342  caublcls  25343  relcmpcmet  25352  bcthlem2  25359  bcthlem4  25361  bcthlem5  25362  ellimc3  25914  ftc1a  26078  ulmdvlem1  26443  psercnlem2  26468  psercn  26470  pserdvlem2  26472  pserdv  26473  efopn  26700  logccv  26705  efrlim  27012  efrlimOLD  27013  lgamucov  27081  ftalem3  27118  logexprlim  27269  pntpbnd1a  27629  pntleme  27652  pntlem3  27653  pntleml  27655  ubthlem1  30889  ubthlem2  30890  tpr2rico  33911  xrmulc1cn  33929  omssubadd  34302  sgnmulrp2  34546  ptrecube  37627  poimirlem29  37656  heicant  37662  ftc1anclem6  37705  ftc1anclem7  37706  sstotbnd2  37781  equivtotbnd  37785  totbndbnd  37796  cntotbnd  37803  heibor1lem  37816  heiborlem3  37820  heiborlem6  37823  heiborlem8  37825  supxrge  45349  infrpge  45362  infleinflem1  45381  stoweid  46078  qndenserrnbl  46310  sge0rpcpnf  46436  sge0xaddlem1  46448