![]() |
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 12247 | . 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | 1 | rexrd 10537 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 ℝ*cxr 10520 ℝ+crp 12239 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rab 3114 df-v 3439 df-un 3864 df-in 3866 df-ss 3874 df-xr 10525 df-rp 12240 |
This theorem is referenced by: xlemul1 12533 xlemul2 12534 xltmul1 12535 xltmul2 12536 modelico 13099 muladdmodid 13129 sgnrrp 14284 blcntrps 22705 blcntr 22706 blssexps 22719 blssex 22720 blin2 22722 neibl 22794 blnei 22795 metss 22801 metss2lem 22804 stdbdmet 22809 stdbdmopn 22811 metrest 22817 prdsxmslem2 22822 metcnp3 22833 metcnp 22834 metcnpi3 22839 txmetcnp 22840 metustid 22847 cfilucfil 22852 blval2 22855 elbl4 22856 metucn 22864 nmoix 23021 xrsmopn 23103 reperflem 23109 reconnlem2 23118 metdseq0 23145 cnllycmp 23243 lebnum 23251 xlebnum 23252 lebnumii 23253 nmhmcn 23407 lmmbr 23544 lmmbr2 23545 lmnn 23549 cfilfcls 23560 iscau2 23563 iscmet3lem2 23578 equivcfil 23585 flimcfil 23600 cmpcmet 23605 bcthlem5 23614 ellimc3 24160 pige3ALT 24788 efopnlem1 24920 efopnlem2 24921 efopn 24922 xrlimcnp 25228 efrlim 25229 lgamcvg2 25314 pntlemi 25862 pntlemp 25868 ubthlem1 28338 xdivpnfrp 30293 pnfinf 30450 signsply0 31438 cnllysconn 32100 poimirlem29 34452 heicant 34458 itg2gt0cn 34478 ftc1anc 34506 areacirclem1 34513 areacirc 34518 blssp 34563 sstotbnd2 34584 isbndx 34592 isbnd2 34593 isbnd3 34594 ssbnd 34598 prdstotbnd 34604 prdsbnd2 34605 cntotbnd 34606 ismtybndlem 34616 heibor1 34620 infleinflem1 41179 limcrecl 41452 islpcn 41462 etransclem18 42079 etransclem46 42107 ioorrnopnlem 42131 sge0iunmptlemre 42239 itscnhlinecirc02p 44253 |
Copyright terms: Public domain | W3C validator |