Theorem rpregt0d 12959

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5099  ℝcr 11029  0cc0 11030   < clt 11170  ℝ⁺crp 12909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-rp 12910

This theorem is referenced by:  reclt1d  12966  recgt1d  12967  ltrecd  12971  lerecd  12972  ltrec1d  12973  lerec2d  12974  lediv2ad  12975  ltdiv2d  12976  lediv2d  12977  ledivdivd  12978  divge0d  12993  ltmul1d  12994  ltmul2d  12995  lemul1d  12996  lemul2d  12997  ltdiv1d  12998  lediv1d  12999  ltmuldivd  13000  ltmuldiv2d  13001  lemuldivd  13002  lemuldiv2d  13003  ltdivmuld  13004  ltdivmul2d  13005  ledivmuld  13006  ledivmul2d  13007  ltdiv23d  13020  lediv23d  13021  lt2mul2divd  13022  mertenslem1  15811  isprm6  16645  nmoi  24676  icopnfhmeo  24901  nmoleub2lem3  25075  lmnn  25223  ovolscalem1  25474  aaliou2b  26309  birthdaylem3  26923  fsumharmonic  26982  bcmono  27248  chtppilim  27446  dchrisum0lem1a  27457  dchrvmasumiflem1  27472  dchrisum0lem1b  27486  dchrisum0lem1  27487  mulog2sumlem2  27506  selberg3lem1  27528  pntrsumo1  27536  pntibndlem1  27560  pntibndlem3  27563  pntlemr  27573  pntlemj  27574  ostth3  27609  minvecolem3  30934  lnconi  32091  poimirlem29  37821  poimirlem30  37822  poimirlem31  37823  poimirlem32  37824  aks4d1p1p2  42361  stoweidlem14  46294  stoweidlem34  46314  stoweidlem42  46322  stoweidlem51  46331  stoweidlem59  46339  stirlinglem5  46358  elbigolo1  48839