Theorem rpxrd 13165

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-ss 3916  df-xr 11347  df-rp 13121

This theorem is used by:  sgnmulrp2  15261  ssblex  24747  metequiv2  24829  metss2lem  24830  methaus  24839  met1stc  24840  met2ndci  24841  metcnp  24860  metcnpi3  24865  metustexhalf  24875  blval2  24881  metuel2  24884  nmoi2  25049  metdcnlem  25156  metdscnlem  25175  metnrmlem2  25180  metnrmlem3  25181  cnheibor  25276  cnllycmp  25277  lebnumlem3  25284  nmoleub2lem  25435  nmhmcn  25441  iscfil2  25587  cfil3i  25590  iscfil3  25594  cfilfcls  25595  iscmet3lem2  25613  caubl  25629  caublcls  25630  relcmpcmet  25639  bcthlem2  25646  bcthlem4  25648  bcthlem5  25649  ellimc3  26199  ftc1a  26357  ulmdvlem1  26727  psercnlem2  26751  psercn  26753  pserdvlem2  26755  pserdv  26756  efopn  26986  logccv  26991  efrlim  27297  lgamucov  27365  ftalem3  27402  logexprlim  27552  pntpbnd1a  27912  pntleme  27935  pntlem3  27936  pntleml  27938  ubthlem1  31472  ubthlem2  31473  tpr2rico  34544  xrmulc1cn  34562  omssubadd  34932  ptrecube  38538  poimirlem29  38567  heicant  38573  ftc1anclem6  38616  ftc1anclem7  38617  sstotbnd2  38708  equivtotbnd  38712  totbndbnd  38723  cntotbnd  38730  heibor1lem  38743  heiborlem3  38747  heiborlem6  38750  heiborlem8  38752  supxrge  46349  infrpge  46362  infleinflem1  46380  stoweid  47072  qndenserrnbl  47304  sge0rpcpnf  47430  sge0xaddlem1  47442