Theorem rpgt0d 9978

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

Syntax hints:   -> wi 4   e. wcel 2202   class class class wbr 4093   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-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-rp 9933

This theorem is referenced by:  rpregt0d  9982  ltmulgt11d  10011  ltmulgt12d  10012  gt0divd  10013  ge0divd  10014  lediv12ad  10035  expgt0  10880  nnesq  10967  bccl2  11076  resqrexlemp1rp  11629  resqrexlemover  11633  resqrexlemnm  11641  resqrexlemgt0  11643  resqrexlemglsq  11645  sqrtgt0d  11782  reccn2ap  11936  fsumlt  12088  eirraplem  12401  dvdsmodexp  12419  bitsmod  12580  prmind2  12755  sqrt2irrlem  12796  modprmn0modprm0  12892  4sqlem11  13037  4sqlem12  13038  modxai  13052  ssblex  15225  mulc1cncf  15383  cncfmptc  15390  mulcncflem  15401  cnplimclemle  15462  pilem3  15577  sgmnncl  15785  iooref1o  16749  trilpolemeq1  16755  nconstwlpolemgt0  16780  taupi  16789