Theorem rpregt0d 9943

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2201   class class class wbr 4089  ℝcr 8036  0cc0 8037   < clt 8219  ℝ⁺crp 9893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rab 2518  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090  df-rp 9894

This theorem is referenced by:  reclt1d  9950  recgt1d  9951  ltrecd  9955  lerecd  9956  ltrec1d  9957  lerec2d  9958  lediv2ad  9959  ltdiv2d  9960  lediv2d  9961  ledivdivd  9962  divge0d  9977  ltmul1d  9978  ltmul2d  9979  lemul1d  9980  lemul2d  9981  ltdiv1d  9982  lediv1d  9983  ltmuldivd  9984  ltmuldiv2d  9985  lemuldivd  9986  lemuldiv2d  9987  ltdivmuld  9988  ltdivmul2d  9989  ledivmuld  9990  ledivmul2d  9991  ltdiv23d  9997  lediv23d  9998  lt2mul2divd  10005  mertenslemi1  12119  isprm6  12742