Theorem rpgt0d 9699

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

Hypothesis

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

Assertion

Ref	Expression
rpgt0d	|- ( ph -> 0 < A )

Proof of Theorem rpgt0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 |- ( ph -> A e. RR+ )
2		rpgt0 9665	. 2 |- ( A e. RR+ -> 0 < A )
3	1, 2	syl 14	1 |- ( ph -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 2148   class class class wbr 4004   0cc0 7811   < clt 7992   RR+crp 9653

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-rp 9654

This theorem is referenced by:  rpregt0d  9703  ltmulgt11d  9732  ltmulgt12d  9733  gt0divd  9734  ge0divd  9735  lediv12ad  9756  expgt0  10553  nnesq  10640  bccl2  10748  resqrexlemp1rp  11015  resqrexlemover  11019  resqrexlemnm  11027  resqrexlemgt0  11029  resqrexlemglsq  11031  sqrtgt0d  11168  reccn2ap  11321  fsumlt  11472  eirraplem  11784  dvdsmodexp  11802  prmind2  12120  sqrt2irrlem  12161  modprmn0modprm0  12256  ssblex  13934  mulc1cncf  14079  cncfmptc  14085  mulcncflem  14093  cnplimclemle  14140  pilem3  14207  iooref1o  14785  trilpolemeq1  14791  nconstwlpolemgt0  14814  taupi  14823