![]() |
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 13013 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1 | rpgt0d 13016 | . 2 ⊢ (𝜑 → 0 < 𝐴) |
4 | 2, 3 | jca 511 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2098 class class class wbr 5138 ℝcr 11105 0cc0 11106 < clt 11245 ℝ+crp 12971 |
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 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-br 5139 df-rp 12972 |
This theorem is referenced by: reclt1d 13026 recgt1d 13027 ltrecd 13031 lerecd 13032 ltrec1d 13033 lerec2d 13034 lediv2ad 13035 ltdiv2d 13036 lediv2d 13037 ledivdivd 13038 divge0d 13053 ltmul1d 13054 ltmul2d 13055 lemul1d 13056 lemul2d 13057 ltdiv1d 13058 lediv1d 13059 ltmuldivd 13060 ltmuldiv2d 13061 lemuldivd 13062 lemuldiv2d 13063 ltdivmuld 13064 ltdivmul2d 13065 ledivmuld 13066 ledivmul2d 13067 ltdiv23d 13080 lediv23d 13081 lt2mul2divd 13082 mertenslem1 15827 isprm6 16648 nmoi 24567 icopnfhmeo 24790 nmoleub2lem3 24964 lmnn 25113 ovolscalem1 25364 aaliou2b 26195 birthdaylem3 26801 fsumharmonic 26860 bcmono 27126 chtppilim 27324 dchrisum0lem1a 27335 dchrvmasumiflem1 27350 dchrisum0lem1b 27364 dchrisum0lem1 27365 mulog2sumlem2 27384 selberg3lem1 27406 pntrsumo1 27414 pntibndlem1 27438 pntibndlem3 27441 pntlemr 27451 pntlemj 27452 ostth3 27487 minvecolem3 30598 lnconi 31755 poimirlem29 37007 poimirlem30 37008 poimirlem31 37009 poimirlem32 37010 aks4d1p1p2 41428 stoweidlem14 45215 stoweidlem34 45235 stoweidlem42 45243 stoweidlem51 45252 stoweidlem59 45260 stirlinglem5 45279 elbigolo1 47431 |
Copyright terms: Public domain | W3C validator |