Theorem rpregt0d 13008

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075   < clt 11215  ℝ⁺crp 12958

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-rp 12959

This theorem is referenced by:  reclt1d  13015  recgt1d  13016  ltrecd  13020  lerecd  13021  ltrec1d  13022  lerec2d  13023  lediv2ad  13024  ltdiv2d  13025  lediv2d  13026  ledivdivd  13027  divge0d  13042  ltmul1d  13043  ltmul2d  13044  lemul1d  13045  lemul2d  13046  ltdiv1d  13047  lediv1d  13048  ltmuldivd  13049  ltmuldiv2d  13050  lemuldivd  13051  lemuldiv2d  13052  ltdivmuld  13053  ltdivmul2d  13054  ledivmuld  13055  ledivmul2d  13056  ltdiv23d  13069  lediv23d  13070  lt2mul2divd  13071  mertenslem1  15857  isprm6  16691  nmoi  24623  icopnfhmeo  24848  nmoleub2lem3  25022  lmnn  25170  ovolscalem1  25421  aaliou2b  26256  birthdaylem3  26870  fsumharmonic  26929  bcmono  27195  chtppilim  27393  dchrisum0lem1a  27404  dchrvmasumiflem1  27419  dchrisum0lem1b  27433  dchrisum0lem1  27434  mulog2sumlem2  27453  selberg3lem1  27475  pntrsumo1  27483  pntibndlem1  27507  pntibndlem3  27510  pntlemr  27520  pntlemj  27521  ostth3  27556  minvecolem3  30812  lnconi  31969  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  aks4d1p1p2  42065  stoweidlem14  46019  stoweidlem34  46039  stoweidlem42  46047  stoweidlem51  46056  stoweidlem59  46064  stirlinglem5  46083  elbigolo1  48550