![]() |
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 12156 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1 | rpgt0d 12159 | . 2 ⊢ (𝜑 → 0 < 𝐴) |
4 | 2, 3 | jca 507 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2164 class class class wbr 4873 ℝcr 10251 0cc0 10252 < clt 10391 ℝ+crp 12112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-br 4874 df-rp 12113 |
This theorem is referenced by: reclt1d 12169 recgt1d 12170 ltrecd 12174 lerecd 12175 ltrec1d 12176 lerec2d 12177 lediv2ad 12178 ltdiv2d 12179 lediv2d 12180 ledivdivd 12181 divge0d 12196 ltmul1d 12197 ltmul2d 12198 lemul1d 12199 lemul2d 12200 ltdiv1d 12201 lediv1d 12202 ltmuldivd 12203 ltmuldiv2d 12204 lemuldivd 12205 lemuldiv2d 12206 ltdivmuld 12207 ltdivmul2d 12208 ledivmuld 12209 ledivmul2d 12210 ltdiv23d 12223 lediv23d 12224 lt2mul2divd 12225 mertenslem1 14989 isprm6 15797 nmoi 22902 icopnfhmeo 23112 nmoleub2lem3 23284 lmnn 23431 ovolscalem1 23679 aaliou2b 24495 birthdaylem3 25093 fsumharmonic 25151 bcmono 25415 chtppilim 25577 dchrisum0lem1a 25588 dchrvmasumiflem1 25603 dchrisum0lem1b 25617 dchrisum0lem1 25618 mulog2sumlem2 25637 selberg3lem1 25659 pntrsumo1 25667 pntibndlem1 25691 pntibndlem3 25694 pntlemr 25704 pntlemj 25705 ostth3 25740 minvecolem3 28276 lnconi 29436 poimirlem29 33975 poimirlem30 33976 poimirlem31 33977 poimirlem32 33978 stoweidlem14 41018 stoweidlem34 41038 stoweidlem42 41046 stoweidlem51 41055 stoweidlem59 41063 stirlinglem5 41082 elbigolo1 43191 |
Copyright terms: Public domain | W3C validator |