Theorem rpxrd 11873

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℝ^*cxr 10073  ℝ⁺crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-xr 10078  df-rp 11833

This theorem is referenced by:  ssblex  22233  metequiv2  22315  metss2lem  22316  methaus  22325  met1stc  22326  met2ndci  22327  metcnp  22346  metcnpi3  22351  metustexhalf  22361  blval2  22367  metuel2  22370  nmoi2  22534  metdcnlem  22639  metdscnlem  22658  metnrmlem2  22663  metnrmlem3  22664  cnheibor  22754  cnllycmp  22755  lebnumlem3  22762  nmoleub2lem  22914  nmhmcn  22920  iscfil2  23064  cfil3i  23067  iscfil3  23071  iscmet3lem2  23090  caubl  23106  caublcls  23107  relcmpcmet  23115  bcthlem2  23122  bcthlem4  23124  bcthlem5  23125  ellimc3  23643  ftc1a  23800  ulmdvlem1  24154  psercnlem2  24178  psercn  24180  pserdvlem2  24182  pserdv  24183  efopn  24404  logccv  24409  efrlim  24696  lgamucov  24764  ftalem3  24801  logexprlim  24950  pntpbnd1a  25274  pntleme  25297  pntlem3  25298  pntleml  25300  ubthlem1  27726  ubthlem2  27727  tpr2rico  29958  xrmulc1cn  29976  omssubadd  30362  sgnmulrp2  30605  ptrecube  33409  poimirlem29  33438  heicant  33444  ftc1anclem6  33490  ftc1anclem7  33491  sstotbnd2  33573  equivtotbnd  33577  totbndbnd  33588  cntotbnd  33595  heibor1lem  33608  heiborlem3  33612  heiborlem6  33615  heiborlem8  33617  supxrge  39554  infrpge  39567  infleinflem1  39586  stoweid  40280  qndenserrnbl  40515  sge0rpcpnf  40638  sge0xaddlem1  40650