![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpregt0 | Structured version Visualization version GIF version |
Description: A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
Ref | Expression |
---|---|
rpregt0 | ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp 13016 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
2 | 1 | biimpi 215 | 1 ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 class class class wbr 5149 ℝcr 11144 0cc0 11145 < clt 11285 ℝ+crp 13014 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-rp 13015 |
This theorem is referenced by: rpne0 13030 divlt1lt 13083 divle1le 13084 ledivge1le 13085 nnledivrp 13126 modge0 13885 modlt 13886 modid 13902 modmuladdnn0 13921 expnlbnd 14236 o1fsum 15800 isprm6 16693 gexexlem 19824 lmnn 25240 aaliou2b 26326 harmonicbnd4 26993 logfaclbnd 27205 logfacrlim 27207 chto1ub 27459 vmadivsum 27465 dchrmusumlema 27476 dchrvmasumlem2 27481 dchrisum0lem2a 27500 dchrisum0lem2 27501 dchrisum0lem3 27502 mulogsumlem 27514 mulog2sumlem2 27518 selberg2lem 27533 selberg3lem1 27540 pntrmax 27547 pntrsumo1 27548 pntibndlem3 27575 divge1b 47768 divgt1b 47769 |
Copyright terms: Public domain | W3C validator |