Theorem rpregt0d 13094

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 13088	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1	rpgt0d 13091	. 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 5107  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13044

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-rp 13045

This theorem is used by:  reclt1d  13101  recgt1d  13102  ltrecd  13106  lerecd  13107  ltrec1d  13108  lerec2d  13109  lediv2ad  13110  ltdiv2d  13111  lediv2d  13112  ledivdivd  13113  divge0d  13128  ltmul1d  13129  ltmul2d  13130  lemul1d  13131  lemul2d  13132  ltdiv1d  13133  lediv1d  13134  ltmuldivd  13135  ltmuldiv2d  13136  lemuldivd  13137  lemuldiv2d  13138  ltdivmuld  13139  ltdivmul2d  13140  ledivmuld  13141  ledivmul2d  13142  ltdiv23d  13155  lediv23d  13156  lt2mul2divd  13157  mertenslem1  15975  isprm6  16809  nmoi  24958  icopnfhmeo  25175  nmoleub2lem3  25347  lmnn  25495  ovolscalem1  25745  aaliou2b  26577  birthdaylem3  27191  fsumharmonic  27249  bcmono  27514  chtppilim  27712  dchrisum0lem1a  27723  dchrvmasumiflem1  27738  dchrisum0lem1b  27752  dchrisum0lem1  27753  mulog2sumlem2  27772  selberg3lem1  27794  pntrsumo1  27802  pntibndlem1  27826  pntibndlem3  27829  pntlemr  27839  pntlemj  27840  ostth3  27875  minvecolem3  31358  lnconi  32515  poimirlem29  38400  poimirlem30  38401  poimirlem31  38402  poimirlem32  38403  aks4d1p1p2  42938  stoweidlem14  46844  stoweidlem34  46864  stoweidlem42  46872  stoweidlem51  46881  stoweidlem59  46889  stirlinglem5  46908  elbigolo1  49489