Theorem rpregt0d 13033

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2136   class class class wbr 5094  ℝcr 11062  0cc0 11063   < clt 11206  ℝ⁺crp 12983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-rp 12984

This theorem is referenced by:  reclt1d  13040  recgt1d  13041  ltrecd  13045  lerecd  13046  ltrec1d  13047  lerec2d  13048  lediv2ad  13049  ltdiv2d  13050  lediv2d  13051  ledivdivd  13052  divge0d  13067  ltmul1d  13068  ltmul2d  13069  lemul1d  13070  lemul2d  13071  ltdiv1d  13072  lediv1d  13073  ltmuldivd  13074  ltmuldiv2d  13075  lemuldivd  13076  lemuldiv2d  13077  ltdivmuld  13078  ltdivmul2d  13079  ledivmuld  13080  ledivmul2d  13081  ltdiv23d  13094  lediv23d  13095  lt2mul2divd  13096  mertenslem1  15890  isprm6  16725  nmoi  24761  icopnfhmeo  24978  nmoleub2lem3  25150  lmnn  25298  ovolscalem1  25548  aaliou2b  26375  birthdaylem3  26988  fsumharmonic  27046  bcmono  27311  chtppilim  27509  dchrisum0lem1a  27520  dchrvmasumiflem1  27535  dchrisum0lem1b  27549  dchrisum0lem1  27550  mulog2sumlem2  27569  selberg3lem1  27591  pntrsumo1  27599  pntibndlem1  27623  pntibndlem3  27626  pntlemr  27636  pntlemj  27637  ostth3  27672  minvecolem3  31018  lnconi  32175  poimirlem29  38096  poimirlem30  38097  poimirlem31  38098  poimirlem32  38099  aks4d1p1p2  42635  stoweidlem14  46536  stoweidlem34  46556  stoweidlem42  46564  stoweidlem51  46573  stoweidlem59  46581  stirlinglem5  46600  elbigolo1  49127