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 12487 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 711 | 1 ⊢ 𝐴 ∈ ℝ+ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 class class class wbr 5040 ℝcr 10627 0cc0 10628 < clt 10766 ℝ+crp 12485 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-rab 3063 df-v 3402 df-un 3858 df-sn 4527 df-pr 4529 df-op 4533 df-br 5041 df-rp 12486 |
This theorem is referenced by: 1rp 12489 2rp 12490 3rp 12491 iexpcyc 13674 discr 13706 epr 15666 aaliou3lem1 25103 aaliou3lem2 25104 aaliou3lem3 25105 pirp 25219 pigt3 25275 efif1olem2 25300 cxpsqrtlem 25458 log2cnv 25695 chtublem 25960 chtub 25961 bposlem6 26038 lgsdir2lem1 26074 lgsdir2lem4 26077 lgsdir2lem5 26078 2sqlem11 26178 chebbnd1lem3 26220 chebbnd1 26221 pntlemg 26347 pntlemr 26351 pntlemf 26354 minvecolem3 28824 dp2lt10 30746 ballotlem2 32038 cntotbnd 35610 heiborlem5 35629 heiborlem7 35631 isosctrlem1ALT 42133 sineq0ALT 42136 limclner 42775 stoweidlem5 43129 stoweidlem28 43152 stoweidlem59 43183 stoweid 43187 stirlinglem12 43209 fourierswlem 43354 fouriersw 43355 |
Copyright terms: Public domain | W3C validator |