Theorem rpregt0d 9845

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2177   class class class wbr 4051   RRcr 7944   0cc0 7945   < clt 8127   RR+crp 9795

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-rp 9796

This theorem is referenced by:  reclt1d  9852  recgt1d  9853  ltrecd  9857  lerecd  9858  ltrec1d  9859  lerec2d  9860  lediv2ad  9861  ltdiv2d  9862  lediv2d  9863  ledivdivd  9864  divge0d  9879  ltmul1d  9880  ltmul2d  9881  lemul1d  9882  lemul2d  9883  ltdiv1d  9884  lediv1d  9885  ltmuldivd  9886  ltmuldiv2d  9887  lemuldivd  9888  lemuldiv2d  9889  ltdivmuld  9890  ltdivmul2d  9891  ledivmuld  9892  ledivmul2d  9893  ltdiv23d  9899  lediv23d  9900  lt2mul2divd  9907  mertenslemi1  11921  isprm6  12544