Theorem rpregt0d 13084

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

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