Theorem rpxrd 13172

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝ^*cxr 11349  ℝ⁺crp 13127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-un 4150  df-xr 11354  df-rp 13128

This theorem is used by:  sgnmulrp2  15270  ssblex  24756  metequiv2  24838  metss2lem  24839  methaus  24848  met1stc  24849  met2ndci  24850  metcnp  24869  metcnpi3  24874  metustexhalf  24884  blval2  24890  metuel2  24893  nmoi2  25058  metdcnlem  25165  metdscnlem  25184  metnrmlem2  25189  metnrmlem3  25190  cnheibor  25285  cnllycmp  25286  lebnumlem3  25293  nmoleub2lem  25444  nmhmcn  25450  iscfil2  25596  cfil3i  25599  iscfil3  25603  cfilfcls  25604  iscmet3lem2  25622  caubl  25638  caublcls  25639  relcmpcmet  25648  bcthlem2  25655  bcthlem4  25657  bcthlem5  25658  ellimc3  26208  ftc1a  26366  ulmdvlem1  26736  psercnlem2  26760  psercn  26762  pserdvlem2  26764  pserdv  26765  efopn  26995  logccv  27000  efrlim  27306  lgamucov  27374  ftalem3  27411  logexprlim  27561  pntpbnd1a  27921  pntleme  27944  pntlem3  27945  pntleml  27947  ubthlem1  31481  ubthlem2  31482  tpr2rico  34594  xrmulc1cn  34612  omssubadd  34982  ptrecube  38675  poimirlem29  38704  heicant  38710  ftc1anclem6  38753  ftc1anclem7  38754  sstotbnd2  38845  equivtotbnd  38849  totbndbnd  38860  cntotbnd  38867  heibor1lem  38880  heiborlem3  38884  heiborlem6  38887  heiborlem8  38889  supxrge  46486  infrpge  46499  infleinflem1  46517  stoweid  47209  qndenserrnbl  47441  sge0rpcpnf  47567  sge0xaddlem1  47579