![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpxrd | Structured version Visualization version GIF version |
Description: A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rpred.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
Ref | Expression |
---|---|
rpxrd | ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpred.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+) | |
2 | 1 | rpred 12181 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | rexrd 10426 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ℝ*cxr 10410 ℝ+crp 12137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-un 3797 df-in 3799 df-ss 3806 df-xr 10415 df-rp 12138 |
This theorem is referenced by: ssblex 22641 metequiv2 22723 metss2lem 22724 methaus 22733 met1stc 22734 met2ndci 22735 metcnp 22754 metcnpi3 22759 metustexhalf 22769 blval2 22775 metuel2 22778 nmoi2 22942 metdcnlem 23047 metdscnlem 23066 metnrmlem2 23071 metnrmlem3 23072 cnheibor 23162 cnllycmp 23163 lebnumlem3 23170 nmoleub2lem 23321 nmhmcn 23327 iscfil2 23472 cfil3i 23475 iscfil3 23479 iscmet3lem2 23498 caubl 23514 caublcls 23515 relcmpcmet 23524 bcthlem2 23531 bcthlem4 23533 bcthlem5 23534 ellimc3 24080 ftc1a 24237 ulmdvlem1 24591 psercnlem2 24615 psercn 24617 pserdvlem2 24619 pserdv 24620 efopn 24841 logccv 24846 efrlim 25148 lgamucov 25216 ftalem3 25253 logexprlim 25402 pntpbnd1a 25726 pntleme 25749 pntlem3 25750 pntleml 25752 ubthlem1 28298 ubthlem2 28299 tpr2rico 30556 xrmulc1cn 30574 omssubadd 30960 sgnmulrp2 31204 ptrecube 34037 poimirlem29 34066 heicant 34072 ftc1anclem6 34117 ftc1anclem7 34118 sstotbnd2 34199 equivtotbnd 34203 totbndbnd 34214 cntotbnd 34221 heibor1lem 34234 heiborlem3 34238 heiborlem6 34241 heiborlem8 34243 supxrge 40466 infrpge 40479 infleinflem1 40498 stoweid 41211 qndenserrnbl 41443 sge0rpcpnf 41566 sge0xaddlem1 41578 |
Copyright terms: Public domain | W3C validator |