Theorem rpxrd 13088

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝ^*cxr 11267  ℝ⁺crp 13043

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-ss 3916  df-xr 11272  df-rp 13044

This theorem is used by:  sgnmulrp2  15182  ssblex  24655  metequiv2  24737  metss2lem  24738  methaus  24747  met1stc  24748  met2ndci  24749  metcnp  24768  metcnpi3  24773  metustexhalf  24783  blval2  24789  metuel2  24792  nmoi2  24957  metdcnlem  25064  metdscnlem  25083  metnrmlem2  25088  metnrmlem3  25089  cnheibor  25184  cnllycmp  25185  lebnumlem3  25192  nmoleub2lem  25343  nmhmcn  25349  iscfil2  25495  cfil3i  25498  iscfil3  25502  cfilfcls  25503  iscmet3lem2  25521  caubl  25537  caublcls  25538  relcmpcmet  25547  bcthlem2  25554  bcthlem4  25556  bcthlem5  25557  ellimc3  26107  ftc1a  26265  ulmdvlem1  26637  psercnlem2  26661  psercn  26663  pserdvlem2  26665  pserdv  26666  efopn  26896  logccv  26901  efrlim  27207  lgamucov  27275  ftalem3  27312  logexprlim  27462  pntpbnd1a  27822  pntleme  27845  pntlem3  27846  pntleml  27848  ubthlem1  31352  ubthlem2  31353  tpr2rico  34423  xrmulc1cn  34441  omssubadd  34812  ptrecube  38370  poimirlem29  38399  heicant  38405  ftc1anclem6  38448  ftc1anclem7  38449  sstotbnd2  38525  equivtotbnd  38529  totbndbnd  38540  cntotbnd  38547  heibor1lem  38560  heiborlem3  38564  heiborlem6  38567  heiborlem8  38569  supxrge  46169  infrpge  46182  infleinflem1  46200  stoweid  46892  qndenserrnbl  47124  sge0rpcpnf  47250  sge0xaddlem1  47262