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 12732 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 708 | 1 ⊢ 𝐴 ∈ ℝ+ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 class class class wbr 5074 ℝcr 10870 0cc0 10871 < clt 11009 ℝ+crp 12730 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-rp 12731 |
This theorem is referenced by: 1rp 12734 2rp 12735 3rp 12736 iexpcyc 13923 discr 13955 epr 15917 aaliou3lem1 25502 aaliou3lem2 25503 aaliou3lem3 25504 pirp 25618 pigt3 25674 efif1olem2 25699 cxpsqrtlem 25857 log2cnv 26094 chtublem 26359 chtub 26360 bposlem6 26437 lgsdir2lem1 26473 lgsdir2lem4 26476 lgsdir2lem5 26477 2sqlem11 26577 chebbnd1lem3 26619 chebbnd1 26620 pntlemg 26746 pntlemr 26750 pntlemf 26753 minvecolem3 29238 dp2lt10 31158 ballotlem2 32455 cntotbnd 35954 heiborlem5 35973 heiborlem7 35975 isosctrlem1ALT 42554 sineq0ALT 42557 limclner 43192 stoweidlem5 43546 stoweidlem28 43569 stoweidlem59 43600 stoweid 43604 stirlinglem12 43626 fourierswlem 43771 fouriersw 43772 |
Copyright terms: Public domain | W3C validator |