Theorem rpregt0d 13057

Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpregt0d	⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem rpregt0d

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 13051	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1	rpgt0d 13054	. 2 ⊢ (𝜑 → 0 < 𝐴)
4	2, 3	jca 520	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   class class class wbr 5105  ℝcr 11087  0cc0 11088   < clt 11231  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-rp 13008

This theorem is referenced by:  reclt1d  13064  recgt1d  13065  ltrecd  13069  lerecd  13070  ltrec1d  13071  lerec2d  13072  lediv2ad  13073  ltdiv2d  13074  lediv2d  13075  ledivdivd  13076  divge0d  13091  ltmul1d  13092  ltmul2d  13093  lemul1d  13094  lemul2d  13095  ltdiv1d  13096  lediv1d  13097  ltmuldivd  13098  ltmuldiv2d  13099  lemuldivd  13100  lemuldiv2d  13101  ltdivmuld  13102  ltdivmul2d  13103  ledivmuld  13104  ledivmul2d  13105  ltdiv23d  13118  lediv23d  13119  lt2mul2divd  13120  mertenslem1  15928  isprm6  16763  nmoi  24846  icopnfhmeo  25063  nmoleub2lem3  25235  lmnn  25383  ovolscalem1  25633  aaliou2b  26463  birthdaylem3  27076  fsumharmonic  27134  bcmono  27399  chtppilim  27597  dchrisum0lem1a  27608  dchrvmasumiflem1  27623  dchrisum0lem1b  27637  dchrisum0lem1  27638  mulog2sumlem2  27657  selberg3lem1  27679  pntrsumo1  27687  pntibndlem1  27711  pntibndlem3  27714  pntlemr  27724  pntlemj  27725  ostth3  27760  minvecolem3  31137  lnconi  32294  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  aks4d1p1p2  42699  stoweidlem14  46586  stoweidlem34  46606  stoweidlem42  46614  stoweidlem51  46623  stoweidlem59  46631  stirlinglem5  46650  elbigolo1  49188