Theorem rpregt0d 9672

Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpregt0d	|- ( ph -> ( A e. RR /\ 0 < A ) )

Proof of Theorem rpregt0d

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 |- ( ph -> A e. RR+ )
2	1	rpred 9665	. 2 |- ( ph -> A e. RR )
3	1	rpgt0d 9668	. 2 |- ( ph -> 0 < A )
4	2, 3	jca 306	1 |- ( ph -> ( A e. RR /\ 0 < A ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2146   class class class wbr 3998   RRcr 7785   0cc0 7786   < clt 7966   RR+crp 9622

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999  df-rp 9623

This theorem is referenced by:  reclt1d  9679  recgt1d  9680  ltrecd  9684  lerecd  9685  ltrec1d  9686  lerec2d  9687  lediv2ad  9688  ltdiv2d  9689  lediv2d  9690  ledivdivd  9691  divge0d  9706  ltmul1d  9707  ltmul2d  9708  lemul1d  9709  lemul2d  9710  ltdiv1d  9711  lediv1d  9712  ltmuldivd  9713  ltmuldiv2d  9714  lemuldivd  9715  lemuldiv2d  9716  ltdivmuld  9717  ltdivmul2d  9718  ledivmuld  9719  ledivmul2d  9720  ltdiv23d  9726  lediv23d  9727  lt2mul2divd  9734  mertenslemi1  11509  isprm6  12112