![]() |
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 12043 | . 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | 1 | rexrd 10292 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2145 ℝ*cxr 10276 ℝ+crp 12036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 df-v 3353 df-un 3729 df-in 3731 df-ss 3738 df-xr 10281 df-rp 12037 |
This theorem is referenced by: xlemul1 12326 xlemul2 12327 xltmul1 12328 xltmul2 12329 modelico 12889 muladdmodid 12919 sgnrrp 14040 blcntrps 22438 blcntr 22439 unirnblps 22445 unirnbl 22446 blssexps 22452 blssex 22453 blin2 22455 neibl 22527 blnei 22528 metss 22534 metss2lem 22537 stdbdmet 22542 stdbdmopn 22544 mopnex 22545 metrest 22550 prdsxmslem2 22555 metcnp3 22566 metcnp 22567 metcnpi3 22572 txmetcnp 22573 metustid 22580 cfilucfil 22585 blval2 22588 elbl4 22589 metucn 22597 dscopn 22599 nmoix 22754 xrsmopn 22836 zdis 22840 reperflem 22842 reconnlem2 22851 metdseq0 22878 cnllycmp 22976 lebnum 22984 xlebnum 22985 lebnumii 22986 nmhmcn 23140 lmmbr 23276 lmmbr2 23277 lmnn 23281 cfilfcls 23292 iscau2 23295 iscmet3lem2 23310 equivcfil 23317 flimcfil 23332 cmpcmet 23336 cncmet 23339 bcthlem5 23345 ellimc3 23864 abelthlem2 24407 abelthlem5 24410 abelthlem7 24413 pige3 24491 dvlog2 24621 efopnlem1 24624 efopnlem2 24625 efopn 24626 logtayl 24628 logtayl2 24630 xrlimcnp 24917 efrlim 24918 lgamcvg2 25003 pntlemi 25515 pntlemp 25521 ubthlem1 28067 xdivpnfrp 29982 pnfinf 30078 signsply0 30969 cnllysconn 31566 poimirlem29 33772 heicant 33778 itg2gt0cn 33798 ftc1anc 33826 areacirclem1 33833 areacirc 33838 blssp 33885 sstotbnd2 33906 isbndx 33914 isbnd2 33915 isbnd3 33916 ssbnd 33920 prdstotbnd 33926 prdsbnd2 33927 cntotbnd 33928 ismtybndlem 33938 heibor1 33942 infleinflem1 40103 limcrecl 40380 islpcn 40390 etransclem18 40987 etransclem46 41015 ioorrnopnlem 41042 sge0iunmptlemre 41150 |
Copyright terms: Public domain | W3C validator |