Theorem rpxrd 12996

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11207  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-ss 3931  df-xr 11212  df-rp 12952

This theorem is referenced by:  ssblex  24316  metequiv2  24398  metss2lem  24399  methaus  24408  met1stc  24409  met2ndci  24410  metcnp  24429  metcnpi3  24434  metustexhalf  24444  blval2  24450  metuel2  24453  nmoi2  24618  metdcnlem  24725  metdscnlem  24744  metnrmlem2  24749  metnrmlem3  24750  cnheibor  24854  cnllycmp  24855  lebnumlem3  24862  nmoleub2lem  25014  nmhmcn  25020  iscfil2  25166  cfil3i  25169  iscfil3  25173  cfilfcls  25174  iscmet3lem2  25192  caubl  25208  caublcls  25209  relcmpcmet  25218  bcthlem2  25225  bcthlem4  25227  bcthlem5  25228  ellimc3  25780  ftc1a  25944  ulmdvlem1  26309  psercnlem2  26334  psercn  26336  pserdvlem2  26338  pserdv  26339  efopn  26567  logccv  26572  efrlim  26879  efrlimOLD  26880  lgamucov  26948  ftalem3  26985  logexprlim  27136  pntpbnd1a  27496  pntleme  27519  pntlem3  27520  pntleml  27522  ubthlem1  30799  ubthlem2  30800  sgnmulrp2  32761  tpr2rico  33902  xrmulc1cn  33920  omssubadd  34291  ptrecube  37614  poimirlem29  37643  heicant  37649  ftc1anclem6  37692  ftc1anclem7  37693  sstotbnd2  37768  equivtotbnd  37772  totbndbnd  37783  cntotbnd  37790  heibor1lem  37803  heiborlem3  37807  heiborlem6  37810  heiborlem8  37812  supxrge  45334  infrpge  45347  infleinflem1  45366  stoweid  46061  qndenserrnbl  46293  sge0rpcpnf  46419  sge0xaddlem1  46431