Theorem rpregt0d 13072

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142   class class class wbr 5108  ℝcr 11105  0cc0 11106   < clt 11249  ℝ⁺crp 13022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  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 13023

This theorem is used by:  reclt1d  13079  recgt1d  13080  ltrecd  13084  lerecd  13085  ltrec1d  13086  lerec2d  13087  lediv2ad  13088  ltdiv2d  13089  lediv2d  13090  ledivdivd  13091  divge0d  13106  ltmul1d  13107  ltmul2d  13108  lemul1d  13109  lemul2d  13110  ltdiv1d  13111  lediv1d  13112  ltmuldivd  13113  ltmuldiv2d  13114  lemuldivd  13115  lemuldiv2d  13116  ltdivmuld  13117  ltdivmul2d  13118  ledivmuld  13119  ledivmul2d  13120  ltdiv23d  13133  lediv23d  13134  lt2mul2divd  13135  mertenslem1  15945  isprm6  16779  nmoi  24896  icopnfhmeo  25113  nmoleub2lem3  25285  lmnn  25433  ovolscalem1  25683  aaliou2b  26515  birthdaylem3  27129  fsumharmonic  27187  bcmono  27452  chtppilim  27650  dchrisum0lem1a  27661  dchrvmasumiflem1  27676  dchrisum0lem1b  27690  dchrisum0lem1  27691  mulog2sumlem2  27710  selberg3lem1  27732  pntrsumo1  27740  pntibndlem1  27764  pntibndlem3  27767  pntlemr  27777  pntlemj  27778  ostth3  27813  minvecolem3  31239  lnconi  32396  poimirlem29  38328  poimirlem30  38329  poimirlem31  38330  poimirlem32  38331  aks4d1p1p2  42865  stoweidlem14  46756  stoweidlem34  46776  stoweidlem42  46784  stoweidlem51  46793  stoweidlem59  46801  stirlinglem5  46820  elbigolo1  49365