Theorem rpregt0d 13021

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5148  ℝcr 11108  0cc0 11109   < clt 11247  ℝ⁺crp 12973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-rp 12974

This theorem is referenced by:  reclt1d  13028  recgt1d  13029  ltrecd  13033  lerecd  13034  ltrec1d  13035  lerec2d  13036  lediv2ad  13037  ltdiv2d  13038  lediv2d  13039  ledivdivd  13040  divge0d  13055  ltmul1d  13056  ltmul2d  13057  lemul1d  13058  lemul2d  13059  ltdiv1d  13060  lediv1d  13061  ltmuldivd  13062  ltmuldiv2d  13063  lemuldivd  13064  lemuldiv2d  13065  ltdivmuld  13066  ltdivmul2d  13067  ledivmuld  13068  ledivmul2d  13069  ltdiv23d  13082  lediv23d  13083  lt2mul2divd  13084  mertenslem1  15829  isprm6  16650  nmoi  24244  icopnfhmeo  24458  nmoleub2lem3  24630  lmnn  24779  ovolscalem1  25029  aaliou2b  25853  birthdaylem3  26455  fsumharmonic  26513  bcmono  26777  chtppilim  26975  dchrisum0lem1a  26986  dchrvmasumiflem1  27001  dchrisum0lem1b  27015  dchrisum0lem1  27016  mulog2sumlem2  27035  selberg3lem1  27057  pntrsumo1  27065  pntibndlem1  27089  pntibndlem3  27092  pntlemr  27102  pntlemj  27103  ostth3  27138  minvecolem3  30124  lnconi  31281  poimirlem29  36512  poimirlem30  36513  poimirlem31  36514  poimirlem32  36515  aks4d1p1p2  40930  stoweidlem14  44720  stoweidlem34  44740  stoweidlem42  44748  stoweidlem51  44757  stoweidlem59  44765  stirlinglem5  44784  elbigolo1  47233