Theorem rpregt0d 13062

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133  0cc0 11134   < clt 11274  ℝ⁺crp 13013

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-rp 13014

This theorem is referenced by:  reclt1d  13069  recgt1d  13070  ltrecd  13074  lerecd  13075  ltrec1d  13076  lerec2d  13077  lediv2ad  13078  ltdiv2d  13079  lediv2d  13080  ledivdivd  13081  divge0d  13096  ltmul1d  13097  ltmul2d  13098  lemul1d  13099  lemul2d  13100  ltdiv1d  13101  lediv1d  13102  ltmuldivd  13103  ltmuldiv2d  13104  lemuldivd  13105  lemuldiv2d  13106  ltdivmuld  13107  ltdivmul2d  13108  ledivmuld  13109  ledivmul2d  13110  ltdiv23d  13123  lediv23d  13124  lt2mul2divd  13125  mertenslem1  15905  isprm6  16738  nmoi  24672  icopnfhmeo  24897  nmoleub2lem3  25071  lmnn  25220  ovolscalem1  25471  aaliou2b  26306  birthdaylem3  26920  fsumharmonic  26979  bcmono  27245  chtppilim  27443  dchrisum0lem1a  27454  dchrvmasumiflem1  27469  dchrisum0lem1b  27483  dchrisum0lem1  27484  mulog2sumlem2  27503  selberg3lem1  27525  pntrsumo1  27533  pntibndlem1  27557  pntibndlem3  27560  pntlemr  27570  pntlemj  27571  ostth3  27606  minvecolem3  30862  lnconi  32019  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimirlem32  37681  aks4d1p1p2  42088  stoweidlem14  46010  stoweidlem34  46030  stoweidlem42  46038  stoweidlem51  46047  stoweidlem59  46055  stirlinglem5  46074  elbigolo1  48504