Theorem rpgt0d 9841

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 9807	. 2 |- ( A e. RR+ -> 0 < A )
3	1, 2	syl 14	1 |- ( ph -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 2177   class class class wbr 4051   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-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-rp 9796

This theorem is referenced by:  rpregt0d  9845  ltmulgt11d  9874  ltmulgt12d  9875  gt0divd  9876  ge0divd  9877  lediv12ad  9898  expgt0  10739  nnesq  10826  bccl2  10935  resqrexlemp1rp  11392  resqrexlemover  11396  resqrexlemnm  11404  resqrexlemgt0  11406  resqrexlemglsq  11408  sqrtgt0d  11545  reccn2ap  11699  fsumlt  11850  eirraplem  12163  dvdsmodexp  12181  bitsmod  12342  prmind2  12517  sqrt2irrlem  12558  modprmn0modprm0  12654  4sqlem11  12799  4sqlem12  12800  modxai  12814  ssblex  14978  mulc1cncf  15136  cncfmptc  15143  mulcncflem  15154  cnplimclemle  15215  pilem3  15330  sgmnncl  15535  iooref1o  16114  trilpolemeq1  16120  nconstwlpolemgt0  16144  taupi  16153