|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > rpxr | Structured version Visualization version GIF version | ||
| Description: A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.) | 
| Ref | Expression | 
|---|---|
| rpxr | ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | rpre 13044 | . 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
| 2 | 1 | rexrd 11312 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∈ wcel 2107 ℝ*cxr 11295 ℝ+crp 13035 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-un 3955 df-ss 3967 df-xr 11300 df-rp 13036 | 
| This theorem is referenced by: xlemul1 13333 xlemul2 13334 xltmul1 13335 xltmul2 13336 modelico 13922 muladdmodid 13952 sgnrrp 15131 blcntrps 24423 blcntr 24424 blssexps 24437 blssex 24438 blin2 24440 neibl 24515 blnei 24516 metss 24522 metss2lem 24525 stdbdmet 24530 stdbdmopn 24532 metrest 24538 prdsxmslem2 24543 metcnp3 24554 metcnp 24555 metcnpi3 24560 txmetcnp 24561 metustid 24568 cfilucfil 24573 blval2 24576 elbl4 24577 metucn 24585 nmoix 24751 xrsmopn 24835 reperflem 24841 reconnlem2 24850 metdseq0 24877 cnllycmp 24989 lebnum 24997 xlebnum 24998 lebnumii 24999 nmhmcn 25154 lmmbr 25293 lmmbr2 25294 lmnn 25298 cfilfcls 25309 iscau2 25312 iscmet3lem2 25327 equivcfil 25334 flimcfil 25349 cmpcmet 25354 bcthlem5 25363 ellimc3 25915 pige3ALT 26563 efopnlem1 26699 efopnlem2 26700 efopn 26701 xrlimcnp 27012 efrlim 27013 efrlimOLD 27014 lgamcvg2 27099 pntlemi 27649 pntlemp 27655 ubthlem1 30890 xdivpnfrp 32916 pnfinf 33191 signsply0 34567 cnllysconn 35251 poimirlem29 37657 heicant 37663 itg2gt0cn 37683 ftc1anc 37709 areacirclem1 37716 areacirc 37721 blssp 37764 sstotbnd2 37782 isbndx 37790 isbnd2 37791 isbnd3 37792 ssbnd 37796 prdstotbnd 37802 prdsbnd2 37803 cntotbnd 37804 ismtybndlem 37814 heibor1 37818 infleinflem1 45386 limcrecl 45649 islpcn 45659 etransclem18 46272 etransclem46 46300 ioorrnopnlem 46324 sge0iunmptlemre 46435 itscnhlinecirc02p 48711 | 
| Copyright terms: Public domain | W3C validator |