Theorem rpregt0d 9982

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 9975	. 2 |- ( ph -> A e. RR )
3	1	rpgt0d 9978	. 2 |- ( ph -> 0 < A )
4	2, 3	jca 306	1 |- ( ph -> ( A e. RR /\ 0 < A ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   class class class wbr 4093   RRcr 8074   0cc0 8075   < clt 8256   RR+crp 9932

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-rp 9933

This theorem is referenced by:  reclt1d  9989  recgt1d  9990  ltrecd  9994  lerecd  9995  ltrec1d  9996  lerec2d  9997  lediv2ad  9998  ltdiv2d  9999  lediv2d  10000  ledivdivd  10001  divge0d  10016  ltmul1d  10017  ltmul2d  10018  lemul1d  10019  lemul2d  10020  ltdiv1d  10021  lediv1d  10022  ltmuldivd  10023  ltmuldiv2d  10024  lemuldivd  10025  lemuldiv2d  10026  ltdivmuld  10027  ltdivmul2d  10028  ledivmuld  10029  ledivmul2d  10030  ltdiv23d  10036  lediv23d  10037  lt2mul2divd  10044  mertenslemi1  12159  isprm6  12782