Theorem rpxrd 11911

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

Syntax hints:   → wi 4   ∈ wcel 2030  ℝ^*cxr 10111  ℝ⁺crp 11870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-xr 10116  df-rp 11871

This theorem is referenced by:  ssblex  22280  metequiv2  22362  metss2lem  22363  methaus  22372  met1stc  22373  met2ndci  22374  metcnp  22393  metcnpi3  22398  metustexhalf  22408  blval2  22414  metuel2  22417  nmoi2  22581  metdcnlem  22686  metdscnlem  22705  metnrmlem2  22710  metnrmlem3  22711  cnheibor  22801  cnllycmp  22802  lebnumlem3  22809  nmoleub2lem  22960  nmhmcn  22966  iscfil2  23110  cfil3i  23113  iscfil3  23117  iscmet3lem2  23136  caubl  23152  caublcls  23153  relcmpcmet  23161  bcthlem2  23168  bcthlem4  23170  bcthlem5  23171  ellimc3  23688  ftc1a  23845  ulmdvlem1  24199  psercnlem2  24223  psercn  24225  pserdvlem2  24227  pserdv  24228  efopn  24449  logccv  24454  efrlim  24741  lgamucov  24809  ftalem3  24846  logexprlim  24995  pntpbnd1a  25319  pntleme  25342  pntlem3  25343  pntleml  25345  ubthlem1  27854  ubthlem2  27855  tpr2rico  30086  xrmulc1cn  30104  omssubadd  30490  sgnmulrp2  30733  ptrecube  33539  poimirlem29  33568  heicant  33574  ftc1anclem6  33620  ftc1anclem7  33621  sstotbnd2  33703  equivtotbnd  33707  totbndbnd  33718  cntotbnd  33725  heibor1lem  33738  heiborlem3  33742  heiborlem6  33745  heiborlem8  33747  supxrge  39867  infrpge  39880  infleinflem1  39899  stoweid  40598  qndenserrnbl  40833  sge0rpcpnf  40956  sge0xaddlem1  40968