![]() |
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 13034 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 711 | 1 ⊢ 𝐴 ∈ ℝ+ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 class class class wbr 5148 ℝcr 11152 0cc0 11153 < clt 11293 ℝ+crp 13032 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-rp 13033 |
This theorem is referenced by: 1rp 13036 2rp 13037 3rp 13038 5rp 13039 iexpcyc 14243 discr 14276 epr 16241 aaliou3lem1 26399 aaliou3lem2 26400 aaliou3lem3 26401 pirp 26518 pigt3 26575 efif1olem2 26600 cxpsqrtlem 26759 log2cnv 27002 chtublem 27270 chtub 27271 bposlem6 27348 lgsdir2lem1 27384 lgsdir2lem4 27387 lgsdir2lem5 27388 2sqlem11 27488 chebbnd1lem3 27530 chebbnd1 27531 pntlemg 27657 pntlemr 27661 pntlemf 27664 minvecolem3 30905 dp2lt10 32851 ballotlem2 34470 cntotbnd 37783 heiborlem5 37802 heiborlem7 37804 4rp 42313 6rp 42314 7rp 42315 8rp 42316 9rp 42317 isosctrlem1ALT 44932 sineq0ALT 44935 limclner 45607 stoweidlem5 45961 stoweidlem28 45984 stoweidlem59 46015 stoweid 46019 stirlinglem12 46041 fourierswlem 46186 fouriersw 46187 |
Copyright terms: Public domain | W3C validator |