Theorem rpregt0d 9867

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2180   class class class wbr 4062  ℝcr 7966  0cc0 7967   < clt 8149  ℝ⁺crp 9817

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rab 2497  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-sn 3652  df-pr 3653  df-op 3655  df-br 4063  df-rp 9818

This theorem is referenced by:  reclt1d  9874  recgt1d  9875  ltrecd  9879  lerecd  9880  ltrec1d  9881  lerec2d  9882  lediv2ad  9883  ltdiv2d  9884  lediv2d  9885  ledivdivd  9886  divge0d  9901  ltmul1d  9902  ltmul2d  9903  lemul1d  9904  lemul2d  9905  ltdiv1d  9906  lediv1d  9907  ltmuldivd  9908  ltmuldiv2d  9909  lemuldivd  9910  lemuldiv2d  9911  ltdivmuld  9912  ltdivmul2d  9913  ledivmuld  9914  ledivmul2d  9915  ltdiv23d  9921  lediv23d  9922  lt2mul2divd  9929  mertenslemi1  12012  isprm6  12635