Theorem rpxrd 13205

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝ^*cxr 11381  ℝ⁺crp 13160

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-un 4154  df-xr 11386  df-rp 13161

This theorem is used by:  sgnmulrp2  15304  ssblex  24802  metequiv2  24884  metss2lem  24885  methaus  24894  met1stc  24895  met2ndci  24896  metcnp  24915  metcnpi3  24920  metustexhalf  24930  blval2  24936  metuel2  24939  nmoi2  25104  metdcnlem  25211  metdscnlem  25230  metnrmlem2  25235  metnrmlem3  25236  cnheibor  25331  cnllycmp  25332  lebnumlem3  25339  nmoleub2lem  25490  nmhmcn  25496  iscfil2  25642  cfil3i  25645  iscfil3  25649  cfilfcls  25650  iscmet3lem2  25668  caubl  25684  caublcls  25685  relcmpcmet  25694  bcthlem2  25701  bcthlem4  25703  bcthlem5  25704  ellimc3  26254  ftc1a  26412  ulmdvlem1  26784  psercnlem2  26808  psercn  26810  pserdvlem2  26812  pserdv  26813  efopn  27043  logccv  27048  efrlim  27354  lgamucov  27422  ftalem3  27459  logexprlim  27609  pntpbnd1a  27969  pntleme  27992  pntlem3  27993  pntleml  27995  ubthlem1  31529  ubthlem2  31530  tpr2rico  34655  xrmulc1cn  34673  omssubadd  35043  ptrecube  38806  poimirlem29  38835  heicant  38841  ftc1anclem6  38884  ftc1anclem7  38885  sstotbnd2  38974  equivtotbnd  38978  totbndbnd  38989  cntotbnd  38996  heibor1lem  39009  heiborlem3  39013  heiborlem6  39016  heiborlem8  39018  supxrge  46623  infrpge  46636  infleinflem1  46654  stoweid  47346  qndenserrnbl  47578  sge0rpcpnf  47704  sge0xaddlem1  47716