Theorem rpregt0d 13026

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104   class class class wbr 5147  ℝcr 11111  0cc0 11112   < clt 11252  ℝ⁺crp 12978

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-rp 12979

This theorem is referenced by:  reclt1d  13033  recgt1d  13034  ltrecd  13038  lerecd  13039  ltrec1d  13040  lerec2d  13041  lediv2ad  13042  ltdiv2d  13043  lediv2d  13044  ledivdivd  13045  divge0d  13060  ltmul1d  13061  ltmul2d  13062  lemul1d  13063  lemul2d  13064  ltdiv1d  13065  lediv1d  13066  ltmuldivd  13067  ltmuldiv2d  13068  lemuldivd  13069  lemuldiv2d  13070  ltdivmuld  13071  ltdivmul2d  13072  ledivmuld  13073  ledivmul2d  13074  ltdiv23d  13087  lediv23d  13088  lt2mul2divd  13089  mertenslem1  15834  isprm6  16655  nmoi  24465  icopnfhmeo  24688  nmoleub2lem3  24862  lmnn  25011  ovolscalem1  25262  aaliou2b  26090  birthdaylem3  26694  fsumharmonic  26752  bcmono  27016  chtppilim  27214  dchrisum0lem1a  27225  dchrvmasumiflem1  27240  dchrisum0lem1b  27254  dchrisum0lem1  27255  mulog2sumlem2  27274  selberg3lem1  27296  pntrsumo1  27304  pntibndlem1  27328  pntibndlem3  27331  pntlemr  27341  pntlemj  27342  ostth3  27377  minvecolem3  30396  lnconi  31553  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimirlem32  36823  aks4d1p1p2  41241  stoweidlem14  45028  stoweidlem34  45048  stoweidlem42  45056  stoweidlem51  45065  stoweidlem59  45073  stirlinglem5  45092  elbigolo1  47330