Theorem rpgt0d 9670

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

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpgt0d	⊢ (𝜑 → 0 < 𝐴)

Proof of Theorem rpgt0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpgt0 9636	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2146   class class class wbr 3998  0cc0 7786   < clt 7966  ℝ⁺crp 9624

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999  df-rp 9625

This theorem is referenced by:  rpregt0d  9674  ltmulgt11d  9703  ltmulgt12d  9704  gt0divd  9705  ge0divd  9706  lediv12ad  9727  expgt0  10523  nnesq  10609  bccl2  10716  resqrexlemp1rp  10983  resqrexlemover  10987  resqrexlemnm  10995  resqrexlemgt0  10997  resqrexlemglsq  10999  sqrtgt0d  11136  reccn2ap  11289  fsumlt  11440  eirraplem  11752  dvdsmodexp  11770  prmind2  12087  sqrt2irrlem  12128  modprmn0modprm0  12223  ssblex  13511  mulc1cncf  13656  cncfmptc  13662  mulcncflem  13670  cnplimclemle  13717  pilem3  13784  iooref1o  14352  trilpolemeq1  14358  nconstwlpolemgt0  14381  taupi  14388