|   | 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 13036 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
| 4 | 1, 2, 3 | mpbir2an 711 | 1 ⊢ 𝐴 ∈ ℝ+ | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∈ wcel 2108 class class class wbr 5143 ℝcr 11154 0cc0 11155 < clt 11295 ℝ+crp 13034 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-rp 13035 | 
| This theorem is referenced by: 1rp 13038 2rp 13039 3rp 13040 5rp 13041 iexpcyc 14246 discr 14279 epr 16244 aaliou3lem1 26384 aaliou3lem2 26385 aaliou3lem3 26386 pirp 26503 pigt3 26560 efif1olem2 26585 cxpsqrtlem 26744 log2cnv 26987 chtublem 27255 chtub 27256 bposlem6 27333 lgsdir2lem1 27369 lgsdir2lem4 27372 lgsdir2lem5 27373 2sqlem11 27473 chebbnd1lem3 27515 chebbnd1 27516 pntlemg 27642 pntlemr 27646 pntlemf 27649 minvecolem3 30895 dp2lt10 32866 ballotlem2 34491 cntotbnd 37803 heiborlem5 37822 heiborlem7 37824 4rp 42334 6rp 42335 7rp 42336 8rp 42337 9rp 42338 isosctrlem1ALT 44954 sineq0ALT 44957 limclner 45666 stoweidlem5 46020 stoweidlem28 46043 stoweidlem59 46074 stoweid 46078 stirlinglem12 46100 fourierswlem 46245 fouriersw 46246 | 
| Copyright terms: Public domain | W3C validator |