Theorem rpregt0d 12440

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538  0cc0 10539   < clt 10677  ℝ⁺crp 12392

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-rp 12393

This theorem is referenced by:  reclt1d  12447  recgt1d  12448  ltrecd  12452  lerecd  12453  ltrec1d  12454  lerec2d  12455  lediv2ad  12456  ltdiv2d  12457  lediv2d  12458  ledivdivd  12459  divge0d  12474  ltmul1d  12475  ltmul2d  12476  lemul1d  12477  lemul2d  12478  ltdiv1d  12479  lediv1d  12480  ltmuldivd  12481  ltmuldiv2d  12482  lemuldivd  12483  lemuldiv2d  12484  ltdivmuld  12485  ltdivmul2d  12486  ledivmuld  12487  ledivmul2d  12488  ltdiv23d  12501  lediv23d  12502  lt2mul2divd  12503  mertenslem1  15242  isprm6  16060  nmoi  23339  icopnfhmeo  23549  nmoleub2lem3  23721  lmnn  23868  ovolscalem1  24116  aaliou2b  24932  birthdaylem3  25533  fsumharmonic  25591  bcmono  25855  chtppilim  26053  dchrisum0lem1a  26064  dchrvmasumiflem1  26079  dchrisum0lem1b  26093  dchrisum0lem1  26094  mulog2sumlem2  26113  selberg3lem1  26135  pntrsumo1  26143  pntibndlem1  26167  pntibndlem3  26170  pntlemr  26180  pntlemj  26181  ostth3  26216  minvecolem3  28655  lnconi  29812  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  poimirlem32  34926  stoweidlem14  42306  stoweidlem34  42326  stoweidlem42  42334  stoweidlem51  42343  stoweidlem59  42351  stirlinglem5  42370  elbigolo1  44624