Theorem rpxrd 12951

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11166  ℝ⁺crp 12906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-ss 3907  df-xr 11171  df-rp 12907

This theorem is referenced by:  ssblex  24371  metequiv2  24453  metss2lem  24454  methaus  24463  met1stc  24464  met2ndci  24465  metcnp  24484  metcnpi3  24489  metustexhalf  24499  blval2  24505  metuel2  24508  nmoi2  24673  metdcnlem  24780  metdscnlem  24799  metnrmlem2  24804  metnrmlem3  24805  cnheibor  24900  cnllycmp  24901  lebnumlem3  24908  nmoleub2lem  25059  nmhmcn  25065  iscfil2  25211  cfil3i  25214  iscfil3  25218  cfilfcls  25219  iscmet3lem2  25237  caubl  25253  caublcls  25254  relcmpcmet  25263  bcthlem2  25270  bcthlem4  25272  bcthlem5  25273  ellimc3  25824  ftc1a  25985  ulmdvlem1  26349  psercnlem2  26374  psercn  26376  pserdvlem2  26378  pserdv  26379  efopn  26607  logccv  26612  efrlim  26919  efrlimOLD  26920  lgamucov  26988  ftalem3  27025  logexprlim  27176  pntpbnd1a  27536  pntleme  27559  pntlem3  27560  pntleml  27562  ubthlem1  30930  ubthlem2  30931  sgnmulrp2  32900  tpr2rico  34062  xrmulc1cn  34080  omssubadd  34450  ptrecube  37932  poimirlem29  37961  heicant  37967  ftc1anclem6  38010  ftc1anclem7  38011  sstotbnd2  38086  equivtotbnd  38090  totbndbnd  38101  cntotbnd  38108  heibor1lem  38121  heiborlem3  38125  heiborlem6  38128  heiborlem8  38130  supxrge  45771  infrpge  45784  infleinflem1  45802  stoweid  46495  qndenserrnbl  46727  sge0rpcpnf  46853  sge0xaddlem1  46865