Theorem rpxr 12950

Description: A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
rpxr	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Proof of Theorem rpxr

Step	Hyp	Ref	Expression
1		rpre 12949	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2	1	rexrd 11193	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2119  ℝ^*cxr 11176  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-un 3895  df-ss 3907  df-xr 11181  df-rp 12941

This theorem is referenced by:  xlemul1  13240  xlemul2  13241  xltmul1  13242  xltmul2  13243  modelico  13838  muladdmodid  13870  sgnrrp  15051  blcntrps  24402  blcntr  24403  blssexps  24416  blssex  24417  blin2  24419  neibl  24491  blnei  24492  metss  24498  metss2lem  24501  stdbdmet  24506  stdbdmopn  24508  metrest  24514  prdsxmslem2  24519  metcnp3  24530  metcnp  24531  metcnpi3  24536  txmetcnp  24537  metustid  24544  cfilucfil  24549  blval2  24552  elbl4  24553  metucn  24561  nmoix  24719  xrsmopn  24803  reperflem  24809  reconnlem2  24818  metdseq0  24845  cnllycmp  24948  lebnum  24956  xlebnum  24957  lebnumii  24958  nmhmcn  25112  lmmbr  25250  lmmbr2  25251  lmnn  25255  cfilfcls  25266  iscau2  25269  iscmet3lem2  25284  equivcfil  25291  flimcfil  25306  cmpcmet  25311  bcthlem5  25320  ellimc3  25871  pige3ALT  26509  efopnlem1  26645  efopnlem2  26646  efopn  26647  xrlimcnp  26957  efrlim  26958  lgamcvg2  27043  pntlemi  27592  pntlemp  27598  ubthlem1  30966  xdivpnfrp  33018  pnfinf  33271  signsply0  34742  cnllysconn  35480  poimirlem29  38023  heicant  38029  itg2gt0cn  38049  ftc1anc  38075  areacirclem1  38082  areacirc  38087  blssp  38130  sstotbnd2  38148  isbndx  38156  isbnd2  38157  isbnd3  38158  ssbnd  38162  prdstotbnd  38168  prdsbnd2  38169  cntotbnd  38170  ismtybndlem  38180  heibor1  38184  infleinflem1  45821  limcrecl  46081  islpcn  46089  etransclem18  46702  etransclem46  46730  ioorrnopnlem  46754  sge0iunmptlemre  46865  itscnhlinecirc02p  49283