Theorem rpregt0d 12961

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027  0cc0 11028   < clt 11168  ℝ⁺crp 12911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-rp 12912

This theorem is referenced by:  reclt1d  12968  recgt1d  12969  ltrecd  12973  lerecd  12974  ltrec1d  12975  lerec2d  12976  lediv2ad  12977  ltdiv2d  12978  lediv2d  12979  ledivdivd  12980  divge0d  12995  ltmul1d  12996  ltmul2d  12997  lemul1d  12998  lemul2d  12999  ltdiv1d  13000  lediv1d  13001  ltmuldivd  13002  ltmuldiv2d  13003  lemuldivd  13004  lemuldiv2d  13005  ltdivmuld  13006  ltdivmul2d  13007  ledivmuld  13008  ledivmul2d  13009  ltdiv23d  13022  lediv23d  13023  lt2mul2divd  13024  mertenslem1  15809  isprm6  16643  nmoi  24632  icopnfhmeo  24857  nmoleub2lem3  25031  lmnn  25179  ovolscalem1  25430  aaliou2b  26265  birthdaylem3  26879  fsumharmonic  26938  bcmono  27204  chtppilim  27402  dchrisum0lem1a  27413  dchrvmasumiflem1  27428  dchrisum0lem1b  27442  dchrisum0lem1  27443  mulog2sumlem2  27462  selberg3lem1  27484  pntrsumo1  27492  pntibndlem1  27516  pntibndlem3  27519  pntlemr  27529  pntlemj  27530  ostth3  27565  minvecolem3  30838  lnconi  31995  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  aks4d1p1p2  42043  stoweidlem14  45996  stoweidlem34  46016  stoweidlem42  46024  stoweidlem51  46033  stoweidlem59  46041  stirlinglem5  46060  elbigolo1  48530