Theorem rpxrd 12935

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝ^*cxr 11145  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3902  df-ss 3914  df-xr 11150  df-rp 12891

This theorem is referenced by:  ssblex  24343  metequiv2  24425  metss2lem  24426  methaus  24435  met1stc  24436  met2ndci  24437  metcnp  24456  metcnpi3  24461  metustexhalf  24471  blval2  24477  metuel2  24480  nmoi2  24645  metdcnlem  24752  metdscnlem  24771  metnrmlem2  24776  metnrmlem3  24777  cnheibor  24881  cnllycmp  24882  lebnumlem3  24889  nmoleub2lem  25041  nmhmcn  25047  iscfil2  25193  cfil3i  25196  iscfil3  25200  cfilfcls  25201  iscmet3lem2  25219  caubl  25235  caublcls  25236  relcmpcmet  25245  bcthlem2  25252  bcthlem4  25254  bcthlem5  25255  ellimc3  25807  ftc1a  25971  ulmdvlem1  26336  psercnlem2  26361  psercn  26363  pserdvlem2  26365  pserdv  26366  efopn  26594  logccv  26599  efrlim  26906  efrlimOLD  26907  lgamucov  26975  ftalem3  27012  logexprlim  27163  pntpbnd1a  27523  pntleme  27546  pntlem3  27547  pntleml  27549  ubthlem1  30850  ubthlem2  30851  sgnmulrp2  32819  tpr2rico  33925  xrmulc1cn  33943  omssubadd  34313  ptrecube  37670  poimirlem29  37699  heicant  37705  ftc1anclem6  37748  ftc1anclem7  37749  sstotbnd2  37824  equivtotbnd  37828  totbndbnd  37839  cntotbnd  37846  heibor1lem  37859  heiborlem3  37863  heiborlem6  37866  heiborlem8  37868  supxrge  45447  infrpge  45460  infleinflem1  45478  stoweid  46171  qndenserrnbl  46403  sge0rpcpnf  46529  sge0xaddlem1  46541