Theorem rpregt0d 12992

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11037  0cc0 11038   < clt 11179  ℝ⁺crp 12942

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12943

This theorem is referenced by:  reclt1d  12999  recgt1d  13000  ltrecd  13004  lerecd  13005  ltrec1d  13006  lerec2d  13007  lediv2ad  13008  ltdiv2d  13009  lediv2d  13010  ledivdivd  13011  divge0d  13026  ltmul1d  13027  ltmul2d  13028  lemul1d  13029  lemul2d  13030  ltdiv1d  13031  lediv1d  13032  ltmuldivd  13033  ltmuldiv2d  13034  lemuldivd  13035  lemuldiv2d  13036  ltdivmuld  13037  ltdivmul2d  13038  ledivmuld  13039  ledivmul2d  13040  ltdiv23d  13053  lediv23d  13054  lt2mul2divd  13055  mertenslem1  15849  isprm6  16684  nmoi  24693  icopnfhmeo  24910  nmoleub2lem3  25082  lmnn  25230  ovolscalem1  25480  aaliou2b  26307  birthdaylem3  26917  fsumharmonic  26975  bcmono  27240  chtppilim  27438  dchrisum0lem1a  27449  dchrvmasumiflem1  27464  dchrisum0lem1b  27478  dchrisum0lem1  27479  mulog2sumlem2  27498  selberg3lem1  27520  pntrsumo1  27528  pntibndlem1  27552  pntibndlem3  27555  pntlemr  27565  pntlemj  27566  ostth3  27601  minvecolem3  30947  lnconi  32104  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  aks4d1p1p2  42509  stoweidlem14  46442  stoweidlem34  46462  stoweidlem42  46470  stoweidlem51  46479  stoweidlem59  46487  stirlinglem5  46506  elbigolo1  49027