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 12419 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | rexrd 10679 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ℝ*cxr 10662 ℝ+crp 12377 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-un 3938 df-in 3940 df-ss 3949 df-xr 10667 df-rp 12378 |
This theorem is referenced by: ssblex 22965 metequiv2 23047 metss2lem 23048 methaus 23057 met1stc 23058 met2ndci 23059 metcnp 23078 metcnpi3 23083 metustexhalf 23093 blval2 23099 metuel2 23102 nmoi2 23266 metdcnlem 23371 metdscnlem 23390 metnrmlem2 23395 metnrmlem3 23396 cnheibor 23486 cnllycmp 23487 lebnumlem3 23494 nmoleub2lem 23645 nmhmcn 23651 iscfil2 23796 cfil3i 23799 iscfil3 23803 cfilfcls 23804 iscmet3lem2 23822 caubl 23838 caublcls 23839 relcmpcmet 23848 bcthlem2 23855 bcthlem4 23857 bcthlem5 23858 ellimc3 24404 ftc1a 24561 ulmdvlem1 24915 psercnlem2 24939 psercn 24941 pserdvlem2 24943 pserdv 24944 efopn 25168 logccv 25173 efrlim 25474 lgamucov 25542 ftalem3 25579 logexprlim 25728 pntpbnd1a 26088 pntleme 26111 pntlem3 26112 pntleml 26114 ubthlem1 28574 ubthlem2 28575 tpr2rico 31054 xrmulc1cn 31072 omssubadd 31457 sgnmulrp2 31700 ptrecube 34773 poimirlem29 34802 heicant 34808 ftc1anclem6 34853 ftc1anclem7 34854 sstotbnd2 34933 equivtotbnd 34937 totbndbnd 34948 cntotbnd 34955 heibor1lem 34968 heiborlem3 34972 heiborlem6 34975 heiborlem8 34977 supxrge 41482 infrpge 41495 infleinflem1 41514 stoweid 42225 qndenserrnbl 42457 sge0rpcpnf 42580 sge0xaddlem1 42592 |
Copyright terms: Public domain | W3C validator |