Theorem rpregt0d 10032

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203   class class class wbr 4108  ℝcr 8122  0cc0 8123   < clt 8304  ℝ⁺crp 9982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rab 2529  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109  df-rp 9983

This theorem is referenced by:  reclt1d  10039  recgt1d  10040  ltrecd  10044  lerecd  10045  ltrec1d  10046  lerec2d  10047  lediv2ad  10048  ltdiv2d  10049  lediv2d  10050  ledivdivd  10051  divge0d  10066  ltmul1d  10067  ltmul2d  10068  lemul1d  10069  lemul2d  10070  ltdiv1d  10071  lediv1d  10072  ltmuldivd  10073  ltmuldiv2d  10074  lemuldivd  10075  lemuldiv2d  10076  ltdivmuld  10077  ltdivmul2d  10078  ledivmuld  10079  ledivmul2d  10080  ltdiv23d  10086  lediv23d  10087  lt2mul2divd  10094  mertenslemi1  12214  isprm6  12837