Theorem rpgt0d 9735

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 9701	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2160   class class class wbr 4021  0cc0 7846   < clt 8027  ℝ⁺crp 9689

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rab 2477  df-v 2754  df-un 3148  df-sn 3616  df-pr 3617  df-op 3619  df-br 4022  df-rp 9690

This theorem is referenced by:  rpregt0d  9739  ltmulgt11d  9768  ltmulgt12d  9769  gt0divd  9770  ge0divd  9771  lediv12ad  9792  expgt0  10593  nnesq  10680  bccl2  10789  resqrexlemp1rp  11056  resqrexlemover  11060  resqrexlemnm  11068  resqrexlemgt0  11070  resqrexlemglsq  11072  sqrtgt0d  11209  reccn2ap  11362  fsumlt  11513  eirraplem  11825  dvdsmodexp  11843  prmind2  12163  sqrt2irrlem  12204  modprmn0modprm0  12299  4sqlem11  12444  4sqlem12  12445  ssblex  14416  mulc1cncf  14561  cncfmptc  14567  mulcncflem  14575  cnplimclemle  14622  pilem3  14689  iooref1o  15270  trilpolemeq1  15276  nconstwlpolemgt0  15300  taupi  15309