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 12619 | . 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | 1 | rexrd 10908 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ℝ*cxr 10891 ℝ+crp 12611 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3071 df-v 3423 df-un 3886 df-in 3888 df-ss 3898 df-xr 10896 df-rp 12612 |
This theorem is referenced by: xlemul1 12905 xlemul2 12906 xltmul1 12907 xltmul2 12908 modelico 13481 muladdmodid 13511 sgnrrp 14682 blcntrps 23337 blcntr 23338 blssexps 23351 blssex 23352 blin2 23354 neibl 23426 blnei 23427 metss 23433 metss2lem 23436 stdbdmet 23441 stdbdmopn 23443 metrest 23449 prdsxmslem2 23454 metcnp3 23465 metcnp 23466 metcnpi3 23471 txmetcnp 23472 metustid 23479 cfilucfil 23484 blval2 23487 elbl4 23488 metucn 23496 nmoix 23654 xrsmopn 23736 reperflem 23742 reconnlem2 23751 metdseq0 23778 cnllycmp 23880 lebnum 23888 xlebnum 23889 lebnumii 23890 nmhmcn 24044 lmmbr 24182 lmmbr2 24183 lmnn 24187 cfilfcls 24198 iscau2 24201 iscmet3lem2 24216 equivcfil 24223 flimcfil 24238 cmpcmet 24243 bcthlem5 24252 ellimc3 24803 pige3ALT 25436 efopnlem1 25571 efopnlem2 25572 efopn 25573 xrlimcnp 25878 efrlim 25879 lgamcvg2 25964 pntlemi 26512 pntlemp 26518 ubthlem1 28978 xdivpnfrp 30954 pnfinf 31183 signsply0 32269 cnllysconn 32946 poimirlem29 35573 heicant 35579 itg2gt0cn 35599 ftc1anc 35625 areacirclem1 35632 areacirc 35637 blssp 35681 sstotbnd2 35699 isbndx 35707 isbnd2 35708 isbnd3 35709 ssbnd 35713 prdstotbnd 35719 prdsbnd2 35720 cntotbnd 35721 ismtybndlem 35731 heibor1 35735 infleinflem1 42615 limcrecl 42876 islpcn 42886 etransclem18 43499 etransclem46 43527 ioorrnopnlem 43551 sge0iunmptlemre 43659 itscnhlinecirc02p 45835 |
Copyright terms: Public domain | W3C validator |