|   | 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 13078 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 3 | 1 | rpgt0d 13081 | . 2 ⊢ (𝜑 → 0 < 𝐴) | 
| 4 | 2, 3 | jca 511 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 class class class wbr 5142 ℝcr 11155 0cc0 11156 < clt 11296 ℝ+crp 13035 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 df-rp 13036 | 
| This theorem is referenced by: reclt1d 13091 recgt1d 13092 ltrecd 13096 lerecd 13097 ltrec1d 13098 lerec2d 13099 lediv2ad 13100 ltdiv2d 13101 lediv2d 13102 ledivdivd 13103 divge0d 13118 ltmul1d 13119 ltmul2d 13120 lemul1d 13121 lemul2d 13122 ltdiv1d 13123 lediv1d 13124 ltmuldivd 13125 ltmuldiv2d 13126 lemuldivd 13127 lemuldiv2d 13128 ltdivmuld 13129 ltdivmul2d 13130 ledivmuld 13131 ledivmul2d 13132 ltdiv23d 13145 lediv23d 13146 lt2mul2divd 13147 mertenslem1 15921 isprm6 16752 nmoi 24750 icopnfhmeo 24975 nmoleub2lem3 25149 lmnn 25298 ovolscalem1 25549 aaliou2b 26384 birthdaylem3 26997 fsumharmonic 27056 bcmono 27322 chtppilim 27520 dchrisum0lem1a 27531 dchrvmasumiflem1 27546 dchrisum0lem1b 27560 dchrisum0lem1 27561 mulog2sumlem2 27580 selberg3lem1 27602 pntrsumo1 27610 pntibndlem1 27634 pntibndlem3 27637 pntlemr 27647 pntlemj 27648 ostth3 27683 minvecolem3 30896 lnconi 32053 poimirlem29 37657 poimirlem30 37658 poimirlem31 37659 poimirlem32 37660 aks4d1p1p2 42072 stoweidlem14 46034 stoweidlem34 46054 stoweidlem42 46062 stoweidlem51 46071 stoweidlem59 46079 stirlinglem5 46098 elbigolo1 48483 | 
| Copyright terms: Public domain | W3C validator |