Theorem rpregt0d 13140

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5102  ℝcr 11171  0cc0 11172   < clt 11315  ℝ⁺crp 13090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13091

This theorem is used by:  reclt1d  13147  recgt1d  13148  ltrecd  13152  lerecd  13153  ltrec1d  13154  lerec2d  13155  lediv2ad  13156  ltdiv2d  13157  lediv2d  13158  ledivdivd  13159  divge0d  13174  ltmul1d  13175  ltmul2d  13176  lemul1d  13177  lemul2d  13178  ltdiv1d  13179  lediv1d  13180  ltmuldivd  13181  ltmuldiv2d  13182  lemuldivd  13183  lemuldiv2d  13184  ltdivmuld  13185  ltdivmul2d  13186  ledivmuld  13187  ledivmul2d  13188  ltdiv23d  13201  lediv23d  13202  lt2mul2divd  13203  mertenslem1  16021  isprm6  16853  nmoi  25009  icopnfhmeo  25226  nmoleub2lem3  25398  lmnn  25546  ovolscalem1  25796  aaliou2b  26632  birthdaylem3  27245  fsumharmonic  27303  bcmono  27568  chtppilim  27766  dchrisum0lem1a  27777  dchrvmasumiflem1  27792  dchrisum0lem1b  27806  dchrisum0lem1  27807  mulog2sumlem2  27826  selberg3lem1  27848  pntrsumo1  27856  pntibndlem1  27880  pntibndlem3  27883  pntlemr  27893  pntlemj  27894  ostth3  27929  minvecolem3  31412  lnconi  32569  poimirlem29  38487  poimirlem30  38488  poimirlem31  38489  poimirlem32  38490  aks4d1p1p2  43040  stoweidlem14  46946  stoweidlem34  46966  stoweidlem42  46974  stoweidlem51  46983  stoweidlem59  46991  stirlinglem5  47010  elbigolo1  49591