Theorem rpregt0d 13001

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067  0cc0 11068   < clt 11208  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-rp 12952

This theorem is referenced by:  reclt1d  13008  recgt1d  13009  ltrecd  13013  lerecd  13014  ltrec1d  13015  lerec2d  13016  lediv2ad  13017  ltdiv2d  13018  lediv2d  13019  ledivdivd  13020  divge0d  13035  ltmul1d  13036  ltmul2d  13037  lemul1d  13038  lemul2d  13039  ltdiv1d  13040  lediv1d  13041  ltmuldivd  13042  ltmuldiv2d  13043  lemuldivd  13044  lemuldiv2d  13045  ltdivmuld  13046  ltdivmul2d  13047  ledivmuld  13048  ledivmul2d  13049  ltdiv23d  13062  lediv23d  13063  lt2mul2divd  13064  mertenslem1  15850  isprm6  16684  nmoi  24616  icopnfhmeo  24841  nmoleub2lem3  25015  lmnn  25163  ovolscalem1  25414  aaliou2b  26249  birthdaylem3  26863  fsumharmonic  26922  bcmono  27188  chtppilim  27386  dchrisum0lem1a  27397  dchrvmasumiflem1  27412  dchrisum0lem1b  27426  dchrisum0lem1  27427  mulog2sumlem2  27446  selberg3lem1  27468  pntrsumo1  27476  pntibndlem1  27500  pntibndlem3  27503  pntlemr  27513  pntlemj  27514  ostth3  27549  minvecolem3  30805  lnconi  31962  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  aks4d1p1p2  42058  stoweidlem14  46012  stoweidlem34  46032  stoweidlem42  46040  stoweidlem51  46049  stoweidlem59  46057  stirlinglem5  46076  elbigolo1  48546