Theorem rpregt0d 12943

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008  0cc0 11009   < clt 11149  ℝ⁺crp 12893

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-rp 12894

This theorem is referenced by:  reclt1d  12950  recgt1d  12951  ltrecd  12955  lerecd  12956  ltrec1d  12957  lerec2d  12958  lediv2ad  12959  ltdiv2d  12960  lediv2d  12961  ledivdivd  12962  divge0d  12977  ltmul1d  12978  ltmul2d  12979  lemul1d  12980  lemul2d  12981  ltdiv1d  12982  lediv1d  12983  ltmuldivd  12984  ltmuldiv2d  12985  lemuldivd  12986  lemuldiv2d  12987  ltdivmuld  12988  ltdivmul2d  12989  ledivmuld  12990  ledivmul2d  12991  ltdiv23d  13004  lediv23d  13005  lt2mul2divd  13006  mertenslem1  15791  isprm6  16625  nmoi  24614  icopnfhmeo  24839  nmoleub2lem3  25013  lmnn  25161  ovolscalem1  25412  aaliou2b  26247  birthdaylem3  26861  fsumharmonic  26920  bcmono  27186  chtppilim  27384  dchrisum0lem1a  27395  dchrvmasumiflem1  27410  dchrisum0lem1b  27424  dchrisum0lem1  27425  mulog2sumlem2  27444  selberg3lem1  27466  pntrsumo1  27474  pntibndlem1  27498  pntibndlem3  27501  pntlemr  27511  pntlemj  27512  ostth3  27547  minvecolem3  30824  lnconi  31981  poimirlem29  37649  poimirlem30  37650  poimirlem31  37651  poimirlem32  37652  aks4d1p1p2  42063  stoweidlem14  46015  stoweidlem34  46035  stoweidlem42  46043  stoweidlem51  46052  stoweidlem59  46060  stirlinglem5  46079  elbigolo1  48562