Theorem rpregt0d 12787

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879  0cc0 10880   < clt 11018  ℝ⁺crp 12739

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-rp 12740

This theorem is referenced by:  reclt1d  12794  recgt1d  12795  ltrecd  12799  lerecd  12800  ltrec1d  12801  lerec2d  12802  lediv2ad  12803  ltdiv2d  12804  lediv2d  12805  ledivdivd  12806  divge0d  12821  ltmul1d  12822  ltmul2d  12823  lemul1d  12824  lemul2d  12825  ltdiv1d  12826  lediv1d  12827  ltmuldivd  12828  ltmuldiv2d  12829  lemuldivd  12830  lemuldiv2d  12831  ltdivmuld  12832  ltdivmul2d  12833  ledivmuld  12834  ledivmul2d  12835  ltdiv23d  12848  lediv23d  12849  lt2mul2divd  12850  mertenslem1  15605  isprm6  16428  nmoi  23901  icopnfhmeo  24115  nmoleub2lem3  24287  lmnn  24436  ovolscalem1  24686  aaliou2b  25510  birthdaylem3  26112  fsumharmonic  26170  bcmono  26434  chtppilim  26632  dchrisum0lem1a  26643  dchrvmasumiflem1  26658  dchrisum0lem1b  26672  dchrisum0lem1  26673  mulog2sumlem2  26692  selberg3lem1  26714  pntrsumo1  26722  pntibndlem1  26746  pntibndlem3  26749  pntlemr  26759  pntlemj  26760  ostth3  26795  minvecolem3  29247  lnconi  30404  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  aks4d1p1p2  40085  stoweidlem14  43562  stoweidlem34  43582  stoweidlem42  43590  stoweidlem51  43599  stoweidlem59  43607  stirlinglem5  43626  elbigolo1  45914