![]() |
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 13075 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1 | rpgt0d 13078 | . 2 ⊢ (𝜑 → 0 < 𝐴) |
4 | 2, 3 | jca 511 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2106 class class class wbr 5148 ℝcr 11152 0cc0 11153 < clt 11293 ℝ+crp 13032 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-rp 13033 |
This theorem is referenced by: reclt1d 13088 recgt1d 13089 ltrecd 13093 lerecd 13094 ltrec1d 13095 lerec2d 13096 lediv2ad 13097 ltdiv2d 13098 lediv2d 13099 ledivdivd 13100 divge0d 13115 ltmul1d 13116 ltmul2d 13117 lemul1d 13118 lemul2d 13119 ltdiv1d 13120 lediv1d 13121 ltmuldivd 13122 ltmuldiv2d 13123 lemuldivd 13124 lemuldiv2d 13125 ltdivmuld 13126 ltdivmul2d 13127 ledivmuld 13128 ledivmul2d 13129 ltdiv23d 13142 lediv23d 13143 lt2mul2divd 13144 mertenslem1 15917 isprm6 16748 nmoi 24765 icopnfhmeo 24988 nmoleub2lem3 25162 lmnn 25311 ovolscalem1 25562 aaliou2b 26398 birthdaylem3 27011 fsumharmonic 27070 bcmono 27336 chtppilim 27534 dchrisum0lem1a 27545 dchrvmasumiflem1 27560 dchrisum0lem1b 27574 dchrisum0lem1 27575 mulog2sumlem2 27594 selberg3lem1 27616 pntrsumo1 27624 pntibndlem1 27648 pntibndlem3 27651 pntlemr 27661 pntlemj 27662 ostth3 27697 minvecolem3 30905 lnconi 32062 poimirlem29 37636 poimirlem30 37637 poimirlem31 37638 poimirlem32 37639 aks4d1p1p2 42052 stoweidlem14 45970 stoweidlem34 45990 stoweidlem42 45998 stoweidlem51 46007 stoweidlem59 46015 stirlinglem5 46034 elbigolo1 48407 |
Copyright terms: Public domain | W3C validator |