Theorem rpregt0d 12932

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2110   class class class wbr 5089  ℝcr 10997  0cc0 10998   < clt 11138  ℝ⁺crp 12882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-rp 12883

This theorem is referenced by:  reclt1d  12939  recgt1d  12940  ltrecd  12944  lerecd  12945  ltrec1d  12946  lerec2d  12947  lediv2ad  12948  ltdiv2d  12949  lediv2d  12950  ledivdivd  12951  divge0d  12966  ltmul1d  12967  ltmul2d  12968  lemul1d  12969  lemul2d  12970  ltdiv1d  12971  lediv1d  12972  ltmuldivd  12973  ltmuldiv2d  12974  lemuldivd  12975  lemuldiv2d  12976  ltdivmuld  12977  ltdivmul2d  12978  ledivmuld  12979  ledivmul2d  12980  ltdiv23d  12993  lediv23d  12994  lt2mul2divd  12995  mertenslem1  15783  isprm6  16617  nmoi  24636  icopnfhmeo  24861  nmoleub2lem3  25035  lmnn  25183  ovolscalem1  25434  aaliou2b  26269  birthdaylem3  26883  fsumharmonic  26942  bcmono  27208  chtppilim  27406  dchrisum0lem1a  27417  dchrvmasumiflem1  27432  dchrisum0lem1b  27446  dchrisum0lem1  27447  mulog2sumlem2  27466  selberg3lem1  27488  pntrsumo1  27496  pntibndlem1  27520  pntibndlem3  27523  pntlemr  27533  pntlemj  27534  ostth3  27569  minvecolem3  30846  lnconi  32003  poimirlem29  37668  poimirlem30  37669  poimirlem31  37670  poimirlem32  37671  aks4d1p1p2  42082  stoweidlem14  46031  stoweidlem34  46051  stoweidlem42  46059  stoweidlem51  46068  stoweidlem59  46076  stirlinglem5  46095  elbigolo1  48568