| 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 13077 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 3 | 2 | rexrd 11311 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ℝ*cxr 11294 ℝ+crp 13034 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-un 3956 df-ss 3968 df-xr 11299 df-rp 13035 |
| This theorem is referenced by: ssblex 24438 metequiv2 24523 metss2lem 24524 methaus 24533 met1stc 24534 met2ndci 24535 metcnp 24554 metcnpi3 24559 metustexhalf 24569 blval2 24575 metuel2 24578 nmoi2 24751 metdcnlem 24858 metdscnlem 24877 metnrmlem2 24882 metnrmlem3 24883 cnheibor 24987 cnllycmp 24988 lebnumlem3 24995 nmoleub2lem 25147 nmhmcn 25153 iscfil2 25300 cfil3i 25303 iscfil3 25307 cfilfcls 25308 iscmet3lem2 25326 caubl 25342 caublcls 25343 relcmpcmet 25352 bcthlem2 25359 bcthlem4 25361 bcthlem5 25362 ellimc3 25914 ftc1a 26078 ulmdvlem1 26443 psercnlem2 26468 psercn 26470 pserdvlem2 26472 pserdv 26473 efopn 26700 logccv 26705 efrlim 27012 efrlimOLD 27013 lgamucov 27081 ftalem3 27118 logexprlim 27269 pntpbnd1a 27629 pntleme 27652 pntlem3 27653 pntleml 27655 ubthlem1 30889 ubthlem2 30890 tpr2rico 33911 xrmulc1cn 33929 omssubadd 34302 sgnmulrp2 34546 ptrecube 37627 poimirlem29 37656 heicant 37662 ftc1anclem6 37705 ftc1anclem7 37706 sstotbnd2 37781 equivtotbnd 37785 totbndbnd 37796 cntotbnd 37803 heibor1lem 37816 heiborlem3 37820 heiborlem6 37823 heiborlem8 37825 supxrge 45349 infrpge 45362 infleinflem1 45381 stoweid 46078 qndenserrnbl 46310 sge0rpcpnf 46436 sge0xaddlem1 46448 |
| Copyright terms: Public domain | W3C validator |