Theorem rpxrd 13060

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℝ^*cxr 11241  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-ss 3930  df-xr 11246  df-rp 13016

This theorem is referenced by:  sgnmulrp2  15144  ssblex  24553  metequiv2  24635  metss2lem  24636  methaus  24645  met1stc  24646  met2ndci  24647  metcnp  24666  metcnpi3  24671  metustexhalf  24681  blval2  24687  metuel2  24690  nmoi2  24855  metdcnlem  24962  metdscnlem  24981  metnrmlem2  24986  metnrmlem3  24987  cnheibor  25082  cnllycmp  25083  lebnumlem3  25090  nmoleub2lem  25241  nmhmcn  25247  iscfil2  25393  cfil3i  25396  iscfil3  25400  cfilfcls  25401  iscmet3lem2  25419  caubl  25435  caublcls  25436  relcmpcmet  25445  bcthlem2  25452  bcthlem4  25454  bcthlem5  25455  ellimc3  26006  ftc1a  26164  ulmdvlem1  26528  psercnlem2  26552  psercn  26554  pserdvlem2  26556  pserdv  26557  efopn  26788  logccv  26793  efrlim  27099  lgamucov  27167  ftalem3  27204  logexprlim  27354  pntpbnd1a  27714  pntleme  27737  pntlem3  27738  pntleml  27740  ubthlem1  31162  ubthlem2  31163  tpr2rico  34246  xrmulc1cn  34264  omssubadd  34634  ptrecube  38158  poimirlem29  38187  heicant  38193  ftc1anclem6  38236  ftc1anclem7  38237  sstotbnd2  38312  equivtotbnd  38316  totbndbnd  38327  cntotbnd  38334  heibor1lem  38347  heiborlem3  38351  heiborlem6  38354  heiborlem8  38356  supxrge  45945  infrpge  45958  infleinflem1  45976  stoweid  46668  qndenserrnbl  46900  sge0rpcpnf  47026  sge0xaddlem1  47038