Theorem rpregt0d 13065

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141   class class class wbr 5108  ℝcr 11098  0cc0 11099   < clt 11242  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-rp 13016

This theorem is referenced by:  reclt1d  13072  recgt1d  13073  ltrecd  13077  lerecd  13078  ltrec1d  13079  lerec2d  13080  lediv2ad  13081  ltdiv2d  13082  lediv2d  13083  ledivdivd  13084  divge0d  13099  ltmul1d  13100  ltmul2d  13101  lemul1d  13102  lemul2d  13103  ltdiv1d  13104  lediv1d  13105  ltmuldivd  13106  ltmuldiv2d  13107  lemuldivd  13108  lemuldiv2d  13109  ltdivmuld  13110  ltdivmul2d  13111  ledivmuld  13112  ledivmul2d  13113  ltdiv23d  13126  lediv23d  13127  lt2mul2divd  13128  mertenslem1  15938  isprm6  16772  nmoi  24864  icopnfhmeo  25081  nmoleub2lem3  25253  lmnn  25401  ovolscalem1  25651  aaliou2b  26481  birthdaylem3  27094  fsumharmonic  27152  bcmono  27417  chtppilim  27615  dchrisum0lem1a  27626  dchrvmasumiflem1  27641  dchrisum0lem1b  27655  dchrisum0lem1  27656  mulog2sumlem2  27675  selberg3lem1  27697  pntrsumo1  27705  pntibndlem1  27729  pntibndlem3  27732  pntlemr  27742  pntlemj  27743  ostth3  27778  minvecolem3  31194  lnconi  32351  poimirlem29  38266  poimirlem30  38267  poimirlem31  38268  poimirlem32  38269  aks4d1p1p2  42805  stoweidlem14  46698  stoweidlem34  46718  stoweidlem42  46726  stoweidlem51  46735  stoweidlem59  46743  stirlinglem5  46762  elbigolo1  49304