Theorem rpregt0d 12990

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035  0cc0 11036   < clt 11177  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-rp 12941

This theorem is referenced by:  reclt1d  12997  recgt1d  12998  ltrecd  13002  lerecd  13003  ltrec1d  13004  lerec2d  13005  lediv2ad  13006  ltdiv2d  13007  lediv2d  13008  ledivdivd  13009  divge0d  13024  ltmul1d  13025  ltmul2d  13026  lemul1d  13027  lemul2d  13028  ltdiv1d  13029  lediv1d  13030  ltmuldivd  13031  ltmuldiv2d  13032  lemuldivd  13033  lemuldiv2d  13034  ltdivmuld  13035  ltdivmul2d  13036  ledivmuld  13037  ledivmul2d  13038  ltdiv23d  13051  lediv23d  13052  lt2mul2divd  13053  mertenslem1  15847  isprm6  16682  nmoi  24718  icopnfhmeo  24935  nmoleub2lem3  25107  lmnn  25255  ovolscalem1  25505  aaliou2b  26332  birthdaylem3  26942  fsumharmonic  27000  bcmono  27265  chtppilim  27463  dchrisum0lem1a  27474  dchrvmasumiflem1  27489  dchrisum0lem1b  27503  dchrisum0lem1  27504  mulog2sumlem2  27523  selberg3lem1  27545  pntrsumo1  27553  pntibndlem1  27577  pntibndlem3  27580  pntlemr  27590  pntlemj  27591  ostth3  27626  minvecolem3  30972  lnconi  32129  poimirlem29  38017  poimirlem30  38018  poimirlem31  38019  poimirlem32  38020  aks4d1p1p2  42556  stoweidlem14  46458  stoweidlem34  46478  stoweidlem42  46486  stoweidlem51  46495  stoweidlem59  46503  stirlinglem5  46522  elbigolo1  49049