Theorem rpregt0d 13019

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098   class class class wbr 5138  ℝcr 11105  0cc0 11106   < clt 11245  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-rp 12972

This theorem is referenced by:  reclt1d  13026  recgt1d  13027  ltrecd  13031  lerecd  13032  ltrec1d  13033  lerec2d  13034  lediv2ad  13035  ltdiv2d  13036  lediv2d  13037  ledivdivd  13038  divge0d  13053  ltmul1d  13054  ltmul2d  13055  lemul1d  13056  lemul2d  13057  ltdiv1d  13058  lediv1d  13059  ltmuldivd  13060  ltmuldiv2d  13061  lemuldivd  13062  lemuldiv2d  13063  ltdivmuld  13064  ltdivmul2d  13065  ledivmuld  13066  ledivmul2d  13067  ltdiv23d  13080  lediv23d  13081  lt2mul2divd  13082  mertenslem1  15827  isprm6  16648  nmoi  24567  icopnfhmeo  24790  nmoleub2lem3  24964  lmnn  25113  ovolscalem1  25364  aaliou2b  26195  birthdaylem3  26801  fsumharmonic  26860  bcmono  27126  chtppilim  27324  dchrisum0lem1a  27335  dchrvmasumiflem1  27350  dchrisum0lem1b  27364  dchrisum0lem1  27365  mulog2sumlem2  27384  selberg3lem1  27406  pntrsumo1  27414  pntibndlem1  27438  pntibndlem3  27441  pntlemr  27451  pntlemj  27452  ostth3  27487  minvecolem3  30598  lnconi  31755  poimirlem29  37007  poimirlem30  37008  poimirlem31  37009  poimirlem32  37010  aks4d1p1p2  41428  stoweidlem14  45215  stoweidlem34  45235  stoweidlem42  45243  stoweidlem51  45252  stoweidlem59  45260  stirlinglem5  45279  elbigolo1  47431