Theorem rpxrd 12433

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 10674  ℝ⁺crp 12390

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679  df-rp 12391

This theorem is referenced by:  ssblex  23038  metequiv2  23120  metss2lem  23121  methaus  23130  met1stc  23131  met2ndci  23132  metcnp  23151  metcnpi3  23156  metustexhalf  23166  blval2  23172  metuel2  23175  nmoi2  23339  metdcnlem  23444  metdscnlem  23463  metnrmlem2  23468  metnrmlem3  23469  cnheibor  23559  cnllycmp  23560  lebnumlem3  23567  nmoleub2lem  23718  nmhmcn  23724  iscfil2  23869  cfil3i  23872  iscfil3  23876  cfilfcls  23877  iscmet3lem2  23895  caubl  23911  caublcls  23912  relcmpcmet  23921  bcthlem2  23928  bcthlem4  23930  bcthlem5  23931  ellimc3  24477  ftc1a  24634  ulmdvlem1  24988  psercnlem2  25012  psercn  25014  pserdvlem2  25016  pserdv  25017  efopn  25241  logccv  25246  efrlim  25547  lgamucov  25615  ftalem3  25652  logexprlim  25801  pntpbnd1a  26161  pntleme  26184  pntlem3  26185  pntleml  26187  ubthlem1  28647  ubthlem2  28648  tpr2rico  31155  xrmulc1cn  31173  omssubadd  31558  sgnmulrp2  31801  ptrecube  34907  poimirlem29  34936  heicant  34942  ftc1anclem6  34987  ftc1anclem7  34988  sstotbnd2  35067  equivtotbnd  35071  totbndbnd  35082  cntotbnd  35089  heibor1lem  35102  heiborlem3  35106  heiborlem6  35109  heiborlem8  35111  supxrge  41626  infrpge  41639  infleinflem1  41658  stoweid  42368  qndenserrnbl  42600  sge0rpcpnf  42723  sge0xaddlem1  42735