Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rpregt0d | Structured version Visualization version GIF version |
Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rpred.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
Ref | Expression |
---|---|
rpregt0d | ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpred.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+) | |
2 | 1 | rpred 12425 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1 | rpgt0d 12428 | . 2 ⊢ (𝜑 → 0 < 𝐴) |
4 | 2, 3 | jca 514 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2110 class class class wbr 5058 ℝcr 10530 0cc0 10531 < clt 10669 ℝ+crp 12383 |
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 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-br 5059 df-rp 12384 |
This theorem is referenced by: reclt1d 12438 recgt1d 12439 ltrecd 12443 lerecd 12444 ltrec1d 12445 lerec2d 12446 lediv2ad 12447 ltdiv2d 12448 lediv2d 12449 ledivdivd 12450 divge0d 12465 ltmul1d 12466 ltmul2d 12467 lemul1d 12468 lemul2d 12469 ltdiv1d 12470 lediv1d 12471 ltmuldivd 12472 ltmuldiv2d 12473 lemuldivd 12474 lemuldiv2d 12475 ltdivmuld 12476 ltdivmul2d 12477 ledivmuld 12478 ledivmul2d 12479 ltdiv23d 12492 lediv23d 12493 lt2mul2divd 12494 mertenslem1 15234 isprm6 16052 nmoi 23331 icopnfhmeo 23541 nmoleub2lem3 23713 lmnn 23860 ovolscalem1 24108 aaliou2b 24924 birthdaylem3 25525 fsumharmonic 25583 bcmono 25847 chtppilim 26045 dchrisum0lem1a 26056 dchrvmasumiflem1 26071 dchrisum0lem1b 26085 dchrisum0lem1 26086 mulog2sumlem2 26105 selberg3lem1 26127 pntrsumo1 26135 pntibndlem1 26159 pntibndlem3 26162 pntlemr 26172 pntlemj 26173 ostth3 26208 minvecolem3 28647 lnconi 29804 poimirlem29 34915 poimirlem30 34916 poimirlem31 34917 poimirlem32 34918 stoweidlem14 42293 stoweidlem34 42313 stoweidlem42 42321 stoweidlem51 42330 stoweidlem59 42338 stirlinglem5 42357 elbigolo1 44611 |
Copyright terms: Public domain | W3C validator |