Theorem rpxrd 12076

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝ^*cxr 10279  ℝ⁺crp 12035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-xr 10284  df-rp 12036

This theorem is referenced by:  ssblex  22453  metequiv2  22535  metss2lem  22536  methaus  22545  met1stc  22546  met2ndci  22547  metcnp  22566  metcnpi3  22571  metustexhalf  22581  blval2  22587  metuel2  22590  nmoi2  22754  metdcnlem  22859  metdscnlem  22878  metnrmlem2  22883  metnrmlem3  22884  cnheibor  22974  cnllycmp  22975  lebnumlem3  22982  nmoleub2lem  23133  nmhmcn  23139  iscfil2  23283  cfil3i  23286  iscfil3  23290  iscmet3lem2  23309  caubl  23325  caublcls  23326  relcmpcmet  23334  bcthlem2  23341  bcthlem4  23343  bcthlem5  23344  ellimc3  23863  ftc1a  24020  ulmdvlem1  24374  psercnlem2  24398  psercn  24400  pserdvlem2  24402  pserdv  24403  efopn  24625  logccv  24630  efrlim  24917  lgamucov  24985  ftalem3  25022  logexprlim  25171  pntpbnd1a  25495  pntleme  25518  pntlem3  25519  pntleml  25521  ubthlem1  28066  ubthlem2  28067  tpr2rico  30298  xrmulc1cn  30316  omssubadd  30702  sgnmulrp2  30945  ptrecube  33741  poimirlem29  33770  heicant  33776  ftc1anclem6  33821  ftc1anclem7  33822  sstotbnd2  33903  equivtotbnd  33907  totbndbnd  33918  cntotbnd  33925  heibor1lem  33938  heiborlem3  33942  heiborlem6  33945  heiborlem8  33947  supxrge  40065  infrpge  40078  infleinflem1  40097  stoweid  40792  qndenserrnbl  41027  sge0rpcpnf  41150  sge0xaddlem1  41162