Theorem rpregt0d 13022

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109  0cc0 11110   < clt 11248  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12975

This theorem is referenced by:  reclt1d  13029  recgt1d  13030  ltrecd  13034  lerecd  13035  ltrec1d  13036  lerec2d  13037  lediv2ad  13038  ltdiv2d  13039  lediv2d  13040  ledivdivd  13041  divge0d  13056  ltmul1d  13057  ltmul2d  13058  lemul1d  13059  lemul2d  13060  ltdiv1d  13061  lediv1d  13062  ltmuldivd  13063  ltmuldiv2d  13064  lemuldivd  13065  lemuldiv2d  13066  ltdivmuld  13067  ltdivmul2d  13068  ledivmuld  13069  ledivmul2d  13070  ltdiv23d  13083  lediv23d  13084  lt2mul2divd  13085  mertenslem1  15830  isprm6  16651  nmoi  24245  icopnfhmeo  24459  nmoleub2lem3  24631  lmnn  24780  ovolscalem1  25030  aaliou2b  25854  birthdaylem3  26458  fsumharmonic  26516  bcmono  26780  chtppilim  26978  dchrisum0lem1a  26989  dchrvmasumiflem1  27004  dchrisum0lem1b  27018  dchrisum0lem1  27019  mulog2sumlem2  27038  selberg3lem1  27060  pntrsumo1  27068  pntibndlem1  27092  pntibndlem3  27095  pntlemr  27105  pntlemj  27106  ostth3  27141  minvecolem3  30129  lnconi  31286  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  aks4d1p1p2  40935  stoweidlem14  44730  stoweidlem34  44750  stoweidlem42  44758  stoweidlem51  44767  stoweidlem59  44775  stirlinglem5  44794  elbigolo1  47243