Theorem rpregt0d 11754

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-rp 11709

This theorem is referenced by:  reclt1d  11761  recgt1d  11762  ltrecd  11766  lerecd  11767  ltrec1d  11768  lerec2d  11769  lediv2ad  11770  ltdiv2d  11771  lediv2d  11772  ledivdivd  11773  divge0d  11788  ltmul1d  11789  ltmul2d  11790  lemul1d  11791  lemul2d  11792  ltdiv1d  11793  lediv1d  11794  ltmuldivd  11795  ltmuldiv2d  11796  lemuldivd  11797  lemuldiv2d  11798  ltdivmuld  11799  ltdivmul2d  11800  ledivmuld  11801  ledivmul2d  11802  ltdiv23d  11813  lediv23d  11814  lt2mul2divd  11815  mertenslem1  14455  isprm6  15264  nmoi  22342  icopnfhmeo  22550  nmoleub2lem3  22723  lmnn  22869  ovolscalem1  23088  aaliou2b  23900  birthdaylem3  24480  fsumharmonic  24538  bcmono  24802  chtppilim  24964  dchrisum0lem1a  24975  dchrvmasumiflem1  24990  dchrisum0lem1b  25004  dchrisum0lem1  25005  mulog2sumlem2  25024  selberg3lem1  25046  pntrsumo1  25054  pntibndlem1  25078  pntibndlem3  25081  pntlemr  25091  pntlemj  25092  ostth3  25127  minvecolem3  27116  lnconi  28276  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  stoweidlem14  38907  stoweidlem34  38927  stoweidlem42  38935  stoweidlem51  38944  stoweidlem59  38952  stirlinglem5  38971  elbigolo1  42149