Theorem rpxrd 13100

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝ^*cxr 11323  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328  df-rp 13058

This theorem is referenced by:  ssblex  24459  metequiv2  24544  metss2lem  24545  methaus  24554  met1stc  24555  met2ndci  24556  metcnp  24575  metcnpi3  24580  metustexhalf  24590  blval2  24596  metuel2  24599  nmoi2  24772  metdcnlem  24877  metdscnlem  24896  metnrmlem2  24901  metnrmlem3  24902  cnheibor  25006  cnllycmp  25007  lebnumlem3  25014  nmoleub2lem  25166  nmhmcn  25172  iscfil2  25319  cfil3i  25322  iscfil3  25326  cfilfcls  25327  iscmet3lem2  25345  caubl  25361  caublcls  25362  relcmpcmet  25371  bcthlem2  25378  bcthlem4  25380  bcthlem5  25381  ellimc3  25934  ftc1a  26098  ulmdvlem1  26461  psercnlem2  26486  psercn  26488  pserdvlem2  26490  pserdv  26491  efopn  26718  logccv  26723  efrlim  27030  efrlimOLD  27031  lgamucov  27099  ftalem3  27136  logexprlim  27287  pntpbnd1a  27647  pntleme  27670  pntlem3  27671  pntleml  27673  ubthlem1  30902  ubthlem2  30903  tpr2rico  33858  xrmulc1cn  33876  omssubadd  34265  sgnmulrp2  34508  ptrecube  37580  poimirlem29  37609  heicant  37615  ftc1anclem6  37658  ftc1anclem7  37659  sstotbnd2  37734  equivtotbnd  37738  totbndbnd  37749  cntotbnd  37756  heibor1lem  37769  heiborlem3  37773  heiborlem6  37776  heiborlem8  37778  supxrge  45253  infrpge  45266  infleinflem1  45285  stoweid  45984  qndenserrnbl  46216  sge0rpcpnf  46342  sge0xaddlem1  46354