Theorem rpregt0d 12707

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 12701	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1	rpgt0d 12704	. 2 ⊢ (𝜑 → 0 < 𝐴)
4	2, 3	jca 511	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801  0cc0 10802   < clt 10940  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-rp 12660

This theorem is referenced by:  reclt1d  12714  recgt1d  12715  ltrecd  12719  lerecd  12720  ltrec1d  12721  lerec2d  12722  lediv2ad  12723  ltdiv2d  12724  lediv2d  12725  ledivdivd  12726  divge0d  12741  ltmul1d  12742  ltmul2d  12743  lemul1d  12744  lemul2d  12745  ltdiv1d  12746  lediv1d  12747  ltmuldivd  12748  ltmuldiv2d  12749  lemuldivd  12750  lemuldiv2d  12751  ltdivmuld  12752  ltdivmul2d  12753  ledivmuld  12754  ledivmul2d  12755  ltdiv23d  12768  lediv23d  12769  lt2mul2divd  12770  mertenslem1  15524  isprm6  16347  nmoi  23798  icopnfhmeo  24012  nmoleub2lem3  24184  lmnn  24332  ovolscalem1  24582  aaliou2b  25406  birthdaylem3  26008  fsumharmonic  26066  bcmono  26330  chtppilim  26528  dchrisum0lem1a  26539  dchrvmasumiflem1  26554  dchrisum0lem1b  26568  dchrisum0lem1  26569  mulog2sumlem2  26588  selberg3lem1  26610  pntrsumo1  26618  pntibndlem1  26642  pntibndlem3  26645  pntlemr  26655  pntlemj  26656  ostth3  26691  minvecolem3  29139  lnconi  30296  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  aks4d1p1p2  40006  stoweidlem14  43445  stoweidlem34  43465  stoweidlem42  43473  stoweidlem51  43482  stoweidlem59  43490  stirlinglem5  43509  elbigolo1  45791