Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrpii | Structured version Visualization version GIF version |
Description: Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.) |
Ref | Expression |
---|---|
elrpi.1 | ⊢ 𝐴 ∈ ℝ |
elrpi.2 | ⊢ 0 < 𝐴 |
Ref | Expression |
---|---|
elrpii | ⊢ 𝐴 ∈ ℝ+ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrpi.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
2 | elrpi.2 | . 2 ⊢ 0 < 𝐴 | |
3 | elrp 12379 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 707 | 1 ⊢ 𝐴 ∈ ℝ+ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 class class class wbr 5057 ℝcr 10524 0cc0 10525 < clt 10663 ℝ+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-3an 1081 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-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-rp 12378 |
This theorem is referenced by: 1rp 12381 2rp 12382 3rp 12383 iexpcyc 13557 discr 13589 epr 15549 aaliou3lem1 24858 aaliou3lem2 24859 aaliou3lem3 24860 pirp 24974 pigt3 25030 efif1olem2 25054 cxpsqrtlem 25212 log2cnv 25449 chtublem 25714 chtub 25715 bposlem6 25792 lgsdir2lem1 25828 lgsdir2lem4 25831 lgsdir2lem5 25832 2sqlem11 25932 chebbnd1lem3 25974 chebbnd1 25975 pntlemg 26101 pntlemr 26105 pntlemf 26108 minvecolem3 28580 dp2lt10 30487 ballotlem2 31645 cntotbnd 34955 heiborlem5 34974 heiborlem7 34976 isosctrlem1ALT 41145 sineq0ALT 41148 limclner 41808 stoweidlem5 42167 stoweidlem28 42190 stoweidlem59 42221 stoweid 42225 stirlinglem12 42247 fourierswlem 42392 fouriersw 42393 |
Copyright terms: Public domain | W3C validator |