Theorem rpregt0d 9697

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148   class class class wbr 4001  ℝcr 7805  0cc0 7806   < clt 7986  ℝ⁺crp 9647

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002  df-rp 9648

This theorem is referenced by:  reclt1d  9704  recgt1d  9705  ltrecd  9709  lerecd  9710  ltrec1d  9711  lerec2d  9712  lediv2ad  9713  ltdiv2d  9714  lediv2d  9715  ledivdivd  9716  divge0d  9731  ltmul1d  9732  ltmul2d  9733  lemul1d  9734  lemul2d  9735  ltdiv1d  9736  lediv1d  9737  ltmuldivd  9738  ltmuldiv2d  9739  lemuldivd  9740  lemuldiv2d  9741  ltdivmuld  9742  ltdivmul2d  9743  ledivmuld  9744  ledivmul2d  9745  ltdiv23d  9751  lediv23d  9752  lt2mul2divd  9759  mertenslemi1  11534  isprm6  12137