![]() |
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 12075 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | rexrd 10295 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2145 ℝ*cxr 10279 ℝ+crp 12035 |
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 837 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 3728 df-in 3730 df-ss 3737 df-xr 10284 df-rp 12036 |
This theorem is referenced by: ssblex 22453 metequiv2 22535 metss2lem 22536 methaus 22545 met1stc 22546 met2ndci 22547 metcnp 22566 metcnpi3 22571 metustexhalf 22581 blval2 22587 metuel2 22590 nmoi2 22754 metdcnlem 22859 metdscnlem 22878 metnrmlem2 22883 metnrmlem3 22884 cnheibor 22974 cnllycmp 22975 lebnumlem3 22982 nmoleub2lem 23133 nmhmcn 23139 iscfil2 23283 cfil3i 23286 iscfil3 23290 iscmet3lem2 23309 caubl 23325 caublcls 23326 relcmpcmet 23334 bcthlem2 23341 bcthlem4 23343 bcthlem5 23344 ellimc3 23863 ftc1a 24020 ulmdvlem1 24374 psercnlem2 24398 psercn 24400 pserdvlem2 24402 pserdv 24403 efopn 24625 logccv 24630 efrlim 24917 lgamucov 24985 ftalem3 25022 logexprlim 25171 pntpbnd1a 25495 pntleme 25518 pntlem3 25519 pntleml 25521 ubthlem1 28066 ubthlem2 28067 tpr2rico 30298 xrmulc1cn 30316 omssubadd 30702 sgnmulrp2 30945 ptrecube 33741 poimirlem29 33770 heicant 33776 ftc1anclem6 33821 ftc1anclem7 33822 sstotbnd2 33903 equivtotbnd 33907 totbndbnd 33918 cntotbnd 33925 heibor1lem 33938 heiborlem3 33942 heiborlem6 33945 heiborlem8 33947 supxrge 40065 infrpge 40078 infleinflem1 40097 stoweid 40792 qndenserrnbl 41027 sge0rpcpnf 41150 sge0xaddlem1 41162 |
Copyright terms: Public domain | W3C validator |