Theorem rpregt0d 12162

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164   class class class wbr 4873  ℝcr 10251  0cc0 10252   < clt 10391  ℝ⁺crp 12112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-rp 12113

This theorem is referenced by:  reclt1d  12169  recgt1d  12170  ltrecd  12174  lerecd  12175  ltrec1d  12176  lerec2d  12177  lediv2ad  12178  ltdiv2d  12179  lediv2d  12180  ledivdivd  12181  divge0d  12196  ltmul1d  12197  ltmul2d  12198  lemul1d  12199  lemul2d  12200  ltdiv1d  12201  lediv1d  12202  ltmuldivd  12203  ltmuldiv2d  12204  lemuldivd  12205  lemuldiv2d  12206  ltdivmuld  12207  ltdivmul2d  12208  ledivmuld  12209  ledivmul2d  12210  ltdiv23d  12223  lediv23d  12224  lt2mul2divd  12225  mertenslem1  14989  isprm6  15797  nmoi  22902  icopnfhmeo  23112  nmoleub2lem3  23284  lmnn  23431  ovolscalem1  23679  aaliou2b  24495  birthdaylem3  25093  fsumharmonic  25151  bcmono  25415  chtppilim  25577  dchrisum0lem1a  25588  dchrvmasumiflem1  25603  dchrisum0lem1b  25617  dchrisum0lem1  25618  mulog2sumlem2  25637  selberg3lem1  25659  pntrsumo1  25667  pntibndlem1  25691  pntibndlem3  25694  pntlemr  25704  pntlemj  25705  ostth3  25740  minvecolem3  28276  lnconi  29436  poimirlem29  33975  poimirlem30  33976  poimirlem31  33977  poimirlem32  33978  stoweidlem14  41018  stoweidlem34  41038  stoweidlem42  41046  stoweidlem51  41055  stoweidlem59  41063  stirlinglem5  41082  elbigolo1  43191