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 12391 | . 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | 1 | rexrd 10685 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 ℝ*cxr 10668 ℝ+crp 12383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-un 3941 df-in 3943 df-ss 3952 df-xr 10673 df-rp 12384 |
This theorem is referenced by: xlemul1 12677 xlemul2 12678 xltmul1 12679 xltmul2 12680 modelico 13243 muladdmodid 13273 sgnrrp 14444 blcntrps 23016 blcntr 23017 blssexps 23030 blssex 23031 blin2 23033 neibl 23105 blnei 23106 metss 23112 metss2lem 23115 stdbdmet 23120 stdbdmopn 23122 metrest 23128 prdsxmslem2 23133 metcnp3 23144 metcnp 23145 metcnpi3 23150 txmetcnp 23151 metustid 23158 cfilucfil 23163 blval2 23166 elbl4 23167 metucn 23175 nmoix 23332 xrsmopn 23414 reperflem 23420 reconnlem2 23429 metdseq0 23456 cnllycmp 23554 lebnum 23562 xlebnum 23563 lebnumii 23564 nmhmcn 23718 lmmbr 23855 lmmbr2 23856 lmnn 23860 cfilfcls 23871 iscau2 23874 iscmet3lem2 23889 equivcfil 23896 flimcfil 23911 cmpcmet 23916 bcthlem5 23925 ellimc3 24471 pige3ALT 25099 efopnlem1 25233 efopnlem2 25234 efopn 25235 xrlimcnp 25540 efrlim 25541 lgamcvg2 25626 pntlemi 26174 pntlemp 26180 ubthlem1 28641 xdivpnfrp 30604 pnfinf 30807 signsply0 31816 cnllysconn 32487 poimirlem29 34915 heicant 34921 itg2gt0cn 34941 ftc1anc 34969 areacirclem1 34976 areacirc 34981 blssp 35025 sstotbnd2 35046 isbndx 35054 isbnd2 35055 isbnd3 35056 ssbnd 35060 prdstotbnd 35066 prdsbnd2 35067 cntotbnd 35068 ismtybndlem 35078 heibor1 35082 infleinflem1 41630 limcrecl 41902 islpcn 41912 etransclem18 42530 etransclem46 42558 ioorrnopnlem 42582 sge0iunmptlemre 42690 itscnhlinecirc02p 44765 |
Copyright terms: Public domain | W3C validator |