Theorem rpregt0d 12950

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5095  ℝcr 11015  0cc0 11016   < clt 11156  ℝ⁺crp 12900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-rp 12901

This theorem is referenced by:  reclt1d  12957  recgt1d  12958  ltrecd  12962  lerecd  12963  ltrec1d  12964  lerec2d  12965  lediv2ad  12966  ltdiv2d  12967  lediv2d  12968  ledivdivd  12969  divge0d  12984  ltmul1d  12985  ltmul2d  12986  lemul1d  12987  lemul2d  12988  ltdiv1d  12989  lediv1d  12990  ltmuldivd  12991  ltmuldiv2d  12992  lemuldivd  12993  lemuldiv2d  12994  ltdivmuld  12995  ltdivmul2d  12996  ledivmuld  12997  ledivmul2d  12998  ltdiv23d  13011  lediv23d  13012  lt2mul2divd  13013  mertenslem1  15801  isprm6  16635  nmoi  24653  icopnfhmeo  24878  nmoleub2lem3  25052  lmnn  25200  ovolscalem1  25451  aaliou2b  26286  birthdaylem3  26900  fsumharmonic  26959  bcmono  27225  chtppilim  27423  dchrisum0lem1a  27434  dchrvmasumiflem1  27449  dchrisum0lem1b  27463  dchrisum0lem1  27464  mulog2sumlem2  27483  selberg3lem1  27505  pntrsumo1  27513  pntibndlem1  27537  pntibndlem3  27540  pntlemr  27550  pntlemj  27551  ostth3  27586  minvecolem3  30867  lnconi  32024  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  aks4d1p1p2  42173  stoweidlem14  46126  stoweidlem34  46146  stoweidlem42  46154  stoweidlem51  46163  stoweidlem59  46171  stirlinglem5  46190  elbigolo1  48672